Add [specialize_by] tactic

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