blob: b4e17c2231b2997109e9bc412f9cf6a8168aaa23 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Unset Strict Universe Declaration.
Set Universe Polymorphism.
Module Type Foo.
Parameter U : Type.
End Foo.
Module Lower (X : Foo with Definition U := True : Type).
End Lower.
Module M : Foo.
Definition U := nat : Type@{i}.
End M.
|