X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=f320f08379d78a5c33f94ca1ac807bd4f7e5e650;hb=7b922ad1f9832c1edb3acea8f0c910fa2c0c20e5;hp=491fe5224f2098cf1fc87765a52c62e5e99db4f4;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 491fe5224..f320f0837 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -31,8 +31,11 @@ open ProofEngineTypes
 let proof = ref (None : proof option)
 let goal = ref (None : goal option)
 
+let get_proof () = !proof;;
+let set_proof p = proof := p;;
+
 let get_current_status_as_xml () =
-  match !proof with
+  match get_proof () with
      None -> assert false
    | Some (uri, metasenv, bo, ty) ->
       let currentproof =
@@ -54,12 +57,12 @@ let get_current_status_as_xml () =
 ;;
 
 let apply_tactic ~tactic =
- match !proof,!goal with
+ match get_proof (),!goal with
   | None,_
   | _,None -> assert false
   | Some proof', Some goal' ->
      let (newproof, newgoals) = tactic ~status:(proof', goal') in
-      proof := Some newproof;
+      set_proof (Some newproof);
       goal :=
        (match newgoals, newproof with
            goal::_, _ -> Some goal
@@ -115,14 +118,16 @@ let metas_in_term term =
 (* are efficiency reasons.                                                   *)
 let perforate context term ty =
  let module C = Cic in
-  match !proof with
+  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
@@ -137,7 +142,7 @@ let perforate context term ty =
           let metasenv'' =
            List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
           in
-           proof := Some (uri,metasenv'',bo',gty) ;
+           set_proof (Some (uri,metasenv'',bo',gty)) ;
            goal := Some newmeta
 
 
@@ -148,7 +153,7 @@ let perforate context term ty =
 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
 let reduction_tactic_in_scratch reduction_function terms ty =
  let metasenv =
-  match !proof with
+  match get_proof () with
      None -> []
    | Some (_,metasenv,_,_) -> metasenv
  in