path: root/test-suite/bugs/closed/bug_13216.v

Class A.
Declare Instance a:A.
Inductive T `(A) := C.
Definition f x := match x with C _ => 0 end.