diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-21 17:16:21 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-14 12:47:47 +0100 |
commit | 125989fc2e9e0efa97dfc4ad3d41502e5d93ca56 (patch) | |
tree | be78d1e18e584e95c21ccf14f69c4a86ba8ac46f /doc | |
parent | 9eac0be2eb0ac450393172fa99d092da226a694b (diff) |
Add doc for Set Debug RAKAM.
Diffstat (limited to 'doc')
-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 9307f5ced..66a5f107a 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} |