diff options
| -rw-r--r-- | src/Algebra.v | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index c0f3b1fba..19a536807 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -841,14 +841,30 @@ Ltac conservative_common_denominator_inequality := | let HG := fresh in intros HG; apply H'; conservative_common_denominator_in HG; [ eexact HG | .. ] ]. +Ltac conservative_common_denominator_hyps := + try match goal with + | [H: _ |- _ ] + => progress conservative_common_denominator_in H; + [ conservative_common_denominator_hyps + | .. ] + end. + +Ltac conservative_common_denominator_inequality_hyps := + try match goal with + | [H: _ |- _ ] + => progress conservative_common_denominator_inequality_in H; + [ conservative_common_denominator_inequality_hyps + | .. ] + end. + Ltac conservative_common_denominator_all := try conservative_common_denominator; - [ repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_in H; [] end + [ try conservative_common_denominator_hyps | .. ]. Ltac conservative_common_denominator_inequality_all := try conservative_common_denominator_inequality; - [ repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_inequality_in H; [] end + [ try conservative_common_denominator_inequality_hyps | .. ]. Ltac conservative_common_denominator_equality_inequality_all := |