From 8e30bdf78eb5feb274b16fb1db1c7350e771ee99 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 7 Feb 2012 16:51:46 +0000
Subject: 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
---
 tactics/extratactics.ml4 | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'tactics')

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
-- 
cgit v1.2.3