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

1 files changed, 4 insertions, 0 deletions

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