summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3242.v
blob: 805baee1533550d4fbe67f8dc45b31180f1a75f1 (plain)
1
2
Inductive Foo (x := Type) := C : Foo -> Foo.