Add doc for Set Debug Cbv.

1 files changed, 8 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 983344801..9307f5ced 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3334,6 +3334,14 @@ evaluating purely computational expressions (i.e. with little dead code).
 
 \end{Variants}
 
+\Rem The following option makes {\tt cbv} (and its derivative {\tt
+  compute}) print information about the constants it encounters and
+the unfolding decisions it makes.
+\begin{quote}
+  \optindex{Debug Cbv}
+  {\tt Set Debug Cbv}
+\end{quote}
+
 % Obsolete? Anyway not very important message
 %\begin{ErrMsgs}
 %\item \errindex{Delta must be specified before}