summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3483.v
blob: 2cc66186201fcedef9c994372ab47d747fe787b4 (plain)
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.