Adding a test-suite for tactic notation naming.

1 files changed, 20 insertions, 0 deletions

diff --git a/test-suite/success/TacticNotation1.v b/test-suite/success/TacticNotation1.v
new file mode 100644
index 000000000..289f2816e
--- /dev/null
+++ b/test-suite/success/TacticNotation1.v
@@ -0,0 +1,20 @@
+Module Type S.
+End S.
+
+Module F (E : S).
+
+  Tactic Notation "foo" := idtac.
+
+  Ltac bar := foo.
+
+End F.
+
+Module G (E : S).
+  Module M := F E.
+
+  Lemma Foo : True.
+  Proof.
+  M.bar.
+  Abort.
+
+End G.