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 =
;;
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
(* 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
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
(* 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