aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1477.v
blob: dfc8c328064e74aee52597e3fa34e5fa1d83e652 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Inductive I : Set :=
  | A : nat -> nat -> I
  | B : nat -> nat -> I.

Definition foo1 (x:I) : nat :=
  match x with
    | A a b | B a b => S b
  end.

Definition foo2 (x:I) : nat :=
  match x with
    | A _ b | B b _ => S b
  end.

Definition foo (x:I) : nat :=
  match x with
    | A a b | B b a => S b
  end.