test-suite/bugs/closed/bug_12528.v


1
2
3
4
5
6

Set Primitive Projections.
Set Universe Polymorphism.
Record ptd := Ptd { t : Type ; p : t }.
Definition type := Ptd Type (unit:Type).
Definition type' := Ptd Type (p type).
Canonical type'.