Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 17 insertions, 1 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index da35edbe..507a1205 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -23,9 +23,13 @@ open Equality
 open Compat
 
 (**********************************************************************)
-(* replace, discriminate, injection, simplify_eq                      *)
+(* admit, replace, discriminate, injection, simplify_eq               *)
 (* cutrewrite, dependent rewrite                                      *)
 
+TACTIC EXTEND admit
+  [ "admit" ] -> [ admit_as_an_axiom ]
+END
+
 let replace_in_clause_maybe_by (sigma1,c1) c2 in_hyp tac =
   Refiner.tclWITHHOLES false
     (replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp))
@@ -761,3 +765,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