diff options
Diffstat (limited to 'src/Algebra.v')
-rw-r--r-- | src/Algebra.v | 2 |
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 *) |