No more anomalies from super_nsatz, hopefully

1 files changed, 2 insertions, 0 deletions

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 *)