From 5572bc8c80f53e8ac9fbb3a90502ef35e3bdc4a2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 22 Sep 2006 16:59:38 +0000
Subject: Test Tactic Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9160 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/ltac.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

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.
-- 
cgit v1.2.3