1 2 3 4 5
(* Check proper failing when using notation of non-constructors in pattern-bmatching *) Fail Definition nonsense ( x : False ) := match x with y + 2 => 0 end.