From 125989fc2e9e0efa97dfc4ad3d41502e5d93ca56 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 21 Nov 2017 17:16:21 +0100
Subject: Add doc for Set Debug RAKAM.

---
 doc/refman/RefMan-tac.tex | 7 +++++++
 1 file changed, 7 insertions(+)

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}
-- 
cgit v1.2.3