From 377860b90b10bdbedad298e705eb4931b16dba1d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 Feb 2015 13:41:30 +0100 Subject: Adding a test-suite for tactic notation naming. --- test-suite/success/TacticNotation1.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 test-suite/success/TacticNotation1.v (limited to 'test-suite/success') 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. -- cgit v1.2.3