Add [Unset Printing Dependent Evars Line]

This allows a work-around for bug #4819,
https://coq.inria.fr/bugs/show_bug.cgi?id=4819.

1 files changed, 8 insertions, 0 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index aea2bae38d..6a8bda35d6 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -947,6 +947,14 @@ time of writing this documentation, the default value is 50).
 \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}}
 This command displays the current nesting depth used for display.
 
+\subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
+This command enables the printing of the ``{\tt (dependent evars: \ldots)}''
+line when {\tt -emacs} is passed.
+
+\subsection[\tt Unset Printing Dependent Evars Line.]{\tt Unset Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
+This command disables the printing of the ``{\tt (dependent evars: \ldots)}''
+line when {\tt -emacs} is passed.
+
 %\subsection{\tt Abstraction ...}
 %Not yet documented.