From 9eac0be2eb0ac450393172fa99d092da226a694b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 21 Nov 2017 17:10:16 +0100
Subject: Add doc for Set Debug Cbv.

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

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9833448015..9307f5ced7 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}
-- 
cgit v1.2.3