blob: 2843488ba0fb4b3ae4c0c7045b799265e0cbbb75 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Module Type A .
Tactic Notation "bar" := idtac "ITSME".
End A.
Module Type B.
Tactic Notation "foo" := fail "NOTME".
End B.
Module Type C := A <+ B.
Module Type F (Import M : C).
Lemma foo : True.
Proof.
bar.
|