moved hard coded uris to HelmLibraryObjects

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index a663282207c6057ae94cf4fdf4e7360bc74ba58f..3af6b861dd4ddafc15c18b0e8aff8d43ecba6bc6 100644 (file)
--- 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) =