diff options
| -rw-r--r-- | src/Util/Tactics.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index cca98c471..4559a1757 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -359,3 +359,29 @@ Ltac simplify_repeated_ifs_step := cut G'; [ destruct b; exact (fun z => z) | cbv iota ] end. Ltac simplify_repeated_ifs := repeat simplify_repeated_ifs_step. + +(** Like [specialize] but allows holes that get filled with evars. *) +Tactic Notation "especialize" open_constr(H) := specialize H. + +(** [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 | .. ]). |