test-suite/output/UselessSyndef.v


1
2
3
4
5
6
7
8
9
10

Module M.
  Definition a := 0.
End M.
Module N.
  Notation a := M.a (only parsing).
End N.

Import M. Import N.

Check a.