Merge PR #6895: [compat] Remove "Refolding Reduction" option.

1 files changed, 0 insertions, 11 deletions

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
@@ -3505,17 +3505,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}
 \end{quote}