blob: 63ac6ef3841efc741a266437ba5823d360bc7855 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
(** [forward H] specializes non-dependent binders in a hypothesis [H]
with side-conditions. Side-conditions come after the main goal,
like with [replace] and [rewrite].
[eforward H] is like [forward H], but also specializes dependent
binders with evars.
Both tactics do nothing on hypotheses they cannot handle. *)
Ltac forward_step H :=
match type of H with
| ?A -> ?B => let a := fresh in cut A; [ intro a; specialize (H a); clear a | ]
end.
Ltac eforward_step H :=
match type of H with
| _ => forward_step H
| forall x : ?A, _
=> let x_or_fresh := fresh x in
evar (x_or_fresh : A);
specialize (H x_or_fresh); subst x_or_fresh
end.
Ltac forward H := try (forward_step H; [ forward H | .. ]).
Ltac eforward H := try (eforward_step H; [ eforward H | .. ]).
|
