diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-29 13:20:54 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-29 13:20:54 -0700 |
| commit | ae61d5234567ab7cf8476244d6dec6f99a03da4d (patch) | |
| tree | 73abf6e1eae6f994f23dfdf5c4409501a4f062a5 /src/Algebra.v | |
| parent | b707a3012eb219de8b3575c84f9e312b4007e4aa (diff) | |
Allow side-conditions in common denom. all in hyps
This should handle #16 /
https://github.com/mit-plv/fiat-crypto/pull/16#discussion_r69009840
Diffstat (limited to 'src/Algebra.v')
| -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 := |