Correction du bug #2175

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12456 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 3 deletions

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index d37fc9f3f..ed54ecb67 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -920,7 +920,7 @@ or the ascii code of the character \verb!"! (i.e. the ascii code
 
 \subsection{Displaying informations about scopes}
 
-\subsubsection{\tt Print Visibility}
+\subsubsection{\tt Print Visibility\comindex{Print Visibility}}
 
 This displays the current stack of notations in scopes and lonely
 notations that is used to interpret a notation. The top of the stack
@@ -937,13 +937,13 @@ notations assuming that {\scope} is pushed on top of the stack.  This
 is useful to know how a subterm locally occurring in the scope of
 {\scope} is interpreted.
 
-\subsubsection{\tt Print Scope {\scope}}
+\subsubsection{\tt Print Scope {\scope}\comindex{Print Scope}}
 
 This displays all the notations defined in interpretation scope
 {\scope}.  It also displays the delimiting key if any and the class to
 which the scope is bound, if any.
 
-\subsubsection{\tt Print Scopes}
+\subsubsection{\tt Print Scopes\comindex{Print Scopes}}
 
 This displays all the notations, delimiting keys and corresponding
 class of all the existing interpretation scopes.