diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-21 17:04:18 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-14 12:47:47 +0100 |
| commit | 9621d7af85f762a9b0266da5826510c4b4ffb6b2 (patch) | |
| tree | f0c8a91e92150432aa9dce3377773e17911885e2 /doc | |
| parent | 0ac79cca3c9f135df4138d1e43afc2b912766974 (diff) | |
Add doc for Set Congruence Verbose
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 675c2bf17..f29dfa30b 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} |