blob: a1daa193aed51c7079bd656dc058393c8fb0e92a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Unset Strict Universe Declaration.
Set Universe Polymorphism.
Module Type Foo.
Definition U := Type : Type.
Parameter eq : Type = U.
End Foo.
Module M : Foo with Definition U := Type : Type.
Definition U := let X := Type in Type.
Definition eq : Type = U := eq_refl.
Fail End M.
|
