From f8d58fcacc3544aeabec15d2157cb5ef6e8d6840 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 22 Jan 2004 10:41:40 +0000 Subject: [PATCH] use new proofEngineHelpers --- helm/gTopLevel/proofEngine.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 -- 2.39.2