diff options
author | 2018-03-03 01:38:19 +0100 | |
---|---|---|
committer | 2018-03-08 21:15:33 +0100 | |
commit | 67091e1d155be19333c5e5bd2cc306792ca630d3 (patch) | |
tree | 04d89c833d37447ee2a02852fb887aedac1edc81 /doc | |
parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) |
[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.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-tac.tex | 11 |
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} |