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

21 files changed, 291 insertions, 429 deletions

diff --git a/doc/refman/Helm.tex b/doc/refman/Helm.tex
index af34af43cb..d07b1204c1 100644
--- a/doc/refman/Helm.tex
+++ b/doc/refman/Helm.tex
@@ -114,8 +114,7 @@ types are called inner types and are exported to files of suffix {\tt
 %% extra file of suffix {\tt proof\_tree.xml} is created. It contains the
 %% proof scripts and is used for rendering the proof.
 
-\subsection{Inner types}
-\label{inner-types}
+\subsection[Inner types]{Inner types\label{inner-types}}
 
 The type of a subterm of a construction is called an {\em inner type}
 if it respects the following conditions.
@@ -142,8 +141,7 @@ condition.
 
 There are also commands to be used interactively in {\tt coqtop}.
 
-\subsubsection{\tt Print XML {\qualid}}
-\comindex{Print XML}
+\subsubsection[\tt Print XML {\qualid}]{\tt Print XML {\qualid}\comindex{Print XML}}
 
 If the variable {\tt COQ\_XML\_LIBRARY\_ROOT} is set, this command creates
 files containing the logical content in XML format of {\qualid}. If
@@ -156,8 +154,7 @@ This writes the logical content of {\qualid} in XML format to files
 whose prefix is {\str}.
 \end{Variants}
 
-\subsubsection{{\tt Show XML Proof}}
-\comindex{Show XML Proof}
+\subsubsection[{\tt Show XML Proof}]{{\tt Show XML Proof}\comindex{Show XML Proof}}
 
 If the variable {\tt COQ\_XML\_LIBRARY\_ROOT} is set, this command creates
 files containing the current proof in progress in XML format. It
diff --git a/doc/refman/RefMan-add.tex b/doc/refman/RefMan-add.tex
index d04d1468fe..e21070d14e 100644
--- a/doc/refman/RefMan-add.tex
+++ b/doc/refman/RefMan-add.tex
@@ -1,45 +1,45 @@
-\chapter{List of additional documentation}\label{Addoc}
+\chapter[List of additional documentation]{List of additional documentation\label{Addoc}}
 
-\section{Tutorials}\label{Tutorial}
+\section[Tutorials]{Tutorials\label{Tutorial}}
 A companion volume to this reference manual, the \Coq\ Tutorial, is
 aimed at gently introducing new users to developing proofs in \Coq\
 without assuming prior knowledge of type theory. In a second step, the
 user can read also the tutorial on recursive types (document {\tt
 RecTutorial.ps}).
 
-\section{The \Coq\ standard library}\label{Addoc-library}
+\section[The \Coq\ standard library]{The \Coq\ standard library\label{Addoc-library}}
 A brief description of the \Coq\ standard library is given in the additional
 document {\tt Library.dvi}.
 
-\section{Installation and un-installation procedures}\label{Addoc-install}
+\section[Installation and un-installation procedures]{Installation and un-installation procedures\label{Addoc-install}}
 A \verb!INSTALL! file in the distribution explains how to install
 \Coq.
 
-\section{{\tt Extraction} of programs}\label{Addoc-extract}
+\section[{\tt Extraction} of programs]{{\tt Extraction} of programs\label{Addoc-extract}}
 {\tt Extraction} is a package offering some special facilities to
 extract ML program files. It is described in the separate document
 {\tt Extraction.dvi}
 \index{Extraction of programs}
 
-\section{Proof printing in {\tt Natural} language}\label{Addoc-natural}
+\section[Proof printing in {\tt Natural} language]{Proof printing in {\tt Natural} language\label{Addoc-natural}}
 {\tt Natural} is a tool to print proofs in natural language.
 It is described in the separate document {\tt Natural.dvi}.
 \index{Natural@{\tt Print Natural}}
 \index{Printing in natural language}
 
-\section{The {\tt Omega} decision tactic}\label{Addoc-omega}
+\section[The {\tt Omega} decision tactic]{The {\tt Omega} decision tactic\label{Addoc-omega}}
 {\bf Omega} is a tactic to automatically solve arithmetical goals in
 Presburger arithmetic (i.e. arithmetic without multiplication). 
 It is described in the separate document {\tt Omega.dvi}.
 \index{Omega@{\tt Omega}}
 
-\section{Simplification on rings}\label{Addoc-polynom}
+\section[Simplification on rings]{Simplification on rings\label{Addoc-polynom}}
 A documentation of the package {\tt polynom} (simplification on rings)
 can be found in the document {\tt Polynom.dvi}
 \index{Polynom@{\tt Polynom}}
 \index{Simplification on rings}
 
-%\section{Anomalies}\label{Addoc-anomalies}
+%\section[Anomalies]{Anomalies\label{Addoc-anomalies}}
 %The separate document {\tt Anomalies.*} gives a list of known
 %anomalies and bugs of the system.  Before communicating us an
 %anomalous behavior, please check first whether it has been already
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 7183e040e1..7759b80555 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1,8 +1,8 @@
-\chapter{Calculus of Inductive Constructions}
+\chapter[Calculus of Inductive Constructions]{Calculus of Inductive Constructions
 \label{Cic}
 \index{Cic@\textsc{CIC}}
 \index{pCic@p\textsc{CIC}}
-\index{Calculus of (Co)Inductive Constructions}
+\index{Calculus of (Co)Inductive Constructions}}
 
 The underlying formal language of {\Coq} is a {\em Calculus of
   Constructions} with {\em Inductive Definitions}.  It is presented in
@@ -53,7 +53,7 @@ formulation of type theory including the possibility of inductive
 constructions, Barendregt~\cite{Bar91} studies the modern form of type
 theory.
 
-\section{The terms}\label{Terms}
+\section[The terms]{The terms\label{Terms}}
 
 In most type theories, one usually makes a syntactic distinction
 between types and terms. This is not the case for \CIC\ which defines
@@ -78,8 +78,8 @@ functions which associate to each natural number $n$ an object of
 type $(P~n)$ and consequently represent proofs of the formula
 ``$\forall x.P(x)$''.
 
-\subsection{Sorts}\label{Sorts}
-\index{Sorts}
+\subsection[Sorts]{Sorts\label{Sorts}
+\index{Sorts}}
 Types are seen as terms of the language and then should belong to
 another type. The type of a type is always a constant of the language
 called a {\em sort}.
@@ -214,13 +214,13 @@ $\lb~x:T\mto U$ and $\forall x:T, U$ the occurrences of $x$ in $U$
 are bound.  They are represented by de Bruijn indexes in the internal
 structure of terms.
 
-\paragraph{Substitution.} \index{Substitution}
+\paragraph[Substitution.]{Substitution.\index{Substitution}}
 The notion of substituting a term $t$ to free occurrences of a
 variable $x$ in a term $u$ is defined as usual. The resulting term
 is written $\subst{u}{x}{t}$.
 
 
-\section{Typed terms}\label{Typed-terms}
+\section[Typed terms]{Typed terms\label{Typed-terms}}
 
 As objects of type theory, terms are subjected to {\em type
 discipline}. The well typing of a term depends on an environment which
@@ -257,7 +257,7 @@ and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$.
 A variable $x$ is said to be free in $\Gamma$ if $\Gamma$ contains a
 declaration $y:T$ such that $x$ is free in $T$.
 
-\paragraph{Environment.}\index{Environment}
+\paragraph[Environment.]{Environment.\index{Environment}}
 Because we are manipulating global declarations (constants and global
 assumptions), we also need to consider a global environment $E$.
 
@@ -281,7 +281,7 @@ rules to which the following definitions apply: if the name $c$ is
 declared in $E$, we write $c \in E$ and if $c:T$ or $c:=t:T$ is
 declared in $E$, we write $(c : T) \in E$.
 
-\paragraph{Typing rules.}\label{Typing-rules}\index{Typing rules}
+\paragraph[Typing rules.]{Typing rules.\label{Typing-rules}\index{Typing rules}}
 In the following, we assume $E$ is a valid environment wrt to
 inductive definitions.  We define simultaneously two
 judgments.  The first one \WTEG{t}{T} means the term $t$ is well-typed
@@ -348,11 +348,9 @@ well-typed without having $((\lb~x:T\mto u)~t)$ well-typed (where
 $T$ is a type of $t$). This is because the value $t$ associated to $x$
 may be used in a conversion rule (see section \ref{conv-rules}).
 
-\section{Conversion rules}
-\index{Conversion rules}
-\label{conv-rules}
-\paragraph{$\beta$-reduction.}
-\label{beta}\index{beta-reduction@$\beta$-reduction}
+\section[Conversion rules]{Conversion rules\index{Conversion rules}
+\label{conv-rules}}
+\paragraph[$\beta$-reduction.]{$\beta$-reduction.\label{beta}\index{beta-reduction@$\beta$-reduction}}
 
 We want to be able to identify some terms as we can identify the
 application of a function to a given argument with its result. For
@@ -372,8 +370,7 @@ confluence, strong normalization, subject reduction. These results are
 theoretically of great importance but we will not detail them here and
 refer the interested reader to \cite{Coq85}.
 
-\paragraph{$\iota$-reduction.}
-\label{iota}\index{iota-reduction@$\iota$-reduction}
+\paragraph[$\iota$-reduction.]{$\iota$-reduction.\label{iota}\index{iota-reduction@$\iota$-reduction}}
 A specific conversion rule is associated to the inductive objects in
 the environment.  We shall give later on (section \ref{iotared}) the
 precise rules but it just says that a destructor applied to an object
@@ -382,8 +379,7 @@ called $\iota$-reduction and is more precisely studied in
 \cite{Moh93,Wer94}.
 
 
-\paragraph{$\delta$-reduction.}
-\label{delta}\index{delta-reduction@$\delta$-reduction}
+\paragraph[$\delta$-reduction.]{$\delta$-reduction.\label{delta}\index{delta-reduction@$\delta$-reduction}}
 
 We may have defined variables in contexts or constants in the global
 environment. It is legal to identify such a reference with its value,
@@ -393,8 +389,7 @@ reduction is called $\delta$-reduction and shows as follows.
 $$\WTEGRED{x}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(x:=t:T) \in \Gamma$}~~~~~~~~~\WTEGRED{c}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(c:=t:T) \in E$}$$
 
 
-\paragraph{$\zeta$-reduction.}
-\label{zeta}\index{zeta-reduction@$\zeta$-reduction}
+\paragraph[$\zeta$-reduction.]{$\zeta$-reduction.\label{zeta}\index{zeta-reduction@$\zeta$-reduction}}
 
 Coq allows also to remove local definitions occurring in terms by
 replacing the defined variable by its value. The declaration being
@@ -403,9 +398,8 @@ called $\zeta$-reduction and shows as follows.
 
 $$\WTEGRED{\kw{let}~x:=u~\kw{in}~t}{\triangleright_{\zeta}}{\subst{t}{x}{u}}$$
 
-\paragraph{Convertibility.}
-\label{convertibility}
-\index{beta-reduction@$\beta$-reduction}\index{iota-reduction@$\iota$-reduction}\index{delta-reduction@$\delta$-reduction}\index{zeta-reduction@$\zeta$-reduction}
+\paragraph[Convertibility.]{Convertibility.\label{convertibility}
+\index{beta-reduction@$\beta$-reduction}\index{iota-reduction@$\iota$-reduction}\index{delta-reduction@$\delta$-reduction}\index{zeta-reduction@$\zeta$-reduction}}
 
 Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the environment $E$ and context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$.
 
@@ -457,7 +451,7 @@ $\lb~x:T\mto (t\ x)$ and $t$ can be identified.
 \Rem The $\eta$-reduction is not taken into account in the
 convertibility rule of \Coq.
 
