aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4299.v
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.