summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/2951.v
blob: 87d544416d68be4b0939f8ef7a55fff3ce9f025f (plain)
1
2
Record C (A: Type) : Type := { f: A }.
Existing Class C.