use new proofEngineHelpers

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index eeef8ff2d27e172c3083b5619d5fae62608f0afc..f320f08379d78a5c33f94ca1ac807bd4f7e5e650 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -121,11 +121,13 @@ let perforate context term ty =
   match get_proof () with
      None -> assert false
    | Some (uri,metasenv,bo,gty as proof') ->
-      let newmeta = new_meta proof' in
+      let newmeta = new_meta_of_proof proof' in
        (* We push the new meta at the end of the list for pretty-printing *)
        (* purposes: in this way metas are ordered.                        *)
        let metasenv' = metasenv@[newmeta,context,ty] in
-        let irl = identity_relocation_list_for_metavariable context in
+        let irl =
+          CicMkImplicit.identity_relocation_list_for_metavariable context
+        in
 (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
         let bo' =
          ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo