diff options
Diffstat (limited to 'test-suite/success/ltac.v')
| -rw-r--r-- | test-suite/success/ltac.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 99cfe017..3f25f703 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -153,3 +153,25 @@ Ltac afi tac := intros; tac. Goal 1 = 2. afi ltac:auto. +(* Tactic Notation avec listes *) + +Tactic Notation "pat" hyp(id) "occs" integer_list(l) := pattern id at l. + +Goal forall x, x=0 -> x=x. +intro x. +pat x occs 1 3. +Abort. + +Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l. + +Goal forall a b c, a=0 -> b=c+a. +intros. +revert a b c H. +Abort. + +(* Used to fail until revision 9280 because of a parasitic App node with + empty args *) + +Goal True. +match None with @None => exact I end. +Abort. |