passes ~subst to FreshNameGenerator

[helm.git] / helm / ocaml / tactics / variousTactics.ml

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 5be94e7df0dd87ee7b2c1368e30052d1e7318602..5e2e39c5df9343dab2d814aff8e59d4633469501 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -65,7 +65,7 @@ e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 
 let generalize_tac 
- ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) terms
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) terms
  =
   let module PET = ProofEngineTypes in
   let generalize_tac mk_fresh_name_callback terms status =