From 9621d7af85f762a9b0266da5826510c4b4ffb6b2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 21 Nov 2017 17:04:18 +0100
Subject: Add doc for Set Congruence Verbose

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 675c2bf174..f29dfa30b4 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4710,6 +4710,13 @@ congruence.
     described above.
 \end{ErrMsgs}
 
+\noindent {\bf Remark: } {\tt congruence} can be made to print debug
+information by setting the following option:
+
+\begin{quote}
+\optindex{Congruence Verbose}
+{\tt Set Congruence Verbose}
+\end{quote}
 
 \section{Checking properties of terms}
 
-- 
cgit v1.2.3