aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/ltac_plus.v
blob: 01d477bdf9707cdf7f25922922667ef815afd6d6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
(** Checks that Ltac's '+' tactical works as intended. *)

Goal forall (A B C D:Prop), (A->C) -> (B->C) -> (D->C) -> B -> C.
Proof.
  intros A B C D h0 h1 h2 h3.
  (* backtracking *)
  (apply h0 + apply h1);apply h3.
  Undo.
  Fail ((apply h0+apply h2) || apply h1); apply h3.
  (* interaction with || *)
  ((apply h0+apply h1) || apply h2); apply h3.
Qed.