fresh_name_generator has now also the metasenv parameter.

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 28acd57ec250400b5144b5098999b68cca72e412..64b9ff790618c6305938d685229ecbb73c6801be 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -83,7 +83,7 @@ let generalize_tac
       ~start:
         (P.cut_tac 
          (C.Prod(
-           (mk_fresh_name_callback context C.Anonymous typ), 
+           (mk_fresh_name_callback metasenv context C.Anonymous typ), 
            typ,
            (ProofEngineReduction.replace_lifting_csc 1
              ~equality:(==)