X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=3af6b861dd4ddafc15c18b0e8aff8d43ecba6bc6;hb=7cb90c67bc6f8113188a91ecc29f6db20db5aeb8;hp=a663282207c6057ae94cf4fdf4e7360bc74ba58f;hpb=296b163c8a2b09a6f87cbab15c2016de92fc8e70;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index a66328220..3af6b861d 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -61,9 +61,8 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
       C.Lambda
        (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
     in
-    let fresh_meta = ProofEngineHelpers.new_meta proof in
-    let irl =
-     ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+    let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
 
      let (proof',goals) =
@@ -123,9 +122,9 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
       C.Lambda
        (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
     in
-    let fresh_meta = ProofEngineHelpers.new_meta proof in
+    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
     let irl =
-     ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+     CicMkImplicit.identity_relocation_list_for_metavariable context in
     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
 
      let (proof',goals) =