From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 22 Jan 2004 10:41:40 +0000 (+0000)
Subject: use new proofEngineHelpers
X-Git-Tag: V_0_5_1_3~4
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f8d58fcacc3544aeabec15d2157cb5ef6e8d6840;p=helm.git

use new proofEngineHelpers
---

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index eeef8ff2d..f320f0837 100644
--- 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