test-suite/success/TacticNotation1.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
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.