path: root/test-suite/bugs/closed/4298.v

Set Universe Polymorphism.

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

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