diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b668239a6..8172b5771 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3293,6 +3293,16 @@ reduced to \texttt{S t}. \end{Variants} +\begin{quote} +\optindex{Refolding Reduction} +{\tt Refolding Reduction} +\end{quote} + +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. + \subsection{\tt unfold \qualid} \tacindex{unfold} \label{unfold} |