diff options
| -rw-r--r-- | CHANGES | 15 | ||||
| -rw-r--r-- | tactics/coretactics.ml4 | 6 |
2 files changed, 14 insertions, 7 deletions
@@ -153,13 +153,14 @@ Tactics as existential variables in other goals. To emulate the old refine, use "refine c;shelve_unifiable". This can still cause incompatibilities in rare occasions. - * New "give_up" tactic to skip over a goal without admitting it. -- The admit tactic has been removed, "give_up" should be used instead. - To compile code containing "admit" the following solutions can be adopted: - * Add Ltac definition "Ltac admit := give_up." and terminate each - incomplete proof with "Admitted". - * Add an "Axiom" for each admitted subproof. - * Add a single "Axiom proof_admitted : False." and the Ltac definition + * New "give_up" tactic to skip over a goal. A proof containing + given up goals cannot be closed with "Qed", but only with "Admitted". +- The implementation of the admit tactic has changed: no axiom is + generated for the admitted sub proof. "admit" is now an alias for + "give_up". Code relying on this specific behavior of "admit" + can be made to work by: + * Adding an "Axiom" for each admitted subproof. + * Adding a single "Axiom proof_admitted : False." and the Ltac definition "Ltac admit := case proof_admitted.". - Matching using "lazymatch" was fundamentally modified. It now behaves like "match" (immediate execution of the matching branch) but without diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 6d3dc461ec..e909a14c9e 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -196,6 +196,12 @@ TACTIC EXTEND simple_destruct [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ] END +(* Admit *) + +TACTIC EXTEND admit + [ "admit" ] -> [ Proofview.give_up ] +END + (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) open Tacexpr |