Revert change to [nsatz] (it was making Coq run out of memory)

1 files changed, 1 insertions, 1 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 42a8607ce..c017a7456 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -1447,7 +1447,7 @@ Ltac combine_field_inequalities :=
   repeat combine_field_inequalities_step.
 (** Handles field inequalities which can be made by splitting multiplications in the goal and the assumptions *)
 Ltac solve_simple_field_inequalities :=
-  repeat (apply conj || specialize_by_assumption || split_field_inequalities);
+  repeat (apply conj || split_field_inequalities);
   try assumption.
 Ltac nsatz_strip_fractions_and_aggregate_inequalities :=
   nsatz_strip_fractions;