(* proof assistant status *)
-let proof = ref (None : proof)
-let goal = ref (None : goal)
+let proof = ref (None : proof option)
+let goal = ref (None : goal option)
let apply_tactic ~tactic:tactic =
- let (newproof, newgoal) = tactic ~status:(!proof, !goal) in
- proof := newproof;
- goal := newgoal
+ match !proof,!goal with
+ None,_
+ | _,None -> assert false
+ | Some proof', Some goal' ->
+ let (newproof, newgoals) = tactic ~status:(proof', goal') in
+ proof := Some newproof;
+ goal :=
+ (match newgoals, newproof with
+ goal::_, _ -> Some goal
+ | [], (_,(goal,_,_)::_,_,_) ->
+ (* the tactic left no open goal ; let's choose the first open goal *)
+(*CSC: here we could implement and use a proof-tree like notion... *)
+ Some goal
+ | _, _ -> None)
(* metas_in_term term *)
(* Returns the ordered list of the metas that occur in [term]. *)
(* are efficiency reasons. *)
let perforate context term ty =
let module C = Cic in
- let newmeta = new_meta !proof in
- match !proof with
- None -> assert false
- | Some (uri,metasenv,bo,gty) ->
+ match !proof with
+ None -> assert false
+ | Some (uri,metasenv,bo,gty as proof') ->
+ let newmeta = new_meta 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 elim_type term = apply_tactic (Ring.elim_type_tac ~term)
let ring () = apply_tactic Ring.ring_tac
+let fourier () = apply_tactic FourierR.fourier_tac