-\paragraph{Normal form.}\index{Normal form}\label{Normal-form}\label{Head-normal-form}\index{Head normal form}
+\paragraph[Normal form.]{Normal form.\index{Normal form}\label{Normal-form}\label{Head-normal-form}\index{Head normal form}}
 A term which cannot be any more reduced is said to be in {\em normal
   form}. There are several ways (or strategies) to apply the reduction
 rule. Among them, we have to mention the {\em head reduction} which
@@ -536,7 +530,7 @@ derive the following property.
                 {\WF{E;\Def{\Delta}{c}{t}{T}}{\Delta}}}
 
 
-\section{Inductive Definitions}\label{Cic-inductive-definitions}
+\section[Inductive Definitions]{Inductive Definitions\label{Cic-inductive-definitions}}
 
 A (possibly mutual) inductive definition is specified by giving the
 names and the type of the inductive sets or families to be
@@ -787,7 +781,7 @@ to inconsistent systems. We restrict ourselves to definitions which
 satisfy a syntactic criterion of positivity. Before giving the formal
 rules, we need a few definitions:
 
-\paragraph{Definitions}\index{Positivity}\label{Positivity}
+\paragraph[Definitions]{Definitions\index{Positivity}\label{Positivity}}
 
 A type $T$ is an {\em arity of sort $s$}\index{Arity} if it converts
 to the sort $s$ or to a product $\forall~x:T,U$ with $U$ an arity
@@ -922,8 +916,7 @@ Inductive exType (P:Type->Prop) : Type
 %is recursive or not.  We shall write the type $(x:_R T)C$ if it is 
 %a recursive argument and $(x:_P T)C$ if the argument is not recursive.
 
-\paragraph{Sort-polymorphism of inductive families.}
-\index{Sort-polymorphism of inductive families}
+\paragraph[Sort-polymorphism of inductive families.]{Sort-polymorphism of inductive families.\index{Sort-polymorphism of inductive families}}
 
 From {\Coq} version 8.1, inductive families declared in {\Type} are
 polymorphic over their arguments in {\Type}.
@@ -1119,9 +1112,8 @@ this version of Coq to factorize the operator for primitive recursion
 into two more primitive operations as was first suggested by Th. Coquand
 in~\cite{Coq92}.  One is the definition by pattern-matching. The second one is a definition by guarded fixpoints. 
 
-\subsubsection{The {\tt match\ldots with \ldots end} construction.}
-\label{Caseexpr}
-\index{match@{\tt match\ldots with\ldots end}}
+\subsubsection[The {\tt match\ldots with \ldots end} construction.]{The {\tt match\ldots with \ldots end} construction.\label{Caseexpr}
+\index{match@{\tt match\ldots with\ldots end}}}
 
 The basic idea of this destructor operation is that we have an object
 $m$ in an inductive type $I$ and we want to prove a property $(P~m)$
@@ -1192,9 +1184,7 @@ compact notation~:
 % \Case{\bool}{l}{\Nil~ \mbox{\tt =>}~\true~ |~ (\cons~a~m)~
 %  \mbox{\tt =>}~ \false}
 
-\paragraph{Allowed elimination sorts.}
-
-\index{Elimination sorts}
+\paragraph[Allowed elimination sorts.]{Allowed elimination sorts.\index{Elimination sorts}}
 
 An important question for building the typing rule for \kw{match} is
 what can be the type of $P$ with respect to the type of the inductive
@@ -1302,10 +1292,9 @@ the two projections on this type.
 %problems if extracted terms are explicitly used such as in the 
 %{\tt Program} tactic or when extracting ML programs.
 
-\paragraph{Empty and singleton elimination}
-\label{singleton}
+\paragraph[Empty and singleton elimination]{Empty and singleton elimination\label{singleton}
 \index{Elimination!Singleton elimination}
-\index{Elimination!Empty elimination}
+\index{Elimination!Empty elimination}}
 
 There are special inductive definitions in \Prop\ for which more
 eliminations are allowed. 
@@ -1417,8 +1406,8 @@ H:(\LengthA~L~N) \\ P:\forall l:\ListA, \forall n:\nat, (\LengthA~l~n)\ra
       \end{array}}
     {\Case{P}{H}{f_1~|~f_2}:(P~L~N~H)}\]
 
-\paragraph{Definition of $\iota$-reduction.}\label{iotared}
-\index{iota-reduction@$\iota$-reduction}
+\paragraph[Definition of $\iota$-reduction.]{Definition of $\iota$-reduction.\label{iotared}
+\index{iota-reduction@$\iota$-reduction}}
 We still have to define the $\iota$-reduction in the general case.
 
 A $\iota$-redex is a term of the following form:
@@ -1432,8 +1421,7 @@ to the general reduction rule:
 \[ \Case{P}{(c_{p_i}~q_1\ldots  q_r~a_1\ldots  a_m)}{f_1|\ldots |
     f_n} \triangleright_{\iota} (f_i~a_1\ldots a_m) \]
 
-\subsection{Fixpoint definitions}
-\label{Fix-term} \index{Fix@{\tt Fix}}
+\subsection[Fixpoint definitions]{Fixpoint definitions\label{Fix-term} \index{Fix@{\tt Fix}}}
 The second operator for elimination is fixpoint definition. 
 This fixpoint may involve several mutually recursive definitions.
 The basic concrete syntax for a recursive set of mutually recursive 
@@ -1566,8 +1554,7 @@ Print sizet.
 \end{coq_example}
 
 
-\subsubsection{Reduction rule}
-\index{iota-reduction@$\iota$-reduction}
+\subsubsection[Reduction rule]{Reduction rule\index{iota-reduction@$\iota$-reduction}}
 Let $F$ be the set of declarations: $f_1/k_1:A_1:=t_1 \ldots
 f_n/k_n:A_n:=t_n$.
 The reduction for fixpoints is:
@@ -1652,8 +1639,9 @@ More information on coinductive definitions can be found
 in~\cite{Gimenez95b,Gim98,GimCas05}.
 %They are described in chapter~\ref{Coinductives}.
 
