(* DO NOT MODIFY THIS FILE DIRECTLY *)
(* It is autogenerated by dev/tools/update-compat.py. *)
Check match 2 with 0 => 0 | S n => n end.
Notation "|" := 1 (compat "8.8").
Check match 2 with 0 => 0 | S n => n end. (* fails *)