From 67091e1d155be19333c5e5bd2cc306792ca630d3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 3 Mar 2018 01:38:19 +0100
Subject: [compat] Remove "Refolding Reduction" option.

Following up on #6791, we remove support refolding in reduction.

We also update a test case that was not properly understood, see the
discussion in #6895.
---
 doc/refman/RefMan-tac.tex | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 40ba43b6c..2597e3c37 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3504,17 +3504,6 @@ reduced to \texttt{S t}.
 
 \end{Variants}
 
-\begin{quote}
-\optindex{Refolding Reduction}
-{\tt Refolding Reduction}
-\end{quote}
-\emph{Deprecated since 8.7}
-
-This option (off by default) controls the use of the refolding strategy
-of {\tt cbn} while doing reductions in unification, type inference and
-tactic applications. It can result in expensive unifications, as
-refolding currently uses a potentially exponential heuristic.
-
 \begin{quote}
   \optindex{Debug RAKAM}
   {\tt Set Debug RAKAM}
-- 
cgit v1.2.3