passes ~subst to FreshNameGenerator

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index a649d4a23e2df518e77f37f96662fd02a3fb718e..fe566ab74f779a5e8ed27ab8a5f4ed2c020ea2ee 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -52,7 +52,7 @@ let rewrite_tac ~term:equality =
         ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
       in
        C.Lambda
-        (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+        (FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context C.Anonymous ~typ:ty,
           ty, gty'')
      in
      let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
@@ -113,7 +113,7 @@ let rewrite_back_tac ~term:equality =
         ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
       in
        C.Lambda
-        (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+        (FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context C.Anonymous ~typ:ty,
           ty, gty'')
      in
      let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in