-\section{\iCIC : the Calculus of Inductive Construction with
-  impredicative \Set}\label{impredicativity}
+\section[\iCIC : the Calculus of Inductive Construction with
+  impredicative \Set]{\iCIC : the Calculus of Inductive Construction with
+  impredicative \Set\label{impredicativity}}
 
 \Coq{} can be used as a type-checker for \iCIC{}, the original 
 Calculus of Inductive Constructions with an impredicative sort \Set{}
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex
index 120c1201ef..7de837436d 100644
--- a/doc/refman/RefMan-coi.tex
+++ b/doc/refman/RefMan-coi.tex
@@ -5,7 +5,7 @@
 %\begin{document}
 
 %\coverpage{Co-inductive types in Coq}{Eduardo Gim\'enez}
-\chapter{Co-inductive types in Coq}\label{Coinductives}
+\chapter[Co-inductive types in Coq]{Co-inductive types in Coq\label{Coinductives}}
 
 %\begin{abstract}
 {\it Co-inductive} types are types whose elements may not be well-founded.
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:
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index f0db1a0fb2..5a648ae6a0 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1,5 +1,4 @@
-\chapter{Extensions of \Gallina{}}
-\label{Gallina-extension}\index{Gallina}
+\chapter[Extensions of \Gallina{}]{Extensions of \Gallina{}\label{Gallina-extension}\index{Gallina}}
 
 {\gallina} is the kernel language of {\Coq}. We describe here extensions of
 the Gallina's syntax.
@@ -610,8 +609,7 @@ Function plus (n m : nat) {struct n} : nat :=
   end.
 \end{coq_example*}
 
-\paragraph{Limitations}
-\label{sec:Function-limitations}
+\paragraph[Limitations]{Limitations\label{sec:Function-limitations}}
 \term$_0$ must be build as a \emph{pure pattern-matching tree}
 (\texttt{match...with}) with applications only \emph{at the end} of
 each branch.  For now dependent cases are not treated.
@@ -1381,10 +1379,9 @@ coercion between {\class$_1$} and {\class$_2$}.
 More details and examples, and a description of the commands related
 to coercions are provided in chapter \ref{Coercions-full}.
 
-\section{Printing constructions in full}
-\label{SetPrintingAll}
+\section[Printing constructions in full]{Printing constructions in full\label{SetPrintingAll}
 \comindex{Set Printing All}
-\comindex{Unset Printing All}
+\comindex{Unset Printing All}}
 
 Coercions, implicit arguments, the type of pattern-matching, but also
 notations (see chapter \ref{Addoc-syntax}) can obfuscate the behavior
@@ -1405,10 +1402,9 @@ printing features, use the command
 {\tt Unset Printing All.}
 \end{quote}
 
-\section{Printing universes}
-\label{PrintingUniverses}
+\section[Printing universes]{Printing universes\label{PrintingUniverses}
 \comindex{Set Printing Universes}
-\comindex{Unset Printing Universes}
+\comindex{Unset Printing Universes}}
 
 The following command:
 \begin{quote}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index f9dee72edb..424e5047da 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -99,9 +99,8 @@ Numerals are sequences of digits. Integers are numerals optionally preceded by a
 \end{tabular}
 \end{center}
 
-\paragraph{Strings}
-\label{strings}
-\index{string@{\qstring}}
+\paragraph[Strings]{Strings\label{strings}
+\index{string@{\qstring}}}
 Strings are delimited by \verb!"! (double quote), and enclose a
 sequence of any characters different from \verb!"! or the sequence
 \verb!""! to denote the double quote character. In grammars, the
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index b771196688..f24d79e28c 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -1,6 +1,5 @@
-\chapter{\Coq{} Integrated Development Environment}
-\label{Addoc-coqide}
-\ttindex{coqide}
+\chapter[\Coq{} Integrated Development Environment]{\Coq{} Integrated Development Environment\label{Addoc-coqide}
+\ttindex{coqide}}
 
 The \Coq{} Integrated Development Environment is a graphical tool, to
 be used as a user-friendly replacement to \texttt{coqtop}. Its main
@@ -90,8 +89,7 @@ termination, you may use the interrupt button (the white cross on a red circle).
 Finally, notice that these navigation buttons are also available in
 the menu, where their keyboard shortcuts are given.
 
-\section{Try tactics automatically}
-\label{sec:trytactics}
+\section[Try tactics automatically]{Try tactics automatically\label{sec:trytactics}}
 
 The menu \texttt{Try Tactics} provides some features for automatically
 trying to solve the current goal using simple tactics. If such a
@@ -287,8 +285,7 @@ to your \verb|binding "text"| section in \verb|.coqiderc-gtk2rc|.
 %\end{verbatim}
 %\end{itemize}
 
-\subsection{Character encoding for saved files}
-\label{sec:coqidecharencoding}
+\subsection[Character encoding for saved files]{Character encoding for saved files\label{sec:coqidecharencoding}}
 
 In the \texttt{Files} section of the preferences, the encoding option
 is related to the way files are saved. 
diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex
index 52935b93c1..0d5017f8ba 100644
--- a/doc/refman/RefMan-ind.tex
+++ b/doc/refman/RefMan-ind.tex
@@ -10,8 +10,7 @@
 
 %\tableofcontents
 
-\chapter{Tactics for inductive types and families}
-\label{Addoc-equality}
+\chapter[Tactics for inductive types and families]{Tactics for inductive types and families\label{Addoc-equality}}
 
 This chapter details a few special tactics useful for inferring facts
 from inductive hypotheses. They can be considered as tools that
@@ -30,8 +29,7 @@ for mutual inductive types.
 %\begin{document}
 %\coverpage{Module Inv: Inversion Tactics}{Cristina CORNES}
 
-\section{Generalities about inversion}
-\label{inversion_introduction}
+\section[Generalities about inversion]{Generalities about inversion\label{inversion_introduction}}
 When working with (co)inductive predicates, we are very often faced to
 some of these situations:
 \begin{itemize}
@@ -88,8 +86,7 @@ For example purposes we defined  \verb+Le: nat->nat->Set+
 it \texttt{Le} of type \verb+nat->nat->Prop+ or \verb+nat->nat->Type+.
 
 
-\section{Inverting an instance}
-\label{inversion_primitive}
+\section[Inverting an instance]{Inverting an instance\label{inversion_primitive}}
 \subsection{The non dependent case}
 \begin{itemize}
 
@@ -255,8 +252,7 @@ Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and
 
 
 
-\section{Deriving the inversion lemmas}
-\label{inversion_derivation}
+\section[Deriving the inversion lemmas]{Deriving the inversion lemmas\label{inversion_derivation}}
 \subsection{The non dependent case}
 
 The tactics (\texttt{Dependent}) \texttt{Inversion} and (\texttt{Dependent})
@@ -375,8 +371,7 @@ Check leminv_dep.
 
 \end{Variants}
 
-\section{Using already defined inversion  lemmas}
-\label{inversion_using}
+\section[Using already defined inversion  lemmas]{Using already defined inversion  lemmas\label{inversion_using}}
 \begin{itemize}
 \item \texttt{Inversion} \ident \texttt{ using} \ident$'$ \\
 \index{Inversion...using@{\tt Inversion...using}}
@@ -407,8 +402,8 @@ This tactic behaves as generalizing  \ident$_1$\ldots \ident$_n$,
 then doing \texttt{Use Inversion} \ident~\ident$'$.
 \end{enumerate}
 
-\section{\tt Scheme ...}\index{Scheme@{\tt Scheme}}\label{Scheme}
-\label{scheme}
+\section[\tt Scheme ...]{\tt Scheme ...\index{Scheme@{\tt Scheme}}\label{Scheme}
+\label{scheme}}
 The {\tt Scheme} command is a high-level tool for generating
 automatically (possibly mutual) induction principles for given types
 and sorts.  Its syntax follows the schema :
@@ -491,8 +486,8 @@ Check odd_even.
 The type of {\tt even\_odd} shares the same premises but the
 conclusion is {\tt (n:nat)(even n)->(Q n)}.
 
-\subsection{\tt Combined Scheme ...}\index{CombinedScheme@{\tt Combined Scheme}}\label{CombinedScheme}
-\label{combinedscheme}
+\subsection[\tt Combined Scheme ...]{\tt Combined Scheme ...\index{CombinedScheme@{\tt Combined Scheme}}\label{CombinedScheme}
+\label{combinedscheme}}
 The {\tt Combined Scheme} command is a tool for combining 
 induction principles generated by the {\tt Scheme} command.
 Its syntax follows the schema :
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 65eab3b742..3d22663c6f 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -1,5 +1,4 @@
-\chapter{The {\Coq} library}
-\index{Theories}\label{Theories}
+\chapter[The {\Coq} library]{The {\Coq} library\index{Theories}\label{Theories}}
 
 The \Coq\ library is structured into three parts:
 
@@ -23,8 +22,7 @@ The \Coq\ library is structured into three parts:
 
 This chapter briefly reviews these libraries.
 
-\section{The basic library}
-\label{Prelude}
+\section[The basic library]{The basic library\label{Prelude}}
 
 This section lists the basic notions and results which are directly
 available in the standard \Coq\ system\footnote{Most 
@@ -39,7 +37,7 @@ root directory; this includes the modules
 and {\tt Wf}.
 Module {\tt Logic\_Type} also makes it in the initial state}.
 
-\subsection{Notations} \label{Notations}
+\subsection[Notations]{Notations\label{Notations}}
 
 This module defines the parsing and pretty-printing of many symbols
 (infixes, prefixes, etc.). However, it does not assign a meaning to these
@@ -84,8 +82,7 @@ Notation & Precedence & Associativity \\
 \label{init-notations}
 \end{figure}
 
-\subsection{Logic} 
-\label{Logic}
+\subsection[Logic]{Logic\label{Logic}}
 
 \begin{figure}
 \begin{centerframe}
@@ -130,8 +127,8 @@ primitive universal quantification (it is a dependent product over a
 proposition). The primitive universal quantification allows both
 first-order and higher-order quantification.
 
-\subsubsection{Propositional Connectives} \label{Connectives}
-\index{Connectives}
+\subsubsection[Propositional Connectives]{Propositional Connectives\label{Connectives}
+\index{Connectives}}
 
 First, we find propositional calculus connectives:
 \ttindex{True}
@@ -173,8 +170,8 @@ Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
 Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
 \end{coq_example*}
 
-\subsubsection{Quantifiers} \label{Quantifiers}
-\index{Quantifiers}
+\subsubsection[Quantifiers]{Quantifiers\label{Quantifiers}
+\index{Quantifiers}}
 
 Then we find first-order quantifiers:
 \ttindex{all}
@@ -208,8 +205,8 @@ The following abbreviations are allowed:
 The type annotation \texttt{:A} can be omitted when \texttt{A} can be
 synthesized by the system.
 
-\subsubsection{Equality} \label{Equality}
-\index{Equality}
+\subsubsection[Equality]{Equality\label{Equality}
+\index{Equality}}
 
 Then, we find equality, defined as an inductive relation. That is,
 given a \verb:Type: \verb:A: and an \verb:x: of type \verb:A:, the
@@ -226,8 +223,7 @@ Inductive eq (A:Type) (x:A) : A -> Prop :=
     refl_equal : eq A x x.
 \end{coq_example*}
 
-\subsubsection{Lemmas} 
-\label{PreludeLemmas}
+\subsubsection[Lemmas]{Lemmas\label{PreludeLemmas}}
 
 Finally, a few easy lemmas are provided.
 
@@ -297,9 +293,8 @@ Theorem f_equal3 :
 Abort.
 \end{coq_eval}
 
-\subsection{Datatypes}
-\label{Datatypes}
-\index{Datatypes}
+\subsection[Datatypes]{Datatypes\label{Datatypes}
+\index{Datatypes}}
 
 \begin{figure}
 \begin{centerframe}
@@ -331,8 +326,7 @@ In the basic library, we find the definition\footnote{They are in {\tt
 defined as inductive constructions over the sort \verb:Set:. Some of
 them come with a special syntax shown on Figure~\ref{specif-syntax}.
 
-\subsubsection{Programming} 
-\label{Programming}
+\subsubsection[Programming]{Programming\label{Programming}
 \index{Programming}
 \label{libnats}
 
@@ -348,7 +342,7 @@ them come with a special syntax shown on Figure~\ref{specif-syntax}.
 \ttindex{Some}
 \ttindex{None}
 \ttindex{identity}
-\ttindex{refl\_identity}
+\ttindex{refl\_identity}}
 
 \begin{coq_example*}
 Inductive unit : Set := tt.
@@ -833,8 +827,7 @@ additional document \verb!Library.dvi!. They are also accessible on the WWW
 through the \Coq\ homepage
 \footnote{\texttt{http://coq.inria.fr}}.
 
-\subsection{Notations for integer arithmetics}
-\index{Arithmetical notations}
+\subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}}
 
 On figure \ref{zarith-syntax} is described the syntax of expressions
 for integer arithmetics. It is provided by requiring and opening the
@@ -889,9 +882,8 @@ Open Scope Z_scope.
 Check 2 + 3.
 \end{coq_example}
 
-\subsection{Peano's arithmetic (\texttt{nat})}
-\index{Peano's arithmetic}
-\ttindex{nat\_scope}
+\subsection[Peano's arithmetic (\texttt{nat})]{Peano's arithmetic (\texttt{nat})\index{Peano's arithmetic}
+\ttindex{nat\_scope}}
 
 While in the initial state, many operations and predicates of Peano's
 arithmetic are defined, further operations and results belong to other
@@ -925,8 +917,7 @@ Notation & Interpretation \\
 
 \subsection{Real numbers library}
 
-\subsubsection{Notations for real numbers}
-\index{Notations for real numbers}
+\subsubsection[Notations for real numbers]{Notations for real numbers\index{Notations for real numbers}}
 
 This is provided by requiring and opening the module {\tt Reals} and
 opening scope {\tt R\_scope}. This set of notations is very similar to
@@ -1031,8 +1022,7 @@ in document \url{http://coq.inria.fr/~desmettr/Reals.ps}.
 Reset Initial.
 \end{coq_eval}
 
-\subsection{List library}
-\index{Notations for lists}
+\subsection[List library]{List library\index{Notations for lists}
 \ttindex{length}
 \ttindex{head}
 \ttindex{tail}
@@ -1042,7 +1032,7 @@ Reset Initial.
 \ttindex{map}
 \ttindex{flat\_map}
 \ttindex{fold\_left}
-\ttindex{fold\_right}
+\ttindex{fold\_right}}
 
 Some elementary operations on polymorphic lists are defined here. They
 can be accessed by requiring module {\tt List}.
@@ -1081,9 +1071,8 @@ Notation & Interpretation & Precedence & Associativity\\
 \end{figure}
 
 
-\section{Users' contributions}
-\index{Contributions}
-\label{Contributions}
+\section[Users' contributions]{Users' contributions\index{Contributions}
+\label{Contributions}}
 
 Numerous users' contributions have been collected and are available at
 URL \url{coq.inria.fr/contribs/}.  On this web page, you have a list
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 0fbe6f4687..467a473462 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1,5 +1,4 @@
-\chapter{The tactic language}
-\label{TacticLanguage}
+\chapter[The tactic language]{The tactic language\label{TacticLanguage}}
 
 %\geometry{a4paper,body={5in,8in}}
 
@@ -257,9 +256,8 @@ of Ltac.
 
 %% \subsection{Evaluation}
 
-\subsubsection{Sequence}
-\tacindex{;}
-\index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}}
+\subsubsection[Sequence]{Sequence\tacindex{;}
+\index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}}}
 
 A sequence is an expression of the following form:
 \begin{quote}
@@ -270,8 +268,7 @@ $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied
 and $v_2$ is applied to every subgoal generated by the application of
 $v_1$. Sequence is left-associative.
 
-\subsubsection{General sequence}
-\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}
+\subsubsection[General sequence]{General sequence\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}}
 %\tacindex{; [ | ]}
 %\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
 \index{Tacticals!; [ | ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
@@ -292,9 +289,8 @@ split ; [ | auto ]} is a shortcut for
 {\tt split ; [ idtac | auto ]}.
 
 
-\subsubsection{For loop}
-\tacindex{do}
-\index{Tacticals!do@{\tt do}}
+\subsubsection[For loop]{For loop\tacindex{do}
+\index{Tacticals!do@{\tt do}}}
 
 There is a for loop that repeats a tactic {\num} times:
 \begin{quote}
@@ -306,9 +302,8 @@ application of $v$, $v$ is applied, at least once, to the generated
 subgoals and so on. It fails if the application of $v$ fails before
 the {\num} applications have been completed.
 
-\subsubsection{Repeat loop}
-\tacindex{repeat}
-\index{Tacticals!repeat@{\tt repeat}}
+\subsubsection[Repeat loop]{Repeat loop\tacindex{repeat}
+\index{Tacticals!repeat@{\tt repeat}}}
 
 We have a repeat loop with:
 \begin{quote}
@@ -320,9 +315,8 @@ of $v$, $v$ is applied, at least once, to the generated subgoals and
 so on. It stops when it fails for all the generated subgoals. It never
 fails.
 
-\subsubsection{Error catching}
-\tacindex{try}
-\index{Tacticals!try@{\tt try}}
+\subsubsection[Error catching]{Error catching\tacindex{try}
+\index{Tacticals!try@{\tt try}}}
 
 We can catch the tactic errors with:
 \begin{quote}
@@ -333,8 +327,7 @@ applied. If the application of $v$ fails, it catches the error and
 leaves the goal unchanged. If the level of the exception is positive,
 then the exception is re-raised with its level decremented.
 
-\subsubsection{Detecting progress}
-\tacindex{progress}
+\subsubsection[Detecting progress]{Detecting progress\tacindex{progress}}
 
 We can check if a tactic made progress with:
 \begin{quote}
@@ -347,9 +340,8 @@ raised.
 
 \ErrMsg \errindex{Failed to progress}
 
-\subsubsection{Branching}
-\tacindex{$\mid\mid$}
-\index{Tacticals!orelse@{\tt $\mid\mid$}}
+\subsubsection[Branching]{Branching\tacindex{$\mid\mid$}
+\index{Tacticals!orelse@{\tt $\mid\mid$}}}
 
 We can easily branch with the following structure:
 \begin{quote}
@@ -359,9 +351,8 @@ We can easily branch with the following structure:
 $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if
 it fails to progress then $v_2$ is applied. Branching is left-associative.
 
-\subsubsection{First tactic to work}
-\tacindex{first}
-\index{Tacticals!first@{\tt first}}
+\subsubsection[First tactic to work]{First tactic to work\tacindex{first}
+\index{Tacticals!first@{\tt first}}}
 
 We may consider the first tactic to work (i.e. which does not fail) among a
 panel of tactics:
@@ -374,9 +365,8 @@ tries to apply $v_2$ and so on. It fails when there is no applicable tactic.
 
 \ErrMsg \errindex{No applicable tactic}
 
-\subsubsection{Solving}
-\tacindex{solve}
-\index{Tacticals!solve@{\tt solve}}
+\subsubsection[Solving]{Solving\tacindex{solve}
+\index{Tacticals!solve@{\tt solve}}}
 
 We may consider the first to solve (i.e. which generates no subgoal) among a
 panel of tactics:
@@ -389,9 +379,8 @@ tries to apply $v_2$ and so on. It fails if there is no solving tactic.
 
 \ErrMsg \errindex{Cannot solve the goal}
 
-\subsubsection{Identity}
-\tacindex{idtac}
-\index{Tacticals!idtac@{\tt idtac}}
+\subsubsection[Identity]{Identity\tacindex{idtac}
+\index{Tacticals!idtac@{\tt idtac}}}
 
 The constant {\tt idtac} is the identity tactic: it leaves any goal
 unchanged but it appears in the proof script.
@@ -404,9 +393,8 @@ interpreted in the current environment. In particular, if a variable
 is given, its value is printed.
 
 
-\subsubsection{Failing}
-\tacindex{fail}
-\index{Tacticals!fail@{\tt fail}}
+\subsubsection[Failing]{Failing\tacindex{fail}
+\index{Tacticals!fail@{\tt fail}}}
 
 The tactic {\tt fail} is the always-failing tactic: it does not solve
 any goal. It is useful for defining other tacticals since it can be
@@ -429,11 +417,10 @@ This is a combination of the previous variants.
 
 \ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}.
 
-\subsubsection{Local definitions}
-\index{Ltac!let}
+\subsubsection[Local definitions]{Local definitions\index{Ltac!let}
 \index{Ltac!let rec}
 \index{let!in Ltac}
-\index{let rec!in Ltac}
+\index{let rec!in Ltac}}
 
 Local definitions can be done as follows:
 \begin{quote}
@@ -468,9 +455,8 @@ definition expecting at least $n$ arguments.  The expressions
 
 %\subsection{Application of tactic values}
 
-\subsubsection{Function construction}
-\index{fun!in Ltac}
-\index{Ltac!fun}
+\subsubsection[Function construction]{Function construction\index{fun!in Ltac}
+\index{Ltac!fun}}
 
 A parameterized tactic can be built anonymously (without resorting to
 local definitions) with:
@@ -480,9 +466,8 @@ local definitions) with:
 Indeed, local definitions of functions are a syntactic sugar for
 binding a {\tt fun} tactic to an identifier.
 
-\subsubsection{Pattern matching on terms}
-\index{Ltac!match}
-\index{match!in Ltac}
+\subsubsection[Pattern matching on terms]{Pattern matching on terms\index{Ltac!match}
+\index{match!in Ltac}}
 
 We can carry out pattern matching on terms with:
 \begin{quote}
@@ -578,11 +563,10 @@ expression gets bound to the variable $x$.
 
 \end{Variants}
 
-\subsubsection{Pattern matching on goals}
-\index{Ltac!match goal}
+\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal}
 \index{Ltac!match reverse goal}
 \index{match goal!in Ltac}
