test-suite/bugs/closed/1551.v


1
2
3
4
5
6
7
8
9
10
11
12
13

Module Type S.
  Parameter empty: Set.
End S.

Module D (M:S).
  Import M.
  Definition empty:=nat.
End D.

Module D' (M:S).
  Import M.
  Definition empty:Set. exact nat. Qed.
End D'.