blob: 955c3017d7afe8d12fe7867472b7c43c59a34a70 (
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.
|