-\index{match reverse goal!in Ltac}
+\index{match reverse goal!in Ltac}}
 
 We can make pattern matching on goals using the following expression:
 \begin{quote}
@@ -661,8 +645,7 @@ test_lazy || idtac "was lazy".
 test_eager || idtac "was lazy".
 \end{coq_example}
 
-\subsubsection{Filling a term context}
-\index{context!in expression}
+\subsubsection[Filling a term context]{Filling a term context\index{context!in expression}}
 
 The following expression is not a tactic in the sense that it does not
 produce subgoals but generates a term to be used in tactic
@@ -678,9 +661,8 @@ replaces the hole of the value of {\ident} by the value of
 \ErrMsg \errindex{not a context variable}
 
 
-\subsubsection{Generating fresh hypothesis names}
-\index{Ltac!fresh}
-\index{fresh!in Ltac}
+\subsubsection[Generating fresh hypothesis names]{Generating fresh hypothesis names\index{Ltac!fresh}
+\index{fresh!in Ltac}}
 
 Tactics sometimes have to generate new names for hypothesis. Letting
 the system decide a name with the {\tt intro} tactic is not so good
@@ -697,9 +679,8 @@ has to refer to a name, or directly a name denoted by a
 with a number so that it becomes fresh. If no component is
 given, the name is a fresh derivative of the name {\tt H}.
 
-\subsubsection{Computing in a constr}
-\index{Ltac!eval}
-\index{eval!in Ltac}
+\subsubsection[Computing in a constr]{Computing in a constr\index{Ltac!eval}
+\index{eval!in Ltac}}
 
 Evaluation of a term can be performed with:
 \begin{quote}
@@ -720,18 +701,16 @@ The following returns the type of {\term}:
 {\tt type of} {\term}
 \end{quote}
 
-\subsubsection{Accessing tactic decomposition}
-\tacindex{info}
-\index{Tacticals!info@{\tt info}}
+\subsubsection[Accessing tactic decomposition]{Accessing tactic decomposition\tacindex{info}
+\index{Tacticals!info@{\tt info}}}
 
 Tactical ``{\tt info} {\tacexpr}'' is not really a tactical. For
 elementary tactics, this is equivalent to \tacexpr. For complex tactic
 like \texttt{auto}, it displays the operations performed by the
 tactic.
 
-\subsubsection{Proving a subgoal as a separate lemma}
-\tacindex{abstract}
-\index{Tacticals!abstract@{\tt abstract}}
+\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}
+\index{Tacticals!abstract@{\tt abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called 
@@ -750,8 +729,7 @@ without having to cut manually the proof in smaller lemmas.
 
 \ErrMsg \errindex{Proof is not complete}
 
-\subsubsection{Calling an external tactic}
-\index{Ltac!external}
+\subsubsection[Calling an external tactic]{Calling an external tactic\index{Ltac!external}}
 
 The tactic {\tt external} allows to run an executable outside the
 {\Coq} executable. The communication is done via an XML encoding of
@@ -814,8 +792,7 @@ An example of parser for this DTD, written in the Objective Caml -
 Camlp4 language, can be found in the file {\tt parsing/g\_xml.ml4} of
 the {\Coq} source archive.
 
-\section{Tactic toplevel definitions}
-\comindex{Ltac}
+\section[Tactic toplevel definitions]{Tactic toplevel definitions\comindex{Ltac}}
 
 \subsection{Defining {\ltac} functions}
 
@@ -856,8 +833,7 @@ possible with the syntax:
 %to be evaluated is the name of a recursive definition).
 
 
-\subsection{Printing {\ltac} tactics}
-\comindex{Print Ltac}
+\subsection[Printing {\ltac} tactics]{Printing {\ltac} tactics\comindex{Print Ltac}}
 
 Defined {\ltac} functions can be displayed using the command
 
@@ -865,10 +841,9 @@ Defined {\ltac} functions can be displayed using the command
 {\tt Print Ltac {\qualid}.}
 \end{quote}
 
-\section{Debugging {\ltac} tactics}
-\comindex{Set Ltac Debug}
+\section[Debugging {\ltac} tactics]{Debugging {\ltac} tactics\comindex{Set Ltac Debug}
 \comindex{Unset Ltac Debug}
-\comindex{Test Ltac Debug}
+\comindex{Test Ltac Debug}}
 
 The {\ltac} interpreter comes with a step-by-step debugger. The
 debugger can be activated using the command
diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex
index e08c7c401a..42dd12d60a 100644
--- a/doc/refman/RefMan-modr.tex
+++ b/doc/refman/RefMan-modr.tex
@@ -1,5 +1,4 @@
-\chapter{The Module System}
-\label{chapter:Modules}
+\chapter[The Module System]{The Module System\label{chapter:Modules}}
 
 The module system extends the Calculus of Inductive Constructions
 providing a convenient way to structure large developments as well as
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index ac5d3ddd3e..1fc5b5bf45 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -1,10 +1,9 @@
-\chapter{Vernacular commands}
-\label{Vernacular-commands}
-\label{Other-commands}
+\chapter[Vernacular commands]{Vernacular commands\label{Vernacular-commands}
+\label{Other-commands}}
 
 \section{Displaying}
 
-\subsection{\tt Print {\qualid}.}\comindex{Print}
+\subsection[\tt Print {\qualid}.]{\tt Print {\qualid}.\comindex{Print}}
 This command displays on the screen informations about the declared or
 defined object referred by {\qualid}.
 
@@ -33,7 +32,7 @@ arguments and argument scopes.
 %to be computed and displays it.
 \end{Variants}
 
-\subsection{\tt Print All.}\comindex{Print All}
+\subsection[\tt Print All.]{\tt Print All.\comindex{Print All}}
 This command displays informations about the current state of the
 environment, including sections and modules.
 
@@ -53,14 +52,12 @@ displays the objects defined since the beginning of this section.
 
 \section{Requests to the environment}
 
-\subsection{\tt Check {\term}.}
-\label{Check}
-\comindex{Check}
+\subsection[\tt Check {\term}.]{\tt Check {\term}.\label{Check}
+\comindex{Check}}
 This command displays the type of {\term}. When called in proof mode, 
 the term is checked in the local context of the current subgoal.
 
-\subsection{\tt Eval {\rm\sl convtactic} in {\term}.}
-\comindex{Eval}
+\subsection[\tt Eval {\rm\sl convtactic} in {\term}.]{\tt Eval {\rm\sl convtactic} in {\term}.\comindex{Eval}}
 
 This command performs the specified reduction on {\term}, and displays
 the resulting term with its type. The term to be reduced may depend on
@@ -69,9 +66,8 @@ progress).
 
 \SeeAlso section~\ref{Conversion-tactics}.
 
-\subsection{\tt Extraction \term.}
-\label{ExtractionTerm}
-\comindex{Extraction} 
+\subsection[\tt Extraction \term.]{\tt Extraction \term.\label{ExtractionTerm}
+\comindex{Extraction}} 
 This command displays the extracted term from
 {\term}. The extraction is processed according to the distinction
 between {\Set} and {\Prop}; that is to say, between logical and
@@ -87,8 +83,7 @@ displayed as in \Coq\ terms.
 
 \SeeAlso chapter~\ref{Extraction}.
 
-\subsection{\tt Opaque \qualid$_1$ \dots \qualid$_n$.}
-\comindex{Opaque}\label{Opaque} This command tells not to unfold the
+\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} This command tells not to unfold the
 the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
 $\delta$-conversion. Unfolding a constant is replacing it by its
 definition. {\tt Opaque} can only apply on constants originally
