ProofEngine.proof is now an abstract data type (since we plan to have OMDoc

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 491fe5224f2098cf1fc87765a52c62e5e99db4f4..eeef8ff2d27e172c3083b5619d5fae62608f0afc 100644 (file)
--- 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,7 +118,7 @@ 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
@@ -137,7 +140,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 +151,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