path: root/test-suite/bugs/closed/shouldsucceed/2307.v

Inductive V: nat -> Type := VS n: V (S n).
Definition f (e: V 1): nat := match e with VS 0 => 3 end.