aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2406.v
blob: 3766e795a060117d78a0d04fa931d587d15132c0 (plain)
1
2
3
4
5
6
(* Check correct handling of unsupported notations *)
Notation "'’'" := (fun x => x) (at level 20).

(* This fails with a syntax error but it is not caught by Fail
Fail Definition crash_the_rooster f := ’.
*)