aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1551.v
blob: 48f0b551293019ca1e3478423b1b16f36b849cc2 (plain)
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'.