moved hard coded uris to HelmLibraryObjects

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

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index a807554c5be305e8f7d4285f23d3f11fcf9195f0..537ef3f5d986f06286ca7ea341cb9d2c750bed0f 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -737,9 +737,9 @@ let r =
 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv 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,t)::metasenv in
    let proof' = curi,metasenv',pbo,pty in
     let proof'',goals =
@@ -762,9 +762,9 @@ let my_cut ~term:c ~status:(proof,goal)=
 debug("my_cut di "^CicPp.ppterm c^"\n");
 
 
-  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)::metasenv in
    let proof' = curi,metasenv',pbo,pty in
     let proof'',goals =
@@ -901,9 +901,9 @@ debug("inizio EQ\n");
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] 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,a_eq_b)::metasenv in
 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
    let (proof,goals) =