aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/TacticNotation1.v
blob: 289f2816e509e826f615b08117d37f6bd04038d3 (plain)
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.