Add tactics to implement better fraction removal

From https://github.com/coq/ceps/blob/master/text/007-nsatz-inequalities.md

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