aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4305.v
blob: 39fc02d22bb19cfefc9381d5fd5b15b297176f7f (plain)
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.