Test Tactic Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9160 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 99cfe01779..9eb5dda721 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -153,3 +153,18 @@ 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.