aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/bug_10824.v
blob: 01271f7d61f4129070a109f990944356a80dc078 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
Module A.
Notation F := False.
Notation "!!" := False (at level 100).
Check False.
End A.

Module B.
Notation "!!" := False (at level 100).
Notation F := False.
Notation "!!" := False (at level 100).
Check False.
End B.