summaryrefslogtreecommitdiff
path: root/tactics/extratactics.ml4
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
commit61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch)
treed88d05baf35b9b09a034233300f35a694f9fa6c2 /tactics/extratactics.ml4
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'tactics/extratactics.ml4')
-rw-r--r--tactics/extratactics.ml418
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