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, 12 insertions, 0 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index da35edbedc..44a3b01737 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -761,3 +761,15 @@ TACTIC EXTEND is_hyp
     | Var _ -> tclIDTAC
     | _ -> tclFAIL 0 (str "Not a variable or hypothesis") ]
 END
+
+
+(* Command to grab the evars left unresolved at the end of a proof. *)
+(* spiwack: I put it in extratactics because it is somewhat tied with
+   the semantics of the LCF-style tactics, hence with the classic tactic
+   mode. *)
+VERNAC COMMAND EXTEND GrabEvars
+[ "Grab" "Existential" "Variables" ] ->
+  [ let p = Proof_global.give_me_the_proof () in
+    Proof.V82.grab_evars p;
+    Flags.if_verbose (fun () -> Pp.msg (Printer.pr_open_subgoals ())) () ]
+END