X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=ac28f9a28e225d36c1dff3f9328d916bef36f250;hb=ba2709d8c270e7f6ffbdb8bd3a192bc071407f03;hp=48d5ea9a63e705780a49784989a59148d852c0b6;hpb=f5b6be7239a35e1d0aba504605b5a0df5cf06726;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 48d5ea9a6..ac28f9a28 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -59,7 +59,8 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
        ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
       C.Lambda
-       (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
+       (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+         ty, gty'')
     in
     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
     let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
@@ -120,7 +121,8 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
        ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
       C.Lambda
-       (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
+       (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+         ty, gty'')
     in
     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
     let irl =