blob: d4a2e197170822debf9567f1c497aa4e52de3be4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
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.
Reset M.
|
