test-suite/bugs/closed/4301.v


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.