aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4298.v
blob: 875612ddf4070bd78ac735957fa75ea4217d293f (plain)
1
2
3
4
5
6
7
Set Universe Polymorphism.

Module Type Foo.
  Definition U := Type.
End Foo.

Fail Module M : Foo with Definition U := Prop.