test-suite/bugs/closed/4305.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

(* Check fallback when an abbreviation is not interpretable as a pattern *)

Notation foo := Type.

Definition t :=
  match 0 with
  | S foo => foo
  | _ => 0
  end.

Notation bar := (option Type).

Definition u :=
  match 0 with
  | S bar => bar
  | _ => 0
  end.