aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/348.v
blob: 28cc5cb1e6e75d664604d59ea5e668a6b2072f3b (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. Save.
End D'.