aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4877.v
blob: 7d153d9828c477e44bb1742e1a35ab2234cc20ec (plain)
1
2
3
4
5
6
7
8
9
10
11
12
Ltac induction_last :=
  let v := match goal with
           | |- forall x y, _ = _ -> _ => 1
           | |- forall x y, _ -> _ = _ -> _ => 2
           | |- forall x y, _ -> _ -> _ = _ -> _ => 3
           end in
  induction v.

Goal forall n m : nat, True -> n = m -> m = n.
  induction_last.
  reflexivity.
Qed.