diff options
Diffstat (limited to 'src/Util/Tactics.v')
-rw-r--r-- | src/Util/Tactics.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index abfc2499c..304ae3c20 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -229,6 +229,15 @@ Ltac destruct_sig_matcher HT := Ltac destruct_sig := destruct_all_matches destruct_sig_matcher. Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher. +(** try to specialize all non-dependent hypotheses using [tac] *) +Ltac specialize_by' tac := + idtac; + match goal with + | [ H : ?A -> ?B |- _ ] => let H' := fresh in assert (H' : A) by tac; specialize (H H'); clear H' + end. + +Ltac specialize_by tac := repeat specialize_by' tac. + (** 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 |