@@ -113,8 +108,7 @@ environment}\\
     and if \texttt{bar} does not exist, \texttt{foo} is set opaque.
 \end{ErrMsgs}
 
-\subsection{\tt Transparent \qualid$_1$ \dots \qualid$_n$.}
-\comindex{Transparent}\label{Transparent}
+\subsection[\tt Transparent \qualid$_1$ \dots \qualid$_n$.]{\tt Transparent \qualid$_1$ \dots \qualid$_n$.\comindex{Transparent}\label{Transparent}}
 This command is the converse of {\tt Opaque} and can only apply on constants originally defined as {\tt Transparent} to restore their initial behaviour after an {\tt Opaque} command.
 
 The constants automatically declared transparent are the ones defined by a proof ended by {\tt Defined}, or by a {\tt
@@ -142,7 +136,7 @@ environment}\\
 \SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
 \ref{Theorem}
 
-\subsection{\tt Search {\qualid}.}\comindex{Search}
+\subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}}
 This command displays the name and type of all theorems of the current
 context whose statement's conclusion has the form {\tt ({\qualid} t1 ..
   tn)}.  This command is useful to remind the user of the name of
@@ -172,7 +166,7 @@ No module \module{} has been required (see section~\ref{Require}).
 
 \end{Variants}
 
-\subsection{\tt SearchAbout {\qualid}.}\comindex{SearchAbout}
+\subsection[\tt SearchAbout {\qualid}.]{\tt SearchAbout {\qualid}.\comindex{SearchAbout}}
 This command displays the name and type of all objects (theorems,
 axioms, etc) of the current context whose statement contains \qualid.
 This command is useful to remind the user of the name of library
@@ -223,7 +217,7 @@ This restricts the search to constructions not defined in modules
 
 \end{Variants}
 
-\subsection{\tt SearchPattern {\term}.}\comindex{SearchPattern}
+\subsection[\tt SearchPattern {\term}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}}
 
 This command displays the name and type of all theorems of the current
 context whose statement's conclusion matches the expression {\term}
@@ -258,7 +252,7 @@ This restricts the search to constructions not defined in modules
 
 \end{Variants}
 
-\subsection{\tt SearchRewrite {\term}.}\comindex{SearchRewrite}
+\subsection[\tt SearchRewrite {\term}.]{\tt SearchRewrite {\term}.\comindex{SearchRewrite}}
 
 This command displays the name and type of all theorems of the current
 context whose statement's conclusion is an equality of which one side matches
@@ -283,7 +277,7 @@ This restricts the search to constructions not defined in modules
 
 \end{Variants}
 
-% \subsection{\tt SearchIsos {\term}.}\comindex{SearchIsos}
+% \subsection[\tt SearchIsos {\term}.]{\tt SearchIsos {\term}.\comindex{SearchIsos}}
 % \label{searchisos}
 % \texttt{SearchIsos} searches terms by their type modulo isomorphism.
 % This command displays the full name of all constants, variables,
@@ -312,8 +306,8 @@ This restricts the search to constructions not defined in modules
 % For more informations about the exact working of this command, see
 % \cite{Del97}.
 
-\subsection{\tt Locate {\qualid}.}\comindex{Locate}
-\label{Locate}
+\subsection[\tt Locate {\qualid}.]{\tt Locate {\qualid}.\comindex{Locate}
+\label{Locate}}
 This command displays the full name of the qualified identifier {\qualid}
 and consequently the \Coq\ module in which it is defined.
 
@@ -373,22 +367,19 @@ This command opens a browser window and displays the result of seeking
 for all statements that match the pattern {\pattern}. Holes in the
 pattern are represented by the wildcard character ``\_''.
 
-\subsubsection{\tt Whelp Instance {\pattern}.}
-\comindex{Whelp Instance}
+\subsubsection[\tt Whelp Instance {\pattern}.]{\tt Whelp Instance {\pattern}.\comindex{Whelp Instance}}
 
 This command opens a browser window and displays the result of seeking
 for all statements that are instances of the pattern {\pattern}. The
 pattern is here assumed to be an universally quantified expression.
 
-\subsubsection{\tt Whelp Elim {\qualid}.}
-\comindex{Whelp Elim}
+\subsubsection[\tt Whelp Elim {\qualid}.]{\tt Whelp Elim {\qualid}.\comindex{Whelp Elim}}
 
 This command opens a browser window and displays the result of seeking
 for all statements that have the ``form'' of an elimination scheme
 over the type denoted by {\qualid}.
 
-\subsubsection{\tt Whelp Hint {\term}.}
-\comindex{Whelp Hint}
+\subsubsection[\tt Whelp Hint {\term}.]{\tt Whelp Hint {\term}.\comindex{Whelp Hint}}
 
 This command opens a browser window and displays the result of seeking
 for all statements that can be instantiated so that to prove the
@@ -410,8 +401,7 @@ for \Coq's toplevel. This kind of file is called a {\em script} for
 \Coq\index{Script file}. The standard (and default) extension of
 \Coq's script files is {\tt .v}.
 
-\subsection{\tt Load {\ident}.}
-\comindex{Load}\label{Load}
+\subsection[\tt Load {\ident}.]{\tt Load {\ident}.\comindex{Load}\label{Load}}
 This command loads the file named {\ident}{\tt .v}, searching
 successively in each of the directories specified in the {\em
   loadpath}. (see section \ref{loadpath})
@@ -435,7 +425,7 @@ successively in each of the directories specified in the {\em
 \item \errindex{Can't find file {\ident} on loadpath}
 \end{ErrMsgs}
 
-\section{Compiled files}\label{compiled}\index{Compiled files}
+\section[Compiled files]{Compiled files\label{compiled}\index{Compiled files}}
 
 This feature allows to build files for a quick loading. When loaded,
 the commands contained in a compiled file will not be {\em replayed}.
@@ -498,7 +488,7 @@ waste of time.
 % \SeeAlso sections \ref{Opaque}, \ref{loadpath}, chapter
 % \ref{Addoc-coqc}
 
-%\subsection{\tt Import {\qualid}.}\comindex{Import}
+%\subsection[\tt Import {\qualid}.]{\tt Import {\qualid}.\comindex{Import}}
 %\label{Import}
 
 %%%%%%%%%%%%
@@ -507,9 +497,8 @@ waste of time.
 % the treatment of normal modules and libraries by Export omitted
 
 
-\subsection{\tt Require {\dirpath}.}
-\label{Require}
-\comindex{Require}
+\subsection[\tt Require {\dirpath}.]{\tt Require {\dirpath}.\label{Require}
+\comindex{Require}}
 
 This command looks in the loadpath for a file containing module
 {\dirpath}, then loads and opens (imports) its contents.
@@ -574,13 +563,11 @@ These different variants can be combined.
 
 \SeeAlso chapter \ref{Addoc-coqc}
 
-\subsection{\tt Print Modules.}
-\comindex{Print Modules}
+\subsection[\tt Print Modules.]{\tt Print Modules.\comindex{Print Modules}}
 This command shows the currently loaded and currently opened
 (imported) modules.
 
-\subsection{\tt Declare ML Module {\str$_1$} .. {\str$_n$}.}
-\comindex{Declare ML Module}
+\subsection[\tt Declare ML Module {\str$_1$} .. {\str$_n$}.]{\tt Declare ML Module {\str$_1$} .. {\str$_n$}.\comindex{Declare ML Module}}
 This commands loads the Objective Caml compiled files {\str$_1$} \dots
 {\str$_n$} (dynamic link). It is mainly used to load tactics
 dynamically.
@@ -597,23 +584,22 @@ files is only possible under the bytecode version of {\tt coqtop}
 \item \errindex{Loading of ML object file forbidden in a native Coq}
 \end{ErrMsgs}
 
-\subsection{\tt Print ML Modules.}\comindex{Print ML Modules}
+\subsection[\tt Print ML Modules.]{\tt Print ML Modules.\comindex{Print ML Modules}}
 This print the name of all \ocaml{} modules loaded with \texttt{Declare
   ML Module}. To know from where these module were loaded, the user
 should use the command \texttt{Locate File} (see page \pageref{Locate File})
 
-\section{Loadpath}
-\label{loadpath}\index{Loadpath}
+\section[Loadpath]{Loadpath\label{loadpath}\index{Loadpath}}
 
 There are currently two loadpaths in \Coq. A loadpath where seeking
 {\Coq} files (extensions {\tt .v} or {\tt .vo} or {\tt .vi}) and one where
 seeking Objective Caml files. The default loadpath contains the
 directory ``\texttt{.}'' denoting the current directory and mapped to the empty logical path (see section \ref{LongNames}).
 
-\subsection{\tt Pwd.}\comindex{Pwd}\label{Pwd}
+\subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}}
 This command displays the current working directory.
 
-\subsection{\tt Cd {\str}.}\comindex{Cd}
+\subsection[\tt Cd {\str}.]{\tt Cd {\str}.\comindex{Cd}}
 This command changes the current directory according to {\str} 
 which can be any valid path.
 
@@ -622,8 +608,7 @@ which can be any valid path.
   Is equivalent to {\tt Pwd.}
 \end{Variants}
 
-\subsection{\tt Add LoadPath {\str} as {\dirpath}.}
-\comindex{Add LoadPath}\label{AddLoadPath}
+\subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}}
 
 This command adds the path {\str} to the current {\Coq} loadpath and
 maps it to the logical directory {\dirpath}, which means that every
@@ -637,7 +622,7 @@ through logical name ``{\dirpath}{\tt{.M}}''.
 Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory path.
 \end{Variants}
 
-\subsection{\tt Add Rec LoadPath {\str} as {\dirpath}.}\comindex{Add Rec LoadPath}\label{AddRecLoadPath}
+\subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}}
 This command adds the directory {\str} and all its subdirectories 
 to the current \Coq\ loadpath. The top directory {\str} is mapped to the logical directory {\dirpath} while any subdirectory {\textsl{pdir}} is mapped to logical directory {\dirpath}{\tt{.pdir}} and so on.
 
@@ -648,47 +633,45 @@ to the current \Coq\ loadpath. The top directory {\str} is mapped to the logical
 Works as {\tt Add Rec LoadPath {\str} as {\dirpath}} but for the empty logical directory path.
 \end{Variants}
 
-\subsection{\tt Remove LoadPath {\str}.}\comindex{Remove LoadPath}
+\subsection[\tt Remove LoadPath {\str}.]{\tt Remove LoadPath {\str}.\comindex{Remove LoadPath}}
 This command removes the path {\str} from the current \Coq\ loadpath.
 
-\subsection{\tt Print LoadPath.}\comindex{Print LoadPath}
+\subsection[\tt Print LoadPath.]{\tt Print LoadPath.\comindex{Print LoadPath}}
 This command displays the current \Coq\ loadpath.
 
-\subsection{\tt Add ML Path {\str}.}\comindex{Add ML Path}
+\subsection[\tt Add ML Path {\str}.]{\tt Add ML Path {\str}.\comindex{Add ML Path}}
 This command adds the path {\str} to the current Objective Caml loadpath (see
 the command {\tt Declare ML Module} in the section \ref{compiled}).
 
 \Rem This command is implied by {\tt Add LoadPath {\str} as {\dirpath}}.
 
-\subsection{\tt Add Rec ML Path {\str}.}\comindex{Add Rec ML Path}
+\subsection[\tt Add Rec ML Path {\str}.]{\tt Add Rec ML Path {\str}.\comindex{Add Rec ML Path}}
 This command adds the directory {\str} and all its subdirectories 
 to the current Objective Caml loadpath (see
 the command {\tt Declare ML Module} in the section \ref{compiled}).
 
 \Rem This command is implied by {\tt Add Rec LoadPath {\str} as {\dirpath}}.
 
