From 6e02a35b241c29d257c8bb90f29161892f69153b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 23 Dec 2005 09:48:18 +0000
Subject: Test printing of Tactic Notation which was broken until dec 2005

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7707 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Tactics.out | 1 +
 test-suite/output/Tactics.v   | 9 +++++++++
 2 files changed, 10 insertions(+)
 create mode 100644 test-suite/output/Tactics.out
 create mode 100644 test-suite/output/Tactics.v

diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
new file mode 100644
index 0000000000..71c59e4327
--- /dev/null
+++ b/test-suite/output/Tactics.out
@@ -0,0 +1 @@
+intro H; split; [  a H |  e H ].
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
new file mode 100644
index 0000000000..24a33651cd
--- /dev/null
+++ b/test-suite/output/Tactics.v
@@ -0,0 +1,9 @@
+(* Test printing of Tactic Notation *)
+
+Tactic Notation "a" constr(x) := apply x.
+Tactic Notation "e" constr(x) := exact x.
+
+Lemma test : True -> True /\ True.
+intro H; split; [a H|e H].
+Show Script.
+Qed.
-- 
cgit v1.2.3