diff options
Diffstat (limited to 'src/Util/Tactics.v')
| -rw-r--r-- | src/Util/Tactics.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index d0c785fed..2f9f6c59f 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -263,7 +263,7 @@ Ltac specialize_by' tac := match goal with | [ H : ?A -> ?B |- _ ] => match type of A with - Prop => + Prop => let H' := fresh in assert (H' : A) by tac; transparent_specialize_one H H'; @@ -279,6 +279,12 @@ Ltac specialize_by tac := repeat specialize_by' tac. flaw. *) Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac. +(** A marginally faster version of [specialize_by assumption] *) +Ltac specialize_by_assumption := + repeat match goal with + | [ H : ?T, H' : (?T -> ?U)%type |- _ ] => specialize (H' H) + end. + (** If [tac_in H] operates in [H] and leaves side-conditions before the original goal, then [side_conditions_before_to_side_conditions_after tac_in H] does |