diff options
| author | herbelin | 2006-09-22 16:55:14 +0000 |
|---|---|---|
| committer | herbelin | 2006-09-22 16:55:14 +0000 |
| commit | 00c1819ddfda8395cd719d9aa6475b8f30ed7076 (patch) | |
| tree | e6409a692e32f8ffa5a01462436796c7466bba9d /theories | |
| parent | 5256f8513a69b57d5a31cd0ad58768ae1c5b78ef (diff) | |
Ajout d'une valeur VList dans tacinterp pour permettre de cabler des
Tactic Notation acceptant des listes en entrée avec application à la
définition de revert dans Tactics.v.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9159 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Tactics.v | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index b1be849c2f..9750be0dfb 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -15,16 +15,7 @@ Require Import Logic. (* A shorter name for generalize + clear, can be seen as an anti-intro *) -Tactic Notation "revert" constr(a) := generalize a; clear a. -Tactic Notation "revert" constr(a) constr(b) := generalize a b; clear a b. -Tactic Notation "revert" constr(a) constr(b) constr(c) := generalize a b c; clear a b c. -Tactic Notation "revert" constr(a) constr(b) constr(c) constr(d) := generalize a b c d; clear a b c d. -Tactic Notation "revert" constr(a) constr(b) constr(c) constr(d) constr(e):= generalize a b c d e; clear a b c d e. -Tactic Notation "revert" constr(a) constr(b) constr(c) constr(d) constr(e) constr(f):= generalize a b c d e f; clear a b c d e f. -Tactic Notation "revert" constr(a) constr(b) constr(c) constr(d) constr(e) constr(f) constr(g) := generalize a b c d e f g; clear a b c d e f g. -Tactic Notation "revert" constr(a) constr(b) constr(c) constr(d) constr(e) constr(f) constr(g) constr(h) := generalize a b c d e f g h; clear a b c d e f g h. -Tactic Notation "revert" constr(a) constr(b) constr(c) constr(d) constr(e) constr(f) constr(g) constr(h) constr(i):= generalize a b c d e f g h i; clear a b c d e f g h i. -Tactic Notation "revert" constr(a) constr(b) constr(c) constr(d) constr(e) constr(f) constr(g) constr(h) constr(i) constr(j):= generalize a b c d e f g h i j; clear a b c d e f g h i j. +Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l. (* to contradict an hypothesis without copying its type. *) |