From 9314779667e9d000e07d68ea55a6dd8647a707e3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jun 2016 16:39:10 -0700 Subject: Fix a typo in the previous commit --- src/Algebra.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'src/Algebra.v') 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}. -- cgit v1.2.3