-\subsection{\tt Print ML Path {\str}.}\comindex{Print ML Path}
+\subsection[\tt Print ML Path {\str}.]{\tt Print ML Path {\str}.\comindex{Print ML Path}}
 This command displays the current Objective Caml loadpath.
 This command makes sense only under the bytecode version of {\tt
 coqtop}, i.e. using option {\tt -byte} (see the
 command {\tt Declare ML Module} in the section
 \ref{compiled}).
 
-\subsection{\tt Locate File {\str}.}\comindex{Locate
-  File}\label{Locate File}
+\subsection[\tt Locate File {\str}.]{\tt Locate File {\str}.\comindex{Locate
+  File}\label{Locate File}}
 This command displays the location of file {\str} in the current loadpath.
 Typically, {\str} is a \texttt{.cmo} or \texttt{.vo} or \texttt{.v} file.
 
-\subsection{\tt Locate Library {\dirpath}.}
-\comindex{Locate Library}
+\subsection[\tt Locate Library {\dirpath}.]{\tt Locate Library {\dirpath}.\comindex{Locate Library}}
 This command gives the status of the \Coq\ module {\dirpath}. It tells if the
 module is loaded and if not searches in the load path for a module
 of logical name {\dirpath}.
 
 \section{States and Reset}
 
-\subsection{\tt Reset \ident.}
-\comindex{Reset}
+\subsection[\tt Reset \ident.]{\tt Reset \ident.\comindex{Reset}}
 This command removes all the objects in the environment since \ident\ 
 was introduced, including \ident. \ident\ may be the name of a defined
 or declared object as well as the name of a section.  One cannot reset
@@ -698,8 +681,7 @@ over the name of a module or of an object inside a module.
 \item \ident: \errindex{no such entry}
 \end{ErrMsgs}
 
-\subsection{\tt Back.}
-\comindex{Back}
+\subsection[\tt Back.]{\tt Back.\comindex{Back}}
 
 This commands undoes all the effects of the last vernacular
 command. This does not include commands that only access to the
@@ -718,8 +700,7 @@ file are considered as a single command.
   Happens when there is vernacular command to undo.
 \end{ErrMsgs}
 
-\subsection{\tt Restore State \str.}
-\comindex{Restore State}
+\subsection[\tt Restore State \str.]{\tt Restore State \str.\comindex{Restore State}}
   Restores the state contained in the file \str.
 
 \begin{Variants}
@@ -731,8 +712,7 @@ file are considered as a single command.
   interactively.
 \end{Variants}
 
-\subsection{\tt Write State \str.}
-\comindex{Write State}
+\subsection[\tt Write State \str.]{\tt Write State \str.\comindex{Write State}}
 Writes the current state into a file \str{} for
 use in a further session. This file can be given as the {\tt
   inputstate} argument of the commands {\tt coqtop} and {\tt coqc}.
@@ -745,10 +725,10 @@ use in a further session. This file can be given as the {\tt
 
 \section{Quitting and debugging}
 
-\subsection{\tt Quit.}\comindex{Quit}
+\subsection[\tt Quit.]{\tt Quit.\comindex{Quit}}
 This command permits to quit \Coq.
 
-\subsection{\tt Drop.}\comindex{Drop}\label{Drop}
+\subsection[\tt Drop.]{\tt Drop.\comindex{Drop}\label{Drop}}
 
 This is used mostly as a debug facility by \Coq's implementors
 and does not concern the casual user.
@@ -782,44 +762,43 @@ go();;
   environment variable \texttt{COQTOP} to the root of your copy of the sources (see section \ref{EnvVariables}).
 \end{Warnings}
 
-\subsection{\tt Time \textrm{\textsl{command}}.}\comindex{Time}
-\label{time}
+\subsection[\tt Time \textrm{\textsl{command}}.]{\tt Time \textrm{\textsl{command}}.\comindex{Time}
+\label{time}}
 This command executes the vernac command \textrm{\textsl{command}}
 and display the time needed to execute it.
 
 \section{Controlling display}
 
-\subsection{\tt Set Silent.}
-\comindex{Begin Silent}
+\subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Begin Silent}
 \label{Begin-Silent}
-\index{Silent mode}
+\index{Silent mode}}
 This command turns off the normal displaying.
 
-\subsection{\tt Unset Silent.}\comindex{End Silent}
+\subsection[\tt Unset Silent.]{\tt Unset Silent.\comindex{End Silent}}
 This command turns the normal display on.
 
-\subsection{\tt Set Printing Width {\integer}.}\comindex{Set Printing Width}
+\subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\comindex{Set Printing Width}}
 This command sets which left-aligned part of the width of the screen
 is used for display. 
 
-\subsection{\tt Unset Printing Width.}\comindex{Unset Printing Width}
+\subsection[\tt Unset Printing Width.]{\tt Unset Printing Width.\comindex{Unset Printing Width}}
 This command resets the width of the screen used for display to its
 default value (which is 78 at the time of writing this documentation).
 
-\subsection{\tt Test Printing Width.}\comindex{Test Printing Width}
+\subsection[\tt Test Printing Width.]{\tt Test Printing Width.\comindex{Test Printing Width}}
 This command displays the current screen width used for display.
 
-\subsection{\tt Set Printing Depth {\integer}.}\comindex{Set Printing Depth}
+\subsection[\tt Set Printing Depth {\integer}.]{\tt Set Printing Depth {\integer}.\comindex{Set Printing Depth}}
 This command sets the nesting depth of the formatter used for
 pretty-printing. Beyond this depth, display of subterms is replaced by
 dots. 
 
-\subsection{\tt Unset Printing Depth.}\comindex{Unset Printing Depth}
+\subsection[\tt Unset Printing Depth.]{\tt Unset Printing Depth.\comindex{Unset Printing Depth}}
 This command resets the nesting depth of the formatter used for
 pretty-printing to its default value (at the
 time of writing this documentation, the default value is 50).
 
-\subsection{\tt Test Printing Depth.}\comindex{Test Printing Depth}
+\subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\comindex{Test Printing Depth}}
 This command displays the current nesting depth used for display.
 
 %\subsection{\tt Explain ...}
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index a8b7e5459a..8aec7cd1cc 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -1,6 +1,5 @@
-\chapter{Proof handling}
-\index{Proof editing}
-\label{Proof-handling}
+\chapter[Proof handling]{Proof handling\index{Proof editing}
+\label{Proof-handling}}
 
 In \Coq's proof editing mode all top-level commands documented in 
 chapter \ref{Vernacular-commands} remain available
@@ -41,8 +40,7 @@ proof editing mode, \Coq~ raises the error message : \errindex{No focused
 
 \section{Switching on/off the proof editing mode}
 
-\subsection{\tt Goal {\form}.}
-\comindex{Goal}\label{Goal}
+\subsection[\tt Goal {\form}.]{\tt Goal {\form}.\comindex{Goal}\label{Goal}}
 This command switches \Coq~ to editing proof mode and sets {\form} as
 the original goal. It associates the name {\tt Unnamed\_thm} to
 that goal.
@@ -58,7 +56,7 @@ that goal.
 
 \SeeAlso section \ref{Theorem}
 
-\subsection{\tt Qed.}\comindex{Qed}\label{Qed}
+\subsection[\tt Qed.]{\tt Qed.\comindex{Qed}\label{Qed}}
 This command is available in interactive editing proof mode when the
 proof is completed.  Then {\tt Qed} extracts a proof term from the
 proof script, switches back to {\Coq} top-level and attaches the
@@ -107,13 +105,12 @@ memory overflow.
   Are equivalent to {\tt Save {\ident}.} 
 \end{Variants}
 
-\subsection{\tt Admitted.}\comindex{Admitted}\label{Admitted}
+\subsection[\tt Admitted.]{\tt Admitted.\comindex{Admitted}\label{Admitted}}
 This command is available in interactive editing proof mode to give up
 the current proof and declare the initial goal as an axiom.
 
-\subsection{\tt Theorem {\ident} : {\form}.}
-\comindex{Theorem}
-\label{Theorem}
+\subsection[\tt Theorem {\ident} : {\form}.]{\tt Theorem {\ident} : {\form}.\comindex{Theorem}
+\label{Theorem}}
 
 This command switches to interactive editing proof mode and declares
 {\ident} as being the name of the original goal {\form}. When declared
@@ -163,9 +160,8 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels:
   current section.
 \end{Variants}
 
-\subsection{\tt Proof {\term}.}
-\comindex{Proof}
-\label{BeginProof}
+\subsection[\tt Proof {\term}.]{\tt Proof {\term}.\comindex{Proof}
+\label{BeginProof}}
 This command applies in proof editing mode. It is equivalent to {\tt
   exact {\term}; Save.} That is, you have to give the full proof in
 one gulp, as a proof term (see section \ref{exact}).
@@ -179,8 +175,7 @@ one gulp, as a proof term (see section \ref{exact}).
 
 \SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}.
 
-\subsection{\tt Abort.}
-\comindex{Abort}
+\subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
 This command cancels the current proof development, switching back to
 the previous proof development, or to the \Coq\ toplevel if no other
@@ -202,14 +197,12 @@ proof was edited.
 
 \end{Variants}
 
-\subsection{\tt Suspend.}
-\comindex{Suspend}
+\subsection[\tt Suspend.]{\tt Suspend.\comindex{Suspend}}
 
 This command applies in proof editing mode. It switches back to the
 \Coq\ toplevel, but without canceling the current proofs.
 
-\subsection{\tt Resume.}
-\comindex{Resume}\label{Resume}
+\subsection[\tt Resume.]{\tt Resume.\comindex{Resume}\label{Resume}}
 
 This commands switches back to the editing of the last edited proof.
 
@@ -232,8 +225,7 @@ This commands switches back to the editing of the last edited proof.
 
 \section{Navigation in the proof tree}
 
-\subsection{\tt Undo.}
-\comindex{Undo}
+\subsection[\tt Undo.]{\tt Undo.\comindex{Undo}}
 
 This command cancels the effect of the last tactic command.  Thus, it
 backtracks one step.
@@ -251,28 +243,26 @@ backtracks one step.
 
 \end{Variants}
 
-\subsection{\tt Set Undo {\num}.}
-\comindex{Set Undo}
+\subsection[\tt Set Undo {\num}.]{\tt Set Undo {\num}.\comindex{Set Undo}}
 
 This command changes the maximum number of {\tt Undo}'s that will be
 possible when doing a proof. It only affects proofs started after
 this command, such that if you want to change the current undo limit
 inside a proof, you should first restart this proof.
 
-\subsection{\tt Unset Undo.}
-\comindex{Unset Undo}
+\subsection[\tt Unset Undo.]{\tt Unset Undo.\comindex{Unset Undo}}
 
 This command resets the default number of possible {\tt Undo} commands
 (which is currently 12).
 
-\subsection{\tt Restart.}\comindex{Restart}
+\subsection[\tt Restart.]{\tt Restart.\comindex{Restart}}
 This command restores the proof editing process to the original goal.
 
 \begin{ErrMsgs}
 \item \errindex{No focused proof to restart}
 \end{ErrMsgs}
 
-\subsection{\tt Focus.}\comindex{Focus}
+\subsection[\tt Focus.]{\tt Focus.\comindex{Focus}}
 This focuses the attention on the first subgoal to prove and the printing
 of the other subgoals is suspended until the focused subgoal is
 solved or unfocused. This is useful when there are many current
@@ -284,13 +274,13 @@ This focuses the attention on the $\num^{\scriptsize th}$ subgoal to prove.
 
 \end{Variant}
 
-\subsection{\tt Unfocus.}\comindex{Unfocus}
+\subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}}
 Turns off the focus mode.
 
 
 \section{Displaying information}
 
-\subsection{\tt Show.}\comindex{Show}\label{Show}
+\subsection[\tt Show.]{\tt Show.\comindex{Show}\label{Show}}
 This command displays the current goals.
 
 \begin{Variants}
