Add doc for Set Debug RAKAM.

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}