A "Grab Existential Variables" to transform the unresolved evars at the end of a proof into goals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14973 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 38 insertions, 10 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 748792744..83ed0ffe1 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -445,14 +445,22 @@ module V82 = struct
   let top_evars p =
     Proofview.V82.top_evars p.state.proofview
 
-  let instantiate_evar n com pr =
-    let starting_point = save_state pr in
-    let sp = pr.state.proofview in
-    try
-      let new_proofview = Proofview.V82.instantiate_evar n com sp in
-      pr.state <- { pr.state with proofview = new_proofview };
-      push_undo starting_point pr
-    with e -> 
-      restore_state starting_point pr;
-      raise e
+  let grab_evars p =
+    if not (is_done p) then
+      raise UnfinishedProof
+    else
+      save p;
+      p.state <- { p.state with proofview = Proofview.V82.grab p.state.proofview }
+    
+
+    let instantiate_evar n com pr =
+      let starting_point = save_state pr in
+      let sp = pr.state.proofview in
+      try
+	let new_proofview = Proofview.V82.instantiate_evar n com sp in
+	pr.state <- { pr.state with proofview = new_proofview };
+	push_undo starting_point pr
+      with e -> 
+	restore_state starting_point pr;
+	raise e
 end
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 7c538cf0e..15ee7cf06 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -178,6 +178,10 @@ module V82 : sig
   (* returns the existential variable used to start the proof *)
   val top_evars : proof -> Evd.evar list
 
+  (* Turns the unresolved evars into goals.
+     Raises [UnfinishedProof] if there are still unsolved goals. *)
+  val grab_evars : proof -> unit
+
   (* Implements the Existential command *)
   val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit
 end
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0d50d521f..4246cc9c7 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -475,6 +475,17 @@ module V82 = struct
   let has_unresolved_evar pv =
     Evd.has_undefined pv.solution
 
+  (* Main function in the implementation of Grab Existential Variables.*)
+  let grab pv =
+    let goals =
+      List.map begin fun (e,_) ->
+	Goal.build e
+      end (Evd.undefined_list pv.solution)
+    in
+    { pv with comb = goals }
+      
+    
+
   (* Returns the open goals of the proofview together with the evar_map to 
      interprete them. *)
   let goals { comb = comb ; solution = solution } = 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 24da9d77b..fe24b54b3 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -195,6 +195,11 @@ module V82 : sig
 
   val has_unresolved_evar : proofview -> bool
 
+  (* Main function in the implementation of Grab Existential Variables.
+     Resets the proofview's goals so that it contains all unresolved evars
+     (in chronological order of insertion). *)
+  val grab : proofview -> proofview
+
   (* Returns the open goals of the proofview together with the evar_map to 
      interprete them. *)
   val goals : proofview -> Goal.goal list Evd.sigma