@@ -363,14 +353,12 @@ process of an {\tt Intros}.
 
 \end{Variants}
 
-\subsection{\tt Set Hyps Limit {\num}.}
-\comindex{Set Hyps Limit}
+\subsection[\tt Set Hyps Limit {\num}.]{\tt Set Hyps Limit {\num}.\comindex{Set Hyps Limit}}
 This command sets the maximum number of hypotheses displayed in
 goals after the application of a tactic. 
 All the hypotheses remains usable in the proof development.
 
-\subsection{\tt Unset Hyps Limit.}
-\comindex{Unset Hyps Limit}
+\subsection[\tt Unset Hyps Limit.]{\tt Unset Hyps Limit.\comindex{Unset Hyps Limit}}
 This command goes back to the default mode which is to print all
 available hypotheses.
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index ae2b1eda2f..9bde8c490c 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -1,5 +1,4 @@
-\chapter{Syntax extensions and interpretation scopes}
-\label{Addoc-syntax}
+\chapter[Syntax extensions and interpretation scopes]{Syntax extensions and interpretation scopes\label{Addoc-syntax}}
 
 In this chapter, we introduce advanced commands to modify the way
 {\Coq} parses and prints objects, i.e. the translations between the
@@ -16,9 +15,8 @@ version 8.0. The underlying AST structure is also no longer available.
 The functionalities of the command {\tt Syntactic Definition} are
 still available, see section \ref{Abbreviations}.
 
-\section{Notations}
-\label{Notation}
-\comindex{Notation}
+\section[Notations]{Notations\label{Notation}
+\comindex{Notation}}
 
 \subsection{Basic notations}
 
@@ -61,9 +59,8 @@ and pretty-printer of {\Coq} already know how to deal with the
 syntactic expression (see \ref{ReservedNotation}), explicit precedences and
 associativity rules have to be given.
 
-\subsection{Precedences and associativity}
-\index{Precedences}
-\index{Associativity}
+\subsection[Precedences and associativity]{Precedences and associativity\index{Precedences}
+\index{Associativity}}
 
 Mixing different symbolic notations in a same text may cause serious
 parsing ambiguity. To deal with the ambiguity of notations, {\Coq}
@@ -631,9 +628,8 @@ Notations do not survive the end of sections. They survive modules
 unless the command {\tt Notation Local} is used instead of {\tt
 Notation}.
 
-\section{Interpretation scopes}
-\index{Interpretation scopes}
-\label{scopes}
+\section[Interpretation scopes]{Interpretation scopes\index{Interpretation scopes}
+\label{scopes}}
 % Introduction
 
 An {\em interpretation scope} is a set of notations for terms with
@@ -788,8 +784,7 @@ interpretation. See the next section.
 \SeeAlso The command to show the scopes bound to the arguments of a
 function is described in section \ref{About}.
 
-\subsection{The {\tt type\_scope} interpretation scope}
-\index{type\_scope}
+\subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope}}
 
 The scope {\tt type\_scope} has a special status. It is a primitive
 interpretation scope which is temporarily activated each time a
@@ -929,10 +924,9 @@ This displays all the notations, delimiting keys and corresponding
 class of all the existing interpretation scopes.
 It also displays the lonely notations.
 
-\section{Abbreviations}
-\index{Abbreviations}
+\section[Abbreviations]{Abbreviations\index{Abbreviations}
 \label{Abbreviations}
-\comindex{Notation}
+\comindex{Notation}}
 
 An {\em abbreviation} is a name denoting a (presumably) more complex
 expression. An abbreviation is a special form of notation with no
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 63f61ea8bb..2403c07a6d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -824,13 +824,14 @@ performs the conversion in hypotheses $H_1\ldots H_n$.
 %voir reduction__conv_x : histoires d'univers.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$
+\subsection[{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$
+\dots\ \flag$_n$} and {\tt compute}]
+{{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$
 \dots\ \flag$_n$} and {\tt compute}
 \tacindex{cbv}
 \tacindex{lazy}
 \tacindex{compute}
-\tacindex{vm\_compute}}
-\label{vmcompute}
+\tacindex{vm\_compute}\label{vmcompute}}
 
 These parameterized reduction tactics apply to any goal and perform
 the normalization of the goal according to the specified flags. Since
@@ -1146,8 +1147,7 @@ equivalent to {\tt intros; apply ci}.
 
 \end{Variants}
 
-\section{Eliminations (Induction and Case Analysis)}
-\label{Tac-induction}
+\section[Eliminations (Induction and Case Analysis)]{Eliminations (Induction and Case Analysis)\label{Tac-induction}}
 Elimination tactics are useful to prove statements by induction or
 case analysis.  Indeed, they make use of the elimination (or
 induction) principles generated with inductive definitions (see
@@ -1471,10 +1471,10 @@ exact c.
 Qed.
 \end{coq_example}
 
-%\subsection{\tt FixPoint \dots}\tacindex{Fixpoint}
+%\subsection[\tt FixPoint \dots]{\tt FixPoint \dots\tacindex{Fixpoint}}
 %Not yet documented.
 
-\subsection {\tt double induction \ident$_1$ \ident$_2$
+\subsection{\tt double induction \ident$_1$ \ident$_2$
 \tacindex{double induction}}
 
 This tactic applies to any goal. If the variables {\ident$_1$} and
@@ -1782,8 +1782,7 @@ When several hypotheses have the form {\tt \ident=t} or {\tt
     for which an equality exists.
 \end{Variants}
 
-\subsection{{\tt stepl {\term}}}
-\tacindex{stepl}
+\subsection[{\tt stepl {\term}}]{{\tt stepl {\term}}\tacindex{stepl}}
 
 This tactic is for chaining rewriting steps. It assumes a goal of the
 form ``$R$ {\term}$_1$ {\term}$_2$'' where $R$ is a binary relation
@@ -1853,7 +1852,7 @@ of an inductive datatype. If $G$ is the current goal, it leaves the sub-goals
 of \term$_1$ and \term$_2$ must satisfy the same restrictions as in the tactic
 \texttt{decide equality}.
 
-\subsection {\tt discriminate {\ident}
+\subsection{\tt discriminate {\ident}
 \label{discriminate}
 \tacindex{discriminate}}
 
@@ -2272,8 +2271,7 @@ the instance with the tactic {\tt inversion}.
 
 
 
-\subsection{\tt functional inversion \ident}
-\label{sec:functional-inversion}
+\subsection[\tt functional inversion \ident]{\tt functional inversion \ident\label{sec:functional-inversion}}
 
 \texttt{functional inversion} is a \emph{highly} experimental tactic
 which performs inversion on hypothesis \ident\ of the form
@@ -2331,8 +2329,7 @@ datatype: see~\ref{quote-examples} for the full details.
 % En attente d'un moyen de valoriser les fichiers de demos
 % \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} in the distribution
 
-\section{Classical tactics}
-\label{ClassicalTactics}
+\section[Classical tactics]{Classical tactics\label{ClassicalTactics}}
 
 In order to ease the proving process, when the {\tt Classical} module is loaded. A few more tactics are available. Make sure to load the module using the \texttt{Require Import} command.
 
@@ -2631,7 +2628,7 @@ vernacular command.
 %% \end{ErrMsgs}
 
 
-% \subsection{\tt Linear}\tacindex{Linear}\label{Linear}
+% \subsection[\tt Linear]{\tt Linear\tacindex{Linear}\label{Linear}}
 % The tactic \texttt{Linear}, due to Jean-Christophe Filli{\^a}atre
 % \cite{Fil94}, implements a decision procedure for {\em Direct
 %   Predicate Calculus}, that is first-order Gentzen's Sequent Calculus
@@ -3258,9 +3255,8 @@ e.g. \texttt{Require Import A.}).
 
 \subsection{Setting implicit automation tactics}
 
-\subsubsection{\tt Proof with {\tac}.}
-\label{ProofWith}
-\comindex{Proof with}
+\subsubsection[\tt Proof with {\tac}.]{\tt Proof with {\tac}.\label{ProofWith}
+\comindex{Proof with}}
 
   This command may be used to start a proof. It defines a default
   tactic to be used each time a tactic command {\tac$_1$} is ended by
@@ -3269,8 +3265,7 @@ e.g. \texttt{Require Import A.}).
 
 \SeeAlso {\tt Proof.} in section~\ref{BeginProof}.
 
-\subsubsection{\tt Declare Implicit Tactic {\tac}.}
-\comindex{Declare Implicit Tactic}
+\subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}}
 
 This command declares a tactic to be used to solve implicit arguments
 that {\Coq} does not know how to solve by unification. It is used
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 8cb7a4807b..951de0cd72 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -1,12 +1,10 @@
-\chapter{Detailed examples of tactics}
-\label{Tactics-examples}
+\chapter[Detailed examples of tactics]{Detailed examples of tactics\label{Tactics-examples}}
 
 This chapter presents detailed examples of certain tactics, to
 illustrate their behavior.
 
-\section{\tt refine}
-\tacindex{refine}
-\label{refine-example}
+\section[\tt refine]{\tt refine\tacindex{refine}
+\label{refine-example}}
 
 This tactic applies to any goal. It behaves like {\tt exact} with a
 big difference : the user can leave some holes (denoted by \texttt{\_} or 
@@ -101,9 +99,8 @@ Defined.
 % Abort.
 % \end{coq_eval}
 
-\section{\tt eapply}
-\tacindex{eapply}
-\label{eapply-example}
+\section[\tt eapply]{\tt eapply\tacindex{eapply}
+\label{eapply-example}}
 \Example
 Assume we have a relation on {\tt nat} which is transitive:
 
@@ -193,9 +190,8 @@ apply Rmp.
 Reset R.
 \end{coq_eval}
 
-\section{{\tt Scheme}}
-\comindex{Scheme}
-\label{Scheme-examples}
+\section[{\tt Scheme}]{{\tt Scheme}\comindex{Scheme}
+\label{Scheme-examples}}
 
 \firstexample
 \example{Induction scheme for \texttt{tree} and \texttt{forest}}
@@ -271,9 +267,8 @@ Check odd_even.
 The type of {\tt even\_odd} shares the same premises but the
 conclusion is {\tt (n:nat)(even n)->(Q n)}.
 
-\subsection{{\tt Combined Scheme}}
-\comindex{Combined Scheme}
-\label{CombinedScheme-examples}
+\subsection[{\tt Combined Scheme}]{{\tt Combined Scheme}\comindex{Combined Scheme}
+\label{CombinedScheme-examples}}
 
 We can define the induction principles for trees and forests using:
 \begin{coq_example}
@@ -291,9 +286,8 @@ The type of {\tt tree\_forest\_mutrec} will be:
 Check tree_forest_mutind.
 \end{coq_example}
 
-\section{{\tt Functional Scheme} and {\tt functional induction}}
-\comindex{Functional Scheme}\tacindex{functional induction}
-\label{FunScheme-examples}
+\section[{\tt Functional Scheme} and {\tt functional induction}]{{\tt Functional Scheme} and {\tt functional induction}\comindex{Functional Scheme}\tacindex{functional induction}
+\label{FunScheme-examples}}
 
 \firstexample
 \example{Induction scheme for \texttt{div2}}
@@ -433,9 +427,8 @@ Check tree_size_ind2.
 
 
 
-\section{{\tt inversion}}
-\tacindex{inversion}
-\label{inversion-examples}
+\section[{\tt inversion}]{{\tt inversion}\tacindex{inversion}
+\label{inversion-examples}}
 
 \subsection*{Generalities about inversion}
 
@@ -593,8 +586,7 @@ inversion H using leminv.
 Reset Initial.
 \end{coq_eval}
 
-\section{\tt autorewrite}
-\label{autorewrite-example}
+\section[\tt autorewrite]{\tt autorewrite\label{autorewrite-example}}
 
 Here are two examples of {\tt autorewrite} use. The first one ({\em Ackermann
 function}) shows actually a quite basic use where there is no conditional
@@ -666,9 +658,8 @@ autorewrite with base1 using reflexivity || simpl.
 Reset Initial.
 \end{coq_eval}
 
-\section{\tt quote}
-\tacindex{quote}
-\label{quote-examples}
+\section[\tt quote]{\tt quote\tacindex{quote}
+\label{quote-examples}}
 
 The tactic \texttt{quote} allows to use Barendregt's so-called
 2-level approach without writing any ML code. Suppose you have a
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index 8be5c9635c..9b3745a0b6 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -9,8 +9,7 @@
 %\tableofcontents
 %\clearpage
 
-\chapter{Writing ad-hoc Tactics in Coq}
-\label{WritingTactics}
+\chapter[Writing ad-hoc Tactics in Coq]{Writing ad-hoc Tactics in Coq\label{WritingTactics}}
 
 \section{Introduction}
 
@@ -274,8 +273,7 @@ most important functions, which are sufficient to implement a large
 class of tactics.
 
 
-\subsection{The Logical Framework}
-\label{LogicalFramework}
+\subsection[The Logical Framework]{The Logical Framework\label{LogicalFramework}}
 
 At the very heart of \Coq there is a generic untyped language for
 expressing abstractions, applications and global constants. This
@@ -398,8 +396,7 @@ The following operations can be used for handling names:
     generates an identifier from the given string.}
 \end{description}
 
