test-suite/bugs/closed/bug_9166.v


1
2
3
4
5
6
7
8
9

Set Warnings "+deprecated".

Notation bar := option (compat "8.7").

Definition foo (x: nat) : nat :=
  match x with
  | 0 => 0
  | S bar => bar
  end.