test-suite/bugs/opened/shouldnotfail/1740.v


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

Definition f :=
  fun n m : nat =>
    match n, m with
      | O, _ => O
      | n, O => n
      | _, _ => O
    end.

Goal f =
  fun n m : nat =>
    match n, m with
      | O, _ => O
      | n, O => n
      | _, _ => O
    end.
  unfold f. 
  reflexivity.
Qed.