-\paragraph{Section paths.} 
-\label{SectionPaths}
+\paragraph[Section paths.]{Section paths.\label{SectionPaths}}
 A \textsl{section-path} is a global name to refer to an object without
 ambiguity.  It can be seen as a sort of filename, where open sections
 play the role of directories. Each section path is formed by three
@@ -645,8 +642,7 @@ information:
     the $ith$ type is recursive, and \texttt{Norec} if it is not.}.
 \end{description}
 
-\subsection{The Type Checker}
-\label{TypeChecker}
+\subsection[The Type Checker]{The Type Checker\label{TypeChecker}}
 
 The third logical module is the type checker. It concentrates two main
 tasks concerning the language of constructions.
@@ -723,8 +719,7 @@ generate it or the machinery of the proof engine, but only on the
 type-checker. In other words, extending the system with a potentially
 bugged new tactic never endangers the consistency of the system.
 
-\subsubsection{What is a Tactic?}
-\label{WhatIsATactic}
+\subsubsection[What is a Tactic?]{What is a Tactic?\label{WhatIsATactic}}
 %Let us now explain what is a tactic, and how the user can introduce
 %new ones. 
 
@@ -871,8 +866,7 @@ val Auto.trivial            : tactic
 The functions hiding the implementation of these tactics are defined
 in the module \texttt{Hiddentac}. Their names are prefixed by ``h\_''.
 
-\subsubsection{Tacticals}
-\label{OcamlTacticals}
+\subsubsection[Tacticals]{Tacticals\label{OcamlTacticals}}
 
 The following tacticals can be used to combine already existing
 tactics:
@@ -949,8 +943,7 @@ expressions from the \gallina{} language (definitions), general
 directives (setting commands) or tactics to be applied by the proof
 engine. 
 
-\subsection{The Parser and the Pretty-Printer}
-\label{PrettyPrinter}
+\subsection[The Parser and the Pretty-Printer]{The Parser and the Pretty-Printer\label{PrettyPrinter}}
 
 The last logical module is the parser and pretty printer of \Coq,
 which is the interface between the vernacular interpreter and the
@@ -1196,8 +1189,7 @@ for example
 \verb+tactics/contrib/polynom/ring.ml+ or 
 \verb+tactics/contrib/polynom/coq_omega.ml+.
 
-\section{Some Useful Tools for Writing Tactics}
-\label{SomeUsefulToolsforWrittingTactics}
+\section[Some Useful Tools for Writing Tactics]{Some Useful Tools for Writing Tactics\label{SomeUsefulToolsforWrittingTactics}}
 When the implementation of a tactic is not a straightforward
 combination of tactics and tacticals, the module \texttt{Tacmach}
 provides several useful functions for handling goals, calling the
@@ -1250,8 +1242,7 @@ Tacmach.pf\_reduction\_of\_redexp  : \\
     {Test whether  two given terms are definitionally equal.}
 \end{description}
 
-\subsection{Patterns}
-\label{Patterns}
+\subsection[Patterns]{Patterns\label{Patterns}}
 
 The \ocaml{} file \texttt{Pattern} provides a quick way for describing a
 term pattern and performing second-order, binding-preserving, matching
@@ -1351,8 +1342,7 @@ They
     {\\ Similarly, but it performs case analysis instead of induction.}
 \end{description}
 
-\section{A Complete Example}
-\label{ACompleteExample}
+\section[A Complete Example]{A Complete Example\label{ACompleteExample}}
 
 In order to illustrate the implementation of a new tactic, let us come
 back to the problem of deciding the equality of two elements of an
@@ -1742,8 +1732,7 @@ Abort.
 Remark that the task performed by the tactic \texttt{solveRightBranch}
 is not displayed, since we have chosen to hide its implementation.
 
-\section{Testing and Debugging your Tactic}
-\label{test-and-debug}
+\section[Testing and Debugging your Tactic]{Testing and Debugging your Tactic\label{test-and-debug}}
 
 When your tactic does not behave as expected, it is possible to trace
 it dynamically from \Coq. In order to do this, you have first to leave
@@ -1786,8 +1775,7 @@ Finally, the traditional \ocaml{} debugging tools like the directives
 execution of your functions. Frequently, a better solution is to use
 the \ocaml{} debugger, see Chapter \ref{Utilities}.
 
-\section{Concrete syntax for ML tactic and vernacular command}
-\label{Notations-for-ML-command}
+\section[Concrete syntax for ML tactic and vernacular command]{Concrete syntax for ML tactic and vernacular command\label{Notations-for-ML-command}}
 
 \subsection{The general case}
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 8c4c5edb8a..8438a63373 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -1,10 +1,9 @@
-\chapter{Utilities}\label{Utilities}
+\chapter[Utilities]{Utilities\label{Utilities}}
 
 The distribution provides utilities to simplify some tedious works
 beside proof development, tactics writing or documentation.
 
-\section{Building a toplevel extended with user tactics}
-\label{Coqmktop}\index{Coqmktop@{\tt coqmktop}}
+\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\index{Coqmktop@{\tt coqmktop}}}
 
 The native-code version of \Coq\ cannot dynamically load user tactics
 using Objective Caml code. It is possible to build a toplevel of \Coq,
@@ -25,8 +24,7 @@ A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}),
 which can be generated by {\tt coqmktop -opt -o coqopt.opt}.
 
 
-\paragraph{Application: how to use the Objective Caml debugger with Coq.}
-\index{Debugger}
+\paragraph[Application: how to use the Objective Caml debugger with Coq.]{Application: how to use the Objective Caml debugger with Coq.\index{Debugger}}
 
 One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in
 order to debug your tactics with the Objective Caml debugger.
@@ -53,8 +51,8 @@ arguments. In other cases, the debugger is simply called without additional
 arguments. Such a wrapper can be found in the \texttt{dev/}
 subdirectory of the sources. 
 
-\section{Modules dependencies}\label{Dependencies}\index{Dependencies}
-  \index{Coqdep@{\tt coqdep}}
+\section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies}
+  \index{Coqdep@{\tt coqdep}}}
 
 In order to compute modules dependencies (so to use {\tt make}),
 \Coq\ comes with an appropriate tool, {\tt coqdep}.
@@ -76,10 +74,9 @@ instead for the \ocaml\ modules dependencies.
 See the man page of {\tt coqdep} for more details and options.
 
 
-\section{Creating a {\tt Makefile} for \Coq\ modules}
-\label{Makefile}
+\section[Creating a {\tt Makefile} for \Coq\ modules]{Creating a {\tt Makefile} for \Coq\ modules\label{Makefile}
 \index{Makefile@{\tt Makefile}}
-\index{CoqMakefile@{\tt coq\_Makefile}}
+\index{CoqMakefile@{\tt coq\_Makefile}}}
 
 When a proof development becomes large and is split into several files,
 it becomes crucial to use a tool like {\tt make} to compile \Coq\
@@ -166,9 +163,8 @@ the sources of \Coq{} somewhere and have an environment variable named
 % \end{description}
 
 
-\section{Documenting \Coq\ files with coqdoc}
-\label{coqdoc}
-\index{Coqdoc@{\sf coqdoc}}
+\section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc}
+\index{Coqdoc@{\sf coqdoc}}}
 
 \input{./coqdoc}
 
@@ -176,8 +172,8 @@ the sources of \Coq{} somewhere and have an environment variable named
 
 \input{./Helm}
 
-\section{Embedded \Coq\ phrases inside \LaTeX\ documents}\label{Latex}
-  \index{Coqtex@{\tt coq-tex}}\index{Latex@{\LaTeX}}
+\section[Embedded \Coq\ phrases inside \LaTeX\ documents]{Embedded \Coq\ phrases inside \LaTeX\ documents\label{Latex}
+  \index{Coqtex@{\tt coq-tex}}\index{Latex@{\LaTeX}}}
 
 When writing a documentation about a proof development, one may want
 to insert \Coq\ phrases inside a \LaTeX\ document, possibly together with
@@ -199,7 +195,7 @@ See the man page of {\tt coq-tex} for more details.
 have been completely produced with {\tt coq-tex}.
 
 
-\section{\Coq\ and \emacs}\label{Emacs}\index{Emacs}
+\section[\Coq\ and \emacs]{\Coq\ and \emacs\label{Emacs}\index{Emacs}}
 
 \subsection{The \Coq\ Emacs mode}
 
@@ -233,7 +229,7 @@ An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also
 included in the distribution, in file \texttt{coq-inferior.el}.
 Instructions to use it are contained in this file.
 
-\subsection{Proof General}\index{Proof General}
+\subsection[Proof General]{Proof General\index{Proof General}}
 
 Proof General is a generic interface for proof assistants based on
 Emacs (or XEmacs). The main idea is that the \Coq\ commands you are
@@ -247,7 +243,7 @@ Proof General is developped and distributed independently of the
 system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
 
 
-\section{Module specification}\label{gallina}\index{Gallina@{\tt gallina}}
+\section[Module specification]{Module specification\label{gallina}\index{Gallina@{\tt gallina}}}
 
 Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its
 specification (inductive types declarations, definitions, type of
@@ -258,7 +254,7 @@ file {\em file}{\tt.v} gives birth to the specification file
 See the man page of {\tt gallina} for more details and options.
 
 
-\section{Man pages}\label{ManPages}\index{Man pages}
+\section[Man pages]{Man pages\label{ManPages}\index{Man pages}}
 
 There are man pages for the commands {\tt coqdep}, {\tt gallina} and
 {\tt coq-tex}. Man pages are installed at installation time
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 62c640b23f..8f2c66e0cb 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -33,7 +33,7 @@
 \input{../common/title.tex}% extension .tex pour htmlgen
 %\input{headers}
 
-\usepackage[linktocpage,colorlinks]{hyperref}
+\usepackage[linktocpage,colorlinks,bookmarks=false]{hyperref}
 % The manual advises to load hyperref package last to be able to redefine
 % necessary commands.
 % The above should work for both latex and pdflatex. Even if PDF is produced
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index 48e91fcd28..63594a18f9 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -440,8 +440,7 @@ Default behavior is to assume ASCII 7 bits input files.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{The coqdoc \LaTeX{} style file}
-\label{section:coqdoc.sty}
+\subsection[The coqdoc \LaTeX{} style file]{The coqdoc \LaTeX{} style file\label{section:coqdoc.sty}}
 
 In case you choose to produce a document without the default \LaTeX{}
 preamble (by using option \verb|--no-preamble|), then you must insert