From 13b43e3c6600d60e335e65d65f4b48fc409560ab Mon Sep 17 00:00:00 2001
From: notin
Date: Mon, 2 Nov 2009 14:39:57 +0000
Subject: Correction du bug #2175

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12456 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-syn.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index d37fc9f3fc..ed54ecb670 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.
-- 
cgit v1.2.3