From ae61d5234567ab7cf8476244d6dec6f99a03da4d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 29 Jun 2016 13:20:54 -0700 Subject: Allow side-conditions in common denom. all in hyps This should handle #16 / https://github.com/mit-plv/fiat-crypto/pull/16#discussion_r69009840 --- src/Algebra.v | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) (limited to 'src/Algebra.v') 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 := -- cgit v1.2.3