blob: 8a08d6465038b6a5b345efbe42f9e04049cbf99f (
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.
|
