Changed many refman/*.tex files. Put \label and \index commands that immediately follow sectioning commands insides those sectioning commands.

If \label{...} is placed after \section{...}, then, when clicking on the
link in the HTML file produced by Hevea, we are moved to the correct
section, but the section header is just above the screen. Hevea manual
recommends writing \section{...\label{...}} and similarly for index.

On the other hand, writing commands inside the argument of sectioning
commands is potentially dangerous because these arguments are reproduced
not only to produce the section header but also to produce headers
and/or table of contents entries. Thus, \index{...} and \labels{...} may
be executed several times. Indeed, if we put a \typeout{...} instruction
inside the argument to a sectioning command then it will be executed,
besides the section itself, in the table of contents and once for every
appearance of the header.

However, it seems that the \label command are not executed several times
unless they are prefixed with \protect, and \index command is not
executed multiple times even then. So maybe it's OK to put \label and
\index inside sectioning commands.

When hyperref package is used, the \newlabel command left in .aux file
has an extra group {...} which includes another \label command! This may
lead to trouble when we use \nameref (?).

However, the most reliable way would be to use the optional argument of
sectioning commands. Then the text only goes to the optional argument and
the text plus \label plus \index goes to the main argument. The optional
argument is used for headers and table of contents. This works fine with
Hevea as well.



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

1 files changed, 7 insertions, 10 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 64f99835b6..a35f12aa6b 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -1,6 +1,6 @@
-\chapter{The \Coq~commands}\label{Addoc-coqc}
+\chapter[The \Coq~commands]{The \Coq~commands\label{Addoc-coqc}
 \ttindex{coqtop}
-\ttindex{coqc}
+\ttindex{coqc}}
 
 There are two \Coq~commands: 
 \begin{itemize}
@@ -54,8 +54,7 @@ available with \verb!coqc!  and allow you to select the byte-code or
 native-code versions of the system.
 
 
-\section{Resource file}
-\index{Resource file}
+\section[Resource file]{Resource file\index{Resource file}}
 
 When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the
 resource file \verb:$HOME/.coqrc.7.0: is loaded, where \verb:$HOME: is
@@ -70,9 +69,8 @@ directories to the load path of \Coq.
 It is possible to skip the loading of the resource file with the
 option \verb:-q:.
 
-\section{Environment variables}
-\label{EnvVariables}
-\index{Environment variables}
+\section[Environment variables]{Environment variables\label{EnvVariables}
+\index{Environment variables}}
 
 There are three environment variables used by the \Coq\ system.
 \verb:$COQBIN: for the directory where the binaries are,
@@ -84,9 +82,8 @@ only for developers that are writing their own tactics and are using
 (defined at installation time). So these variables are useful only if
 you move the \Coq\ binaries and library after installation.
 
-\section{Options}
-\index{Options of the command line}
-\label{vmoption}
+\section[Options]{Options\index{Options of the command line}
+\label{vmoption}}
 
 The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise: