diff options
| author | emakarov | 2007-05-11 13:15:53 +0000 |
|---|---|---|
| committer | emakarov | 2007-05-11 13:15:53 +0000 |
| commit | 95f043a4aa63630de133e667f3da1f48a8f9c4f3 (patch) | |
| tree | ef2af25fdd0226d40e3f7e8ae90936bc87a8bd1d /doc/refman/RefMan-oth.tex | |
| parent | de6e0fdd9f3078b9b0ccf87ba8a7dcc9cc47c9aa (diff) | |
Made some places in the reference manual clearer. Corrected
an example about modules that produced a Coq error.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9820 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/RefMan-oth.tex')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 1fc5b5bf45..1a53adf694 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -769,12 +769,12 @@ and display the time needed to execute it. \section{Controlling display} -\subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Begin Silent} +\subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent} \label{Begin-Silent} \index{Silent mode}} This command turns off the normal displaying. -\subsection[\tt Unset Silent.]{\tt Unset Silent.\comindex{End Silent}} +\subsection[\tt Unset Silent.]{\tt Unset Silent.\comindex{Unset Silent}} This command turns the normal display on. \subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\comindex{Set Printing Width}} |