X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=fe566ab74f779a5e8ed27ab8a5f4ed2c020ea2ee;hb=1e51af833318b686d3852fbce5c1b516f3901b5a;hp=a649d4a23e2df518e77f37f96662fd02a3fb718e;hpb=887340c4bccbc9f83dda7bb99c9d929852d9d1a9;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index a649d4a23..fe566ab74 100644
--- 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