blob: 21cd770cbb044026ac735d1308746d922cbbcbaf (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* DO NOT MODIFY THIS FILE DIRECTLY *)
(* It is autogenerated by dev/tools/update-compat.py. *)
Set Warnings "+deprecated".
Notation bar := option (compat "8.8").
Definition foo (x: nat) : nat :=
match x with
| 0 => 0
| S bar => bar
end.
|
