diff options
Diffstat (limited to 'src/Algebra.v')
-rw-r--r-- | src/Algebra.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index bfc61fc69..c3b0434cf 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1007,7 +1007,7 @@ Ltac nsatz_inequality_to_equality := | [ H : (?R ?x ?zero -> False)%type |- False ] => apply H end. (** Clean up tactic handling side-conditions *) -Ltac super_nsatz_post_clean_inequalities try_tac := +Ltac super_nsatz_post_clean_inequalities := repeat (apply conj || split_field_inequalities); try assumption; prensatz_contradict; nsatz_inequality_to_equality; @@ -1020,9 +1020,10 @@ Ltac super_nsatz := (* Each goal left over by [prensatz_contradict] is separate (and there might not be any), so we handle them all separately *) [ try conservative_common_denominator_equality_inequality_all; - [ try nsatz_inequality_to_equality; try nsatz - | .. ]; - super_nsatz_post_clean_inequalities.. ]. + [ try nsatz_inequality_to_equality; try nsatz; + (* [nstaz] might leave over side-conditions; we handle them if they are inequalities *) + try super_nsatz_post_clean_inequalities + | super_nsatz_post_clean_inequalities.. ].. ]. Section ExtraLemmas. Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. |