diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 9307f5ced7..66a5f107a5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3515,6 +3515,13 @@ 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} +This option makes {\tt cbn} print various debugging information. +{\tt RAKAM} is the Refolding Algebraic Krivine Abstract Machine. + \subsection{\tt unfold \qualid} \tacindex{unfold} \label{unfold} |