diff options
Diffstat (limited to 'src/Util/Tactics/Forward.v')
-rw-r--r-- | src/Util/Tactics/Forward.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/Util/Tactics/Forward.v b/src/Util/Tactics/Forward.v new file mode 100644 index 000000000..63ac6ef38 --- /dev/null +++ b/src/Util/Tactics/Forward.v @@ -0,0 +1,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 | .. ]). |