X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=64b9ff790618c6305938d685229ecbb73c6801be;hb=9f60b3b0f4460aec52ec241037f6c475b421dd15;hp=04959e6962fdc2bd246db1282ae516682e5c837b;hpb=f5b6be7239a35e1d0aba504605b5a0df5cf06726;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 04959e696..64b9ff790 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -59,7 +59,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 = ProofEngineHelpers.mk_fresh_name)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
  terms ~status:((proof,goal) as status)
 =
   let module C = Cic in
@@ -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:(==)