Many improvements in tactics (and tactical) representation:

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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index ca8c0b54dc52cb0d35a8ab528859f67fbfc33451..47af12f4e35d6adeebc7e4c14d5746e1fefda8e2 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -28,13 +28,24 @@ open ProofEngineTypes
 
   (* 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].       *)
@@ -80,10 +91,10 @@ let metas_in_term 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