aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_3242.v
blob: 145375c1adb31505f8415c98967235c3402638bd (plain)
1
Inductive Foo (x := Type) := C : Foo -> Foo.