From 7884ee594837ce388c2b56466861fc6d3a8e2f40 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jun 2016 14:28:02 -0700 Subject: No more anomalies from super_nsatz, hopefully --- src/Algebra.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Algebra.v') diff --git a/src/Algebra.v b/src/Algebra.v index d0f4e62cc..eca1b2bb1 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1008,6 +1008,8 @@ Ltac nsatz_inequality_to_equality := end. (** Handles inequalities and fractions *) Ltac super_nsatz := + (* [nsatz] gives anomalies on duplicate hypotheses, so we strip them *) + clear_algebraic_duplicates; prensatz_contradict; (* Each goal left over by [prensatz_contradict] is separate (and there might not be any), so we handle them all separately *) -- cgit v1.2.3