test-suite/bugs/closed/4904.v


1
2
3
4
5
6
7
8
9
10
11

Module A.
Module B.
Notation mynat := nat.
Notation nat := nat.
End B.
End A.

Print A.B.nat. (* Notation A.B.nat := nat *)
Import A.
Print B.mynat.
Print B.nat.