correction bugs commit precedent et mise en forme html

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

22 files changed, 1298 insertions, 1400 deletions

diff --git a/doc/Coercion.tex b/doc/Coercion.tex
index be496adb2..186a9be73 100644
--- a/doc/Coercion.tex
+++ b/doc/Coercion.tex
@@ -38,19 +38,18 @@ classes:
   type, i.e. of form $forall~ x:A, B$.
 \end{itemize}
 
-Formally, the syntax of a classes is defined by
-
-\medskip
-\begin{center}
-\begin{tabular}{|lcl|}
-\hline
+Formally, the syntax of a classes is defined on Figure~\ref{fig:classes}.
+\begin{figure}
+\begin{centerframe}
+\begin{tabular}{lcl}
 {\class} & ::= & {\qualid} \\
   & $|$ & {\tt Sortclass} \\
-  & $|$ & {\tt Funclass} \\
-\hline
+  & $|$ & {\tt Funclass} 
 \end{tabular}
-\end{center}
-\medskip
+\end{centerframe}
+\caption{Syntax of classes}
+\label{fig:classes}
+\end{figure}
 
 \asection{Coercions}
 \index{Coercions!Funclass}
diff --git a/doc/Library.tex b/doc/Library.tex
index 7483e602c..58b2dc6df 100755
--- a/doc/Library.tex
+++ b/doc/Library.tex
@@ -25,7 +25,6 @@ of this library). It provides a set of modules directly available
 through the \verb!Require! command.
 
 The standard library is composed of the following subdirectories:
-
 \medskip
 \begin{tabular}{lp{12cm}}
   {\bf Logic}   & Classical logic and dependent equality \\
diff --git a/doc/Makefile b/doc/Makefile
index 424a3d1be..f0a0c4c60 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -31,7 +31,7 @@ COQWEBSTY=/usr/share/texmf/tex/latex/misc/
 HEVEALIB=/usr/local/lib/hevea
 
 LATEX=latex
-BIBTEX=bibtex -min-crossref=10
+BIBTEX=bibtex -min-crossrefs=10
 MAKEINDEX=makeindex
 PDFLATEX=pdflatex
 
@@ -139,8 +139,9 @@ Changes.v.html: Changes.v.tex
 	hevea ./Changes.v.tex
 
 Reference-Manual.html: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib
-	hevea -fix ./book-html.sty ./coq-html.sty ./Reference-Manual.tex
+#1.05 ?	hevea -fix ./book-html.sty ./coq-html.sty ./Reference-Manual.tex
 #1.04	hevea ./book-html.sty ./coq-html.sty ./Reference-Manual.tex
+	hevea -fix -nosymb -exec xxdate.exe ./Reference-Manual.tex
 
 faq.v.html: faq.v.tex
 	hevea ./faq.v.tex
diff --git a/doc/Polynom.tex b/doc/Polynom.tex
index 37633d199..81947aad2 100644
--- a/doc/Polynom.tex
+++ b/doc/Polynom.tex
@@ -386,8 +386,7 @@ replace it by \verb|(interp v (polynomial_simplify ap))|, using the
 main correctness theorem and we reduce it to a concrete expression
 \texttt{p'}, which is the concrete normal form of
 \texttt{p}. This is summarized in this diagram:
-
-\medskip
+\begin{center}
 \begin{tabular}{rcl}
 \texttt{p} & $\rightarrow_{\beta\delta\iota}$  
    & \texttt{(interp v ap)} \\
@@ -396,8 +395,7 @@ main correctness theorem and we reduce it to a concrete expression
    & $\leftarrow_{\beta\delta\iota}$ 
    & \texttt{(interp v (polynomial\_simplify ap))}
 \end{tabular}
-\medskip
-
+\end{center}
 The user do not see the right part of the diagram. 
 From outside, the tactic behaves like a
 $\beta\delta\iota$ simplification extended with AC rewriting rules.
diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index d9a94bb72..87b55744a 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -285,9 +285,9 @@ $\Gamma$
 A term $t$ is well typed in an environment $E$ iff there exists a
 context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can
 be derived from the following rules.
-\begin{itemize}
-\item [W-E] \inference{\WF{[]}{[]}}
-\item [W-S]  % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma
+\begin{description}
+\item[W-E] \inference{\WF{[]}{[]}}
+\item[W-S]  % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma
 \inference{\frac{\WTEG{T}{s}~~~~s\in \Sort~~~~x \not\in
       \Gamma           % \cup E
       }
@@ -297,7 +297,7 @@ be derived from the following rules.
      }{\WFE{\Gamma::(x:=t:T)}}}
 \item[Def] \inference{\frac{\WTEG{t}{T}~~~c \notin E\cup \Gamma}
                       {\WF{E;\Def{\Gamma}{c}{t}{T}}{\Gamma}}}
-\item [Ax] \index{Typing rules!Ax}
+\item[Ax] \index{Typing rules!Ax}
 \inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(p)}}~~~~~
 \frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(q)}}}
 \inference{\frac{\WFE{\Gamma}~~~~i<j}{\WTEG{\Type(i)}{\Type(j)}}}
@@ -305,7 +305,7 @@ be derived from the following rules.
  \inference{\frac{ \WFE{\Gamma}~~~~~(x:T)\in\Gamma~~\mbox{or}~~(x:=t:T)\in\Gamma~\mbox{for some $t$}}{\WTEG{x}{T}}}
 \item[Const]  \index{Typing rules!Const}
 \inference{\frac{\WFE{\Gamma}~~~~(c:T) \in E}{\WTEG{c}{T}}}
-\item [Prod]  \index{Typing rules!Prod}
+\item[Prod]  \index{Typing rules!Prod}
 \inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~
     \WTE{\Gamma::(x:T)}{U}{\Prop}}
       { \WTEG{\forall~x:T,U}{\Prop}}} 
@@ -315,18 +315,18 @@ be derived from the following rules.
 \inference{\frac{\WTEG{T}{\Type(i)}~~~~i\leq k~~~
     \WTE{\Gamma::(x:T)}{U}{\Type(j)}~~~j \leq k}
     {\WTEG{\forall~x:T,U}{\Type(k)}}}
-\item [Lam]\index{Typing rules!Lam} 
+\item[Lam]\index{Typing rules!Lam} 
 \inference{\frac{\WTEG{\forall~x:T,U}{s}~~~~ \WTE{\Gamma::(x:T)}{t}{U}}
         {\WTEG{\lb~x:T\mto t}{\forall x:T, U}}}
-\item [App]\index{Typing rules!App}
+\item[App]\index{Typing rules!App}
  \inference{\frac{\WTEG{t}{\forall~x:U,T}~~~~\WTEG{u}{U}}
                  {\WTEG{(t\ u)}{\subst{T}{x}{u}}}}
-\item [Let]\index{Typing rules!Let} 
+\item[Let]\index{Typing rules!Let} 
 \inference{\frac{\WTEG{t}{T}~~~~ \WTE{\Gamma::(x:=t:T)}{u}{U}}
         {\WTEG{\kw{let}~x:=t~\kw{in}~u}{\subst{U}{x}{t}}}}
-\end{itemize}
-
-\noindent {\bf Remark. } We may have $\kw{let}~x:=t~\kw{in}~u$
+\end{description}
+    
+\Rem We may have $\kw{let}~x:=t~\kw{in}~u$
 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}).
@@ -416,14 +416,18 @@ convertibility into an order inductively defined by:
 
 The conversion rule is now exactly:
 
-\begin{itemize}\label{Conv}
-\item [Conv]\index{Typing rules!Conv}
+\begin{description}\label{Conv}
+\item[Conv]\index{Typing rules!Conv}
  \inference{
       \frac{\WTEG{U}{s}~~~~\WTEG{t}{T}~~~~\WTEGLECONV{T}{U}}{\WTEG{t}{U}}}
-\end{itemize}
+  \end{description}
+
 
+\paragraph{$\eta$-conversion.
+\label{eta}
+\index{eta-conversion@$\eta$-conversion}
+\index{eta-reduction@$\eta$-reduction}}
 
-\paragraph{$\eta$-conversion.}\label{eta}\index{eta-conversion@$\eta$-conversion}\index{eta-reduction@$\eta$-reduction}
 An other important rule is the $\eta$-conversion. It is to identify
 terms over a dummy abstraction of a variable followed by an
 application of this variable. Let $T$ be a type, $t$ be a term in
diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex
index da21ec467..34e421149 100755
--- a/doc/RefMan-com.tex
+++ b/doc/RefMan-com.tex
@@ -3,20 +3,17 @@
 \ttindex{coqc}
 
 There are two \Coq~commands: 
-
-\bigskip
-\begin{tabular}{l@{\quad:\quad}l}
-  -- {\tt coqtop} & The \Coq\ toplevel (interactive mode) ; \\[1em]
-  -- {\tt coqc}   & The \Coq\ compiler (batch compilation).
-\end{tabular}
-\bigskip
-
+\begin{itemize}
+\item {\tt coqtop}: The \Coq\ toplevel (interactive mode) ; 
+\item {\tt coqc} : The \Coq\ compiler (batch compilation).
+\end{itemize}
 The options are (basically) the same for the two commands, and
 roughly described below. You can also look at the \verb!man! pages of
 \verb!coqtop! and \verb!coqc! for more details.
 
 
 \section{Interactive use ({\tt coqtop})}
+
 In the interactive mode, also known as the \Coq~toplevel, the user can
 develop his theories and proofs step by step.  The \Coq~toplevel is
 run by the command {\tt coqtop}. 
@@ -173,7 +170,7 @@ The following command-line options are recognized by the commands {\tt
   only available for {\tt coqtop}.
 
 %\item[{\tt -compile-verbose} {\em file}]\ 
-@
+
 %  This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} with
 %  a copy of the contents of the file on standard input.
 %  This option implies options {\tt -batch} and {\tt -silent}. It is
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 568f8713b..39541153d 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -4,8 +4,9 @@
 {\gallina} is the kernel language of {\Coq}. We describe here extensions of
 the Gallina's syntax.
 
-\section{Record types}\comindex{Record}
-\label{Record}
+\section{Record types
+\comindex{Record}
+\label{Record}}
 
 The \verb+Record+ construction is a macro allowing the definition of
 records as is done in many programming languages.  Its syntax is
@@ -15,8 +16,7 @@ also for ``manifest'' expressions. In this sense, the \verb+Record+
 construction allows to define ``signatures''.
 
 \begin{figure}[h]
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
+\begin{centerframe}
 \begin{tabular}{lcl}
 {\sentence} & ++= & {\record}\\
   & & \\
@@ -27,8 +27,7 @@ construction allows to define ``signatures''.
 {\field} & ::= & {\name} : {\type} \\
  & $|$ & {\name} {\typecstr} := {\term}
 \end{tabular}
-\end{minipage}}
-\end{center}
+\end{centerframe}
 \caption{Syntax for the definition of {\tt Record}}
 \label{record-syntax}
 \end{figure}
@@ -80,31 +79,29 @@ Record Rat : Set := mkRat
 Remark here that the field
 \verb+Rat_cond+ depends on the field \verb+bottom+. 
 
-Let us now see the work done by the {\tt Record} macro.
-First the macro generates an inductive definition
-with just one constructor:
-
-\medskip
-\noindent
-{\tt Inductive {\ident} {\binderlet} : {\sort} := \\
-\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) .. 
-({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.}
-\medskip
+%Let us now see the work done by the {\tt Record} macro.
+%First the macro generates an inductive definition
+%with just one constructor:
+%
+%\medskip
+%\noindent
+%{\tt Inductive {\ident} {\binderlet} : {\sort} := \\
+%\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) .. 
+%({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.}
+%\medskip
 
 Let us now see the work done by the {\tt Record} macro.  First the
 macro generates an inductive definition with just one constructor:
-\begin{tabular}{l}
+\begin{quote}
 {\tt Inductive {\ident} {\params} :{\sort} :=} \\
-~~~~{\tt
+\qquad {\tt
   {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).}
-\end{tabular}
-
+\end{quote}
 To build an object of type {\ident}, one should provide the
 constructor {\ident$_0$} with $n$ terms filling the fields of
 the record.
 
-Let us define the rational $1/2$.
-
+As an example, let us define the rational $1/2$:
 \begin{coq_example*}
 Require Import Arith.
 Theorem one_two_irred :
@@ -159,51 +156,53 @@ Reset Initial.
   There may be three reasons:
    \begin{enumerate}
    \item The name {\ident$_i$} already exists in the environment (see
-     section \ref{Axiom}).
+     Section~\ref{Axiom}).
    \item The body of {\ident$_i$} uses an incorrect elimination for
-     {\ident} (see sections \ref{Fixpoint} and \ref{Caseexpr}).
+     {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}).
    \item The type of the projections {\ident$_i$} depends on previous
    projections which themselves couldn't be defined.
    \end{enumerate}  
 \end{Warnings}     
 
 \begin{ErrMsgs}
-\item \errindex{A record cannot be recursive}\\
+
+\item \errindex{A record cannot be recursive}
+
   The record name {\ident} appears in the type of its fields.
+  
+\item During the definition of the one-constructor inductive
+  definition, all the errors of inductive definitions, as described in
+  Section~\ref{gal_Inductive_Definitions}, may also occur.
 
-\item
-  During the definition of the one-constructor inductive definition,
-  all the errors of inductive definitions, as described in section
-  \ref{gal_Inductive_Definitions}, may also occur.
 \end{ErrMsgs}
 
-\SeeAlso Coercions and records in section \ref{Coercions-and-records}
+\SeeAlso Coercions and records in Section~\ref{Coercions-and-records}
 of the chapter devoted to coercions.
 
 \Rem {\tt Structure} is a synonym of the keyword {\tt Record}.
 
 \Rem An experimental syntax for projections based on a dot notation is
 available. The command to activate it is
-
-\bigskip
+\begin{quote}
 {\tt Set Printing Projections.}
-\bigskip
-
-The corresponding grammar is:
-\bigskip
+\end{quote}
 
-\begin{tabular}{|lcl|}
-\hline
+\begin{figure}[t]
+\begin{centerframe}
+\begin{tabular}{lcl}
 {\term} & ++= & {\term} {\tt .(} {\qualid} {\tt )}\\
  & $|$ & {\term} {\tt .(} {\qualid} \nelist{\termarg}{} {\tt )}\\
- & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )}\\
-\hline
+ & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )}
 \end{tabular}
-\bigskip
+\end{centerframe}
+\caption{Syntax of \texttt{Record} projections}
+\label{fig:projsyntax}
+\end{figure}
 
+The corresponding grammar rules are given Figure~\ref{fig:projsyntax}.
 When {\qualid} denotes a projection, the syntax {\tt
-{\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax {\tt
-{\term}.({\qualid}~{\termarg}$_1$~ \ldots~ {\termarg}$_n$)} to
+  {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax
+{\tt {\term}.({\qualid}~{\termarg}$_1$~ \ldots~ {\termarg}$_n$)} to
 {\qualid~{\termarg}$_1$ \ldots {\termarg}$_n$~\term}, and the syntax
 {\tt {\term}.(@{\qualid}~{\term}$_1$~\ldots~{\term}$_n$)} to
 {@\qualid~{\term}$_1$ \ldots {\term}$_n$~\term}. In each case, {\term}
@@ -214,13 +213,13 @@ To deactivate the printing of projections, use
 {\tt Unset Printing Projections}.
 
 
-\section{Variants and extensions of {\tt match}}
+\section{Variants and extensions of {\tt match}
 \label{Extensions-of-match}
-\index{match@{\tt match\ldots with\ldots end}}
+\index{match@{\tt match\ldots with\ldots end}}}
 
-\subsection{Multiple and nested pattern-matching}
+\subsection{Multiple and nested pattern-matching
 \index{ML-like patterns}
-\label{Mult-match}
+\label{Mult-match}}
 
 The basic version of \verb+match+ allows pattern-matching on simple
 patterns. As an extension, multiple and nested patterns are
@@ -233,8 +232,8 @@ its expanded form.
 
 \SeeAlso chapter \ref{Mult-match-full}.
 
-\subsection{Pattern-matching on boolean values: the {\tt if} expression}
-\index{if@{\tt if ... then ... else}}
+\subsection{Pattern-matching on boolean values: the {\tt if} expression
+\index{if@{\tt if ... then ... else}}}
 
 For inductive types with exactly two constructors, it is possible to
 use a {\tt if ... then ... else} notation. For instance, the
@@ -257,9 +256,9 @@ Reset not.
 Definition not (b:bool) := if b then false else true.
 \end{coq_example}
 
-\subsection{Irrefutable patterns: the destructuring {\tt let}}
+\subsection{Irrefutable patterns: the destructuring {\tt let}
 \index{let in@{\tt let ... in}}
-\label{Letin}
+\label{Letin}}
 
 
 
@@ -294,117 +293,136 @@ can be put in constructor form. Otherwise, reduction is blocked.
 
 The pretty-printing of a definition by matching on a
 irrefutable pattern can either be done using {\tt match} or the {\tt
-let} construction (see section \ref{printing-options}).
+let} construction (see Section~\ref{printing-options}).
 
-\subsection{Options for pretty-printing of {\tt match}}
-\label{printing-options}
+\subsection{Options for pretty-printing of {\tt match}
+\label{printing-options}}
 
 There are three options controlling the pretty-printing of {\tt match}
 expressions.
 
-\subsubsection{Printing of wildcard pattern}
+\subsubsection{Printing of wildcard pattern
 \comindex{Set Printing Wildcard}
 \comindex{Unset Printing Wildcard}
-\comindex{Test Printing Wildcard}
+\comindex{Test Printing Wildcard}}
 
 Some variables in a pattern may not occur in the right-hand side of
 the pattern-matching clause.  There are options to control the
 display of these variables.
 
-\subsubsection{\tt Set Printing Wildcard.}
- The variables having no occurrences
-in the right-hand side of the pattern-matching clause are just
-printed using the wildcard symbol ``{\tt \_}''.
+\begin{quote}
+{\tt Set Printing Wildcard.}
+\end{quote}
+The variables having no occurrences in the right-hand side of the
+pattern-matching clause are just printed using the wildcard symbol
+``{\tt \_}''.
 
-\subsubsection{\tt Unset Printing Wildcard.}
+\begin{quote}
+{\tt Unset Printing Wildcard.}
+\end{quote}
 The variables, even useless, are printed using their usual name. But some
 non dependent variables have no name. These ones are still printed
 using a ``{\tt \_}''.
 
-\subsubsection{\tt Test Printing Wildcard.}
-This tells if the wildcard
-printing mode is on or off. The default is to print wildcard for
-useless variables.
+\begin{quote}
+{\tt Test Printing Wildcard.}
+\end{quote}
+This tells if the wildcard printing mode is on or off. The default is
+to print wildcard for useless variables.
 
-\subsubsection{Printing of the elimination predicate}
+\subsubsection{Printing of the elimination predicate
 \comindex{Set Printing Synth}
 \comindex{Unset Printing Synth}
-\comindex{Test Printing Synth}
+\comindex{Test Printing Synth}}
 
 In most of the cases, the type of the result of a matched term is
 mechanically synthesisable. Especially, if the result type does not
 depend of the matched term.
 
-\subsubsection{\tt Set Printing Synth.}
-The result type is not printed
-when {\Coq} knows that it can re-synthesise it.
+\begin{quote}
+{\tt Set Printing Synth.}
+\end{quote}
+The result type is not printed when {\Coq} knows that it can
+re-synthesise it.
 
-\subsubsection{\tt Unset Printing Synth.}
+\begin{quote}
+{\tt Unset Printing Synth.}
+\end{quote}
 This forces the result type to be always printed.
 
-\subsubsection{\tt Test Printing Synth.}
-This tells if the non-printing
-of synthesisable types is on or off. The default is to not print 
-synthesisable types.
+\begin{quote}
+{\tt Test Printing Synth.}
+\end{quote}
+This tells if the non-printing of synthesisable types is on or off.
+The default is to not print synthesisable types.
 
-\subsubsection{Printing matching on irrefutable pattern}
+\subsubsection{Printing matching on irrefutable pattern
 \comindex{Add Printing Let {\ident}}
 \comindex{Remove Printing Let {\ident}}
 \comindex{Test Printing Let {\ident}}
-\comindex{Print Table Printing Let}
+\comindex{Print Table Printing Let}}
 
 If an inductive type has just one constructor,
 pattern-matching can be written using {\tt let} ... {\tt :=}
 ... {\tt in}~...
 
-\subsubsection{\tt Add Printing Let {\ident}.}
-This adds {\ident} to the list
-of inductive types for which pattern-matching is written using a {\tt
-let} expression.
+\begin{quote}
+{\tt Add Printing Let {\ident}.}
+\end{quote}
+This adds {\ident} to the list of inductive types for which
+pattern-matching is written using a {\tt let} expression.
 
-\subsubsection{\tt Remove Printing Let {\ident}.}
+\begin{quote}
+{\tt Remove Printing Let {\ident}.}
+\end{quote}
 This removes {\ident} from this list.
 
-\subsubsection{\tt Test Printing Let {\ident}.}
-This tells if {\ident} belongs
-to the list.
+\begin{quote}
+{\tt Test Printing Let {\ident}.}
+\end{quote}
+This tells if {\ident} belongs to the list.
 
-\subsubsection{\tt Print Table Printing Let.}
-This prints the list of inductive types
-for which pattern-matching is written using a {\tt
-let} expression.
+\begin{quote}
+{\tt Print Table Printing Let.}
+\end{quote}
+This prints the list of inductive types for which pattern-matching is
+written using a {\tt let} expression.
 
 The list of inductive types for which pattern-matching is written
 using a {\tt let} expression is managed synchronously. This means that
 it is sensible to the command {\tt Reset}.
 
-
-\subsubsection{Printing matching on booleans}
+\subsubsection{Printing matching on booleans
 \comindex{Add Printing If {\ident}}
 \comindex{Remove Printing If {\ident}}
 \comindex{Test Printing If {\ident}}
-\comindex{Print Table Printing If}
+\comindex{Print Table Printing If}}
 
 If an inductive type is isomorphic to the boolean type,
-pattern-matching can be written using {\tt if} ... {\tt then}
-... {\tt else} ...
+pattern-matching can be written using {\tt if} ... {\tt then} ... {\tt
+  else} ...
 
-\subsubsection{\tt Add Printing If {\ident}.}
-This adds {\ident} to the list
-of inductive types for which pattern-matching is written using an {\tt
-if} expression.
+\begin{quote}
+{\tt Add Printing If {\ident}.}
+\end{quote}
+This adds {\ident} to the list of inductive types for which
+pattern-matching is written using an {\tt if} expression.
 
-\subsubsection{\tt Remove Printing If {\ident}.}
+\begin{quote}
+{\tt Remove Printing If {\ident}.}
+\end{quote}
 This removes {\ident} from this list.
 
-\subsubsection{\tt Test Printing If {\ident}.}
-This tells if {\ident} belongs
-to the list.
+\begin{quote}
+{\tt Test Printing If {\ident}.}
+\end{quote}
+This tells if {\ident} belongs to the list.
 
-\subsubsection{\tt Print Table Printing If.}
-This prints the list of inductive types
-for which pattern-matching is written using an {\tt
-if} expression.
+\begin{quote}
+{\tt Print Table Printing If.}
+\end{quote}
+This prints the list of inductive types for which pattern-matching is
+written using an {\tt if} expression.
 
 The list of inductive types for which pattern-matching is written
 using an {\tt if} expression is managed synchronously. This means that
@@ -412,7 +430,7 @@ it is sensible to the command {\tt Reset}.
 
 \subsubsection{Example}
 
-This example emphasises what the printing options offer.
+This example emphasizes what the printing options offer.
 
 \begin{coq_example}
 Test Printing Let prod.
@@ -472,12 +490,16 @@ Print fst.
 %% Check id.
 %% \end{coq_example}
 
-\section{Section mechanism}\index{Sections}\label{Section}
+\section{Section mechanism
+\index{Sections}
+\label{Section}}
+
 The sectioning mechanism allows to organise a proof in structured
-sections. Then local declarations become available (see section
-\ref{Simpl-definitions}).
+sections. Then local declarations become available (see
+Section~\ref{Simpl-definitions}). 
+
+\subsection{\tt Section {\ident}\comindex{Section}}
 
-\subsection{\tt Section {\ident}}\comindex{Section}
 This command is used to open a section named {\ident}.
 
 %% Discontinued ?
@@ -487,7 +509,9 @@ This command is used to open a section named {\ident}.
 %%         Same as {\tt Section {\ident}}
 %% \end{Variants}
 
-\subsection{\tt End {\ident}}\comindex{End}
+\subsection{\tt End {\ident}
+\comindex{End}}
+
 This command closes the section named {\ident}. When a section is
 closed, all local declarations (variables and local definitions) are
 {\em discharged}. This means that all global objects defined in the
@@ -533,10 +557,11 @@ section is closed.
 
 \section{Libraries and qualified names}
 
-\subsection{Names of libraries and files}
+\subsection{Names of libraries and files
 \label{Libraries}
 \index{Libraries}
-\index{Logical paths}
+\index{Logical paths}}
+
 \paragraph{Libraries}
 
 The theories developed in {\Coq} are stored in {\em libraries}.  A
@@ -563,15 +588,12 @@ paths} (written {\dirpath} and of which the syntax is the same as
 {\qualid}, see \ref{qualid}). Logical directory
 paths can be mapped to physical directories of the
 operating system using the command (see \ref{AddLoadPath})
-
 \begin{quote}
 {\tt Add LoadPath {\it physical\_path} as {\dirpath}}.
 \end{quote}
-
 A library can inherit the tree structure of a physical directory by
 using the {\tt -R} option to {\tt coqtop} or the
 command (see \ref{AddRecLoadPath})
-
 \begin{quote}
 {\tt Add Rec LoadPath {\it physical\_path} as {\dirpath}}.
 \end{quote}
@@ -580,22 +602,23 @@ command (see \ref{AddRecLoadPath})
 library called {\tt Top}.
 
 \paragraph{The file level}
+
 At some point, (sub-)libraries contain {\it modules} which coincide
-with files at the physical level.
-As for sublibraries, the dot notation is used to denote a specific
-module of a library. Typically, {\tt Coq.Init.Logic} is the logical path
-associated to the file {\tt Logic.v} of {\Coq} standard library.
-Notice that compilation (see \ref{Addoc-coqc}) is done at the level of files.
+with files at the physical level.  As for sublibraries, the dot
+notation is used to denote a specific module of a library. Typically,
+{\tt Coq.Init.Logic} is the logical path associated to the file {\tt
+  Logic.v} of {\Coq} standard library.  Notice that compilation (see
+\ref{Addoc-coqc}) is done at the level of files.
 
 If the physical directory where a file {\tt File.v} lies is mapped to
 the empty logical directory path (which is the default when using the
 simple form of {\tt Add LoadPath} or {\tt -I} option to coqtop), then
 the name of the module it defines is {\tt File}.
 
-\subsection{Qualified names}
+\subsection{Qualified names
 \label{LongNames}
 \index{Qualified identifiers}
-\index{Absolute names}
+\index{Absolute names}}
 
 Modules contain constructions (sub-modules, axioms, parameters,
 definitions, lemmas, theorems, remarks or facts). The (full) name of a
@@ -640,11 +663,9 @@ qualification. Still, to ensure that a construction always remains
 accessible, absolute names can never be hidden.
 
 Examples:
-
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
-
 \begin{coq_example}
 Check 0.
 Definition nat := bool.
@@ -657,10 +678,10 @@ Locate nat.
 
 \Rem In versions prior to {\Coq} 7.4, lemmas declared with {\tt
 Remark} and {\tt Fact} kept in their full name the names of the
-sections in which they were defined. From {\Coq} 7.4, they strictly
+sections in which they were defined. Since {\Coq} 7.4, they strictly
 behaves as {\tt Theorem} and {\tt Lemma} do.
 
-\SeeAlso Command {\tt Locate} in section \ref{Locate}.
+\SeeAlso Command {\tt Locate} in Section~\ref{Locate}.
 
 %% \paragraph{The special case of remarks and facts}
 %% 
@@ -683,9 +704,9 @@ When requiring the file, the mapping between physical directories and logical li
 The command {\tt Add Rec LoadPath} is also available from {\tt coqtop}
 and {\tt coqc} by using option~\verb=-R=.
 
-\section{Implicit arguments}
+\section{Implicit arguments
 \index{Implicit arguments}
-\label{Implicit Arguments}
+\label{Implicit Arguments}}
 
 An implicit argument of a function is an argument which can be
 inferred from the knowledge of the type of other arguments of the
@@ -707,18 +728,16 @@ itself applied or matched against patterns (since the original
 form of the argument can be lost by reduction).
 
 For instance, the first argument of
-
-\begin{verbatim}
-   cons : forall A:Set, A -> list A -> list A
-\end{verbatim}
+\begin{quote}
+\verb|cons: forall A:Set, A -> list A -> list A|
+\end{quote}
 in module {\tt List.v} is strict because {\tt list} is an inductive
 type and {\tt A} will always be inferable from the type {\tt
 list A} of the third argument of {\tt cons}.
 On the opposite, the second argument of a term of type 
-
-\begin{verbatim}
-   forall P:nat->Prop, forall n:nat, P n -> ex nat P
-\end{verbatim}
+\begin{quote}
+\verb|forall P:nat->Prop, forall n:nat, P n -> ex nat P|
+\end{quote}
 is implicit but not strict, since it can only be inferred from the
 type {\tt P n} of the the third argument and if {\tt P} is e.g. {\tt
 fun \_ => True}, it reduces to an expression where {\tt n} does not
@@ -735,15 +754,13 @@ An implicit argument can be {\em contextual} or non. An implicit
 argument is said {\em contextual} if it can be inferred only from the
 knowledge of the type of the context of the current expression. For
 instance, the only argument of
-
-\begin{verbatim}
-   nil : forall A:Set, list A
-\end{verbatim}
+\begin{quote}
+\verb|nil : forall A:Set, list A|
+\end{quote}
 is contextual. Similarly, both arguments of a term of type
-
-\begin{verbatim}
-   forall P:nat->Prop, forall n:nat, P n \/ n = 0
-\end{verbatim}
+\begin{quote}
+\verb|forall P:nat->Prop, forall n:nat, P n \/ n = 0|
+\end{quote}
 are contextual (moreover, {\tt n} is strict and {\tt P} is not).
 
 \subsection{Casual use of implicit arguments}
@@ -753,26 +770,24 @@ can be inferred from the type of the other arguments, the user can
 force the given argument to be guessed by replacing it by ``{\tt \_}''. If
 possible, the correct argument will be automatically generated.
 
-\ErrMsg
-\begin{enumerate}
-\item \errindex{Cannot infer a term for this placeholder}\\
+\begin{ErrMsgs}
+
+\item \errindex{Cannot infer a term for this placeholder}
+
   {\Coq} was not able to deduce an instantiation of a ``{\tt \_}''.
-\end{enumerate}
 
-\subsection{Declaration of implicit arguments for a constant}
-\comindex{Implicit Arguments}
+\end{ErrMsgs}
+
+\subsection{Declaration of implicit arguments for a constant
+\comindex{Implicit Arguments}}
 
 In case one wants that some arguments of a given object (constant,
 inductive types, constructors, assumptions, local or not) are always
 inferred by Coq, one may declare once for all which are the expected
 implicit arguments of this object. The syntax is
-
-\bigskip
-\begin{tt}
-Implicit Arguments {\qualid} [ \nelist{\ident}{} ]
-\end{tt}
-\bigskip
-
+\begin{quote}
+\tt Implicit Arguments {\qualid} [ \nelist{\ident}{} ]
+\end{quote}
 where the list of {\ident} is the list of parameters to be declared
 implicit. After this, implicit arguments can just (and have to) be
 skipped in any expression involving an application of {\qualid}.
@@ -803,19 +818,14 @@ implicit arguments of {\qualid}.
 
 {\Coq} can also automatically detect what are the implicit arguments
 of a defined object. The command is just
-
-\bigskip
-\begin{tt}
-Implicit Arguments {\qualid}.
-\end{tt}
-\bigskip
-
+\begin{quote}
+\tt Implicit Arguments {\qualid}.
+\end{quote}
 The auto-detection is governed by options telling if strict and
-contextual implicit arguments must be considered or not (see sections
-\ref{SetStrictImplicit} and \ref{SetContextualImplicit}).
+contextual implicit arguments must be considered or not (see
+Sections~\ref{SetStrictImplicit} and~\ref{SetContextualImplicit}). 
 
 \Example
-
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
@@ -859,62 +869,56 @@ Variables (a b c : X) (r1 : R a b) (r2 : R b c).
 Check (p r1 r2).
 \end{coq_example}
 
-\subsection{Mode for automatic declaration of implicit arguments}
+\subsection{Mode for automatic declaration of implicit arguments
 \label{Auto-implicit}
 \comindex{Set Implicit Arguments}
-\comindex{Unset Implicit Arguments}
+\comindex{Unset Implicit Arguments}}
 
 In case one wants to systematically declare implicit the arguments
 detectable as such, one may switch to the automatic declaration of
 implicit arguments mode by using the command
-
-\bigskip
-{\tt Set Implicit Arguments}.
-\bigskip
-
+\begin{quote}
+\tt Set Implicit Arguments.
+\end{quote}
 Conversely, one may unset the mode by using {\tt Unset Implicit
 Arguments}.  The mode is off by default. Auto-detection of implicit
 arguments is governed by options controlling whether strict and
 contextual implicit arguments have to be considered or not.
 
-\subsection{Controlling strict implicit arguments}
+\subsection{Controlling strict implicit arguments
 \comindex{Set Strict Implicit}
 \comindex{Unset Strict Implicit}
-\label{SetStrictImplicit}
+\label{SetStrictImplicit}}
 
 By default, {\Coq} automatically set implicit only the strict implicit
 arguments. To relax this constraint, use command 
-
-\bigskip 
-{\tt Unset Strict Implicit}.
-\bigskip 
-
+\begin{quote}
+\tt Unset Strict Implicit.
+\end{quote}
 Conversely, use command {\tt Set Strict Implicit} to
 restore the strict implicit mode.
 
 \Rem In versions of {\Coq} prior to version 8.0, the default was to
 declare the strict implicit arguments as implicit.
 
-\subsection{Controlling contextual implicit arguments}
+\subsection{Controlling contextual implicit arguments
 \comindex{Set Contextual Implicit}
 \comindex{Unset Contextual Implicit}
-\label{SetContextualImplicit}
+\label{SetContextualImplicit}}
 
 By default, {\Coq} does not automatically set implicit the contextual
 implicit arguments. To tell {\Coq} to infer also contextual implicit
 argument, use command  
-
-\bigskip
-{\tt Set Contextual Implicit}. 
-\bigskip
-
+\begin{quote}
+\tt Set Contextual Implicit. 
+\end{quote}
 Conversely, use command {\tt Unset Contextual Implicit} to
 unset the contextual implicit mode.
 
-\subsection{Explicit Applications}
+\subsection{Explicit Applications
 \index{Explicitation of implicit arguments}
 \label{Implicits-explicitation}
-\index{@{\qualid}}
+\index{qualid@{\qualid}}}
 
 In presence of non strict or contextual argument, or in presence of
 partial applications, the synthesis of implicit arguments may fail, so
@@ -923,9 +927,10 @@ application. The syntax for this is {\tt (\ident:=\term)} where {\ident}
 is the name of the implicit argument and {\term} is its corresponding
 explicit term. Alternatively, one can locally deactivate the hidding of
 implicit arguments of a function by using the notation
-{\tt @{\qualid}~{\term}$_1$..{\term}$_n$}.
-
-\medskip
+{\tt @{\qualid}~{\term}$_1$..{\term}$_n$}. This syntax extension is
+given Figure~\ref{fig:explicitations}.
+\begin{figure}
+\begin{centerframe}
 \begin{tabular}{lcl}
 {\term} & ++= & @ {\qualid} \nelist{\term}{}\\
 & $|$ & @ {\qualid}\\
@@ -934,44 +939,43 @@ implicit arguments of a function by using the notation
 {\textrm{\textsl{argument}}} & ::= & {\term} \\
 & $|$ & {\tt ({\ident}:={\term})}\\
 \end{tabular}
-\medskip
-
-{\medskip \noindent {\bf Example (continued): }}
+\end{centerframe}
+\caption{Syntax for explicitations of implicit arguments}
+\label{fig:explicitations}
+\end{figure}
 
+\noindent {\bf Example (continued): }
 \begin{coq_example}
 Check (p r1 (z:=c)).
 Check (p (x:=a) (y:=b) r1 (z:=c) r2).
 \end{coq_example}
 
-\subsection{Displaying what the implicit arguments are}
+\subsection{Displaying what the implicit arguments are
 \comindex{Print Implicit}
-\label{PrintImplicit}
+\label{PrintImplicit}}
 
 To display the implicit arguments associated to an object use command
+\begin{quote}
+\tt Print Implicit {\qualid}.
+\end{quote}
 
-\bigskip
-{\tt Print Implicit {\qualid}}.
-\bigskip
-
-\subsection{Explicitation of implicit arguments for pretty-printing}
+\subsection{Explicitation of implicit arguments for pretty-printing
 \comindex{Set Print Implicit}
-\comindex{Unset Print Implicit}
+\comindex{Unset Print Implicit}}
 
 By default the basic pretty-printing rules hide the inferable implicit
 arguments of an application. To force printing all implicit arguments,
 use command
-
-\bigskip
+\begin{quote}
 {\tt Set Printing Implicit.}
-\bigskip
-
+\end{quote}
 Conversely, to restore the hidding of implicit arguments, use command
-
-\bigskip
+\begin{quote}
 {\tt Unset Printing Implicit.}
-\bigskip
+\end{quote}
 
-\subsection{Canonical structures}
+\subsection{Canonical structures
+\comindex{Canonical Structure}}
 
 A canonical structure is an instance of a record/structure type that
 can be used to solve equations involving implicit arguments. Assume
@@ -979,12 +983,9 @@ that {\qualid} denotes an object $(Build\_struc~ c_1~ \ldots~ c_n)$ in the
 structure {\em struct} of which the fields are $x_1$, ...,
 $x_n$. Assume that {\qualid} is declared as a canonical structure
 using the command
-
-\bigskip
+\begin{quote}
 {\tt Canonical Structure {\qualid}.}
-\comindex{Canonical Structure}
-\bigskip
-
+\end{quote}
 Then, each time an equation of the form $(x_i~
 \_)=_{\beta\delta\iota\zeta}c_i$ has to be solved during the
 type-checking process, {\qualid} is used as a solution. Otherwise
@@ -993,7 +994,6 @@ complete structure built on $c_i$.
 
 Canonical structures are particularly useful when mixed with
 coercions and strict implicit arguments. Here is an example.
-
 \begin{coq_example*}
 Require Import Relations.
 Require Import EqNat.
@@ -1012,7 +1012,6 @@ Canonical Structure nat_setoid.
 
 Thanks to \texttt{nat\_setoid} declared as canonical, the implicit
 arguments {\tt A} and {\tt B} can be synthesised in the next statement.
-
 \begin{coq_example}
 Lemma is_law_S : is_law S.
 \end{coq_example}
@@ -1040,11 +1039,9 @@ It is possible to bind variable names to a given type (e.g. in a
 development using arithmetic, it may be convenient to bind the names
 {\tt n} or {\tt m} to the type {\tt nat} of natural numbers). The
 command for that is
-
-\bigskip
-{\tt Implicit Types \nelist{\ident}{} : {\type}}
-\bigskip
-
+\begin{quote}
+\tt Implicit Types \nelist{\ident}{} : {\type}
+\end{quote}
 The effect of the command is to automatically set the type of bound
 variables starting with {\ident} (either {\ident} itself or
 {\ident} followed by one or more single quotes, underscore or digits)
@@ -1052,7 +1049,6 @@ to be {\type} (unless the bound variable is already declared with an
 explicit type in which case, this latter type is considered).
 
 \Example
-
 \begin{coq_example}
 Require Import List.
 Implicit Types m n : nat.
@@ -1066,8 +1062,9 @@ Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m.
 This is useful for declaring the implicit type of a single variable.
 \end{Variants}
 
-\section{Coercions}
-\label{Coercions}\index{Coercions}
+\section{Coercions
+\label{Coercions}
+\index{Coercions}}
 
 Coercions can be used to implicitly inject terms from one {\em class} in
 which they reside into another one. A {\em class} is either a sort
@@ -1080,13 +1077,11 @@ Then the user is able to apply an
 object that is not a function, but can be coerced to a function, and
 more generally to consider that a term of type A is of type B provided
 that there is a declared coercion between A and B. The main command is
-
-\bigskip
 \comindex{Coercion}
-{\tt Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.}
-\bigskip
-
-\noindent which declares the construction denoted by {\qualid} as a
+\begin{quote}
+\tt Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.
+\end{quote}
+which declares the construction denoted by {\qualid} as a
 coercion between {\class$_1$} and {\class$_2$}.
 
 More details and examples, and a description of the commands related
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 93045fae6..5a4983151 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -1,5 +1,5 @@
-\chapter{The \gallina{} specification language}
-\label{Gallina}\index{Gallina}
+\chapter{The \gallina{} specification language
+\label{Gallina}\index{Gallina}}
 
 This chapter describes \gallina, the specification language of Coq.
 It allows to develop mathematical theories and to prove specifications
@@ -14,8 +14,8 @@ In Coq, logical objects are typed to ensure their logical
 correctness. The rules implemented by the typing algorithm are described in
 chapter \ref{Cic}.
 
-\subsection*{About the grammars in the manual}
-\label{BNF-syntax}\index{BNF metasyntax}
+\subsection*{About the grammars in the manual
+\label{BNF-syntax}\index{BNF metasyntax}}
 
 Grammars are presented in Backus-Naur form (BNF). Terminal symbols are
 set in {\tt typewriter font}.  In addition, there are special
@@ -40,8 +40,8 @@ At the end, the notation ``\sequence{\entry}{\tt sep}'' stands for a
 possibly empty sequence of expressions parsed by the ``{\entry}'' entry,
 separated by the literal ``{\tt sep}''.
 
-\section{Lexical conventions}
-\label{lexical}\index{Lexical conventions}
+\section{Lexical conventions
+\label{lexical}\index{Lexical conventions}}
 
 \paragraph{Blanks}
 Space, newline and horizontal tabulation are considered as blanks.
@@ -63,11 +63,13 @@ That is, they are recognized by the following lexical class:
 \index{ident@\ident}
 \begin{center}
 \begin{tabular}{rcl} 
-{\firstletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{\_}%\op\ml{unicode-letter}
- \\
-{\subsequentletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{0..9}\op\ml{\_}%\op\ml{\$}
-\op\ml{'} \\
-{\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{}\\
+{\firstletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt \_}
+% $\mid$ {\tt unicode-letter}  
+\\
+{\subsequentletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt 0..9}
+$\mid$ {\tt \_} % $\mid$ {\tt \$}
+$\mid$ {\tt '} \\
+{\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{}
 \end{tabular}
 \end{center}
 All characters are meaningful. In particular, identifiers are case-sensitive.
@@ -82,9 +84,9 @@ Numerals are sequences of digits. Integers are numerals optionally preceded by a
 \index{integer@{\integer}}
 \begin{center}
 \begin{tabular}{r@{\quad::=\quad}l}
-{\digit} & \ml{0..9} \\
+{\digit} & {\tt 0..9} \\
 {\num} & \nelistwithoutblank{\digit}{} \\
-{\integer} & \zeroone{\ml{-}}{\num} \\
+{\integer} & \zeroone{\tt -}{\num} \\
 \end{tabular}
 \end{center}
 
@@ -202,7 +204,8 @@ rule: when a sequence of non alphanumerical characters can be decomposed
 into several different ways, then the first token is the longest
 possible one (among all tokens defined at this moment), and so on.
 
-\section{Terms}\label{term}\index{Terms}
+\section{Terms \label{term}\index{Terms}}
+
 \subsection{Syntax of terms}
 
 Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic
@@ -213,9 +216,8 @@ chapter \ref{Cic}. Extensions of this syntax are given in chapter
 chapter \ref{Addoc-syntax}.
 
 \begin{figure}[htbp]
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
-\begin{tabular}{lcl@{~~~~~}r}
+\begin{centerframe}
+\begin{tabular}{lcl@{\qquad}r}
 {\term} & ::= &
          {\tt forall} {\binderlist} {\tt ,} {\term}  &(\ref{products})\\
  & $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\
@@ -261,17 +263,15 @@ chapter \ref{Addoc-syntax}.
 {\binderlet} & ::= & {\binder} & \ref{Binders} \\
  & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
 & & &\\
-{\name} & \cn{}::= & {\ident} &\\
+{\name} & ::= & {\ident} &\\
  & $|$ & {\tt \_} &\\
 &&&\\
 {\qualid} & ::= & {\ident} & \\
  & $|$ & {\qualid} {\accessident} &\\
  & & &\\
-{\sort} & ::= & {\tt Prop} ~$|$~ {\tt Set} ~$|$~ {\tt Type} &\\
-\hline
+{\sort} & ::= & {\tt Prop} ~$|$~ {\tt Set} ~$|$~ {\tt Type} &
 \end{tabular}
-\end{minipage}}
-\end{center}
+\end{centerframe}
 \caption{Syntax of terms}
 \label{term-syntax}
 \index{term@{\term}}
@@ -281,8 +281,7 @@ chapter \ref{Addoc-syntax}.
 
 
 \begin{figure}[htb]
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
+\begin{centerframe}
 \begin{tabular}{lcl}
 {\idparams} & ::= &  {\ident} \sequence{\binderlet}{} {\typecstr} \\
 &&\\
@@ -319,8 +318,7 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\num}                                 \\
  & $|$ & {\tt (} \nelist{\pattern}{,} {\tt )}     
 \end{tabular}
-\end{minipage}}
-\end{center}
+\end{centerframe}
 \caption{Syntax of terms (continued)}
 \label{term-syntax-aux}
 \end{figure}
@@ -336,9 +334,9 @@ of types inside the syntactic class {\term}.
 \index{type@{\type}}
 
 
-\subsection{Qualified identifiers and simple identifiers}
+\subsection{Qualified identifiers and simple identifiers
 \label{qualid}
-\label{ident}
+\label{ident}}
 
 {\em Qualified identifiers} ({\qualid}) denote {\em global constants}
 (definitions, lemmas, theorems, remarks or facts), {\em global
@@ -348,8 +346,8 @@ types} or {\em constructors of inductive types}.
 syntactic subset of qualified identifiers.  Identifiers may also
 denote local {\em variables}, what qualified identifiers do not.
 
-\subsection{Numerals}
-\label{numerals}
+\subsection{Numerals
+\label{numerals}}
 
 Numerals have no definite semantics in the calculus. They are mere
 notations that can be bound to objects through the notation mechanism
@@ -360,15 +358,15 @@ bound to Peano's representation of natural numbers
 Note: negative integers are not at the same level as {\num}, for this
 would make precedence unnatural.
 
-\subsection{Sorts}\index{Sorts}
+\subsection{Sorts 
+\index{Sorts}
 \index{Type@{\Type}}
 \index{Set@{\Set}}
 \index{Prop@{\Prop}}
 \index{Sorts}
-\label{Gallina-sorts}
+\label{Gallina-sorts}}
 
 There are three sorts \Set, \Prop\ and \Type.
-
 \begin{itemize}
 \item \Prop\ is the universe of {\em logical propositions}.
 The logical propositions themselves are typing the proofs.
@@ -383,12 +381,11 @@ subclass of the syntactic class {\term}.
 \index{specif@{\specif}}
 \item {\Type} is the type of {\Set} and {\Prop}
 \end{itemize}
+More on sorts can be found in section \ref{Sorts}.
 
-\noindent More on sorts can be found in section \ref{Sorts}.
-
-\subsection{Binders}
+\subsection{Binders
 \label{Binders}
-\index{binders}
+\index{binders}}
 
 Various constructions introduce variables which scope is some of its
 sub-expressions. There is a uniform syntax for this. A binder may be
@@ -415,9 +412,9 @@ syntactic class as {\term}. We denote by {\type} the semantic subclass
 of types inside the syntactic class {\term}.
 \index{type@{\type}}
 
-\subsection{Abstractions}
+\subsection{Abstractions
 \label{abstractions}
-\index{abstractions}
+\index{abstractions}}
 
 The expression ``{\tt fun} {\ident} {\tt :} \type {\tt =>} {\term}''
 denotes the {\em abstraction} of the variable {\ident} of type
@@ -425,18 +422,18 @@ denotes the {\em abstraction} of the variable {\ident} of type
 formal parameter {\ident} of type {\type} returning {\term}.
 
 Keyword {\tt fun} is followed by a ``binder list'', so any of the
-binders of section~\ref{Binders} apply. Internally, abstractions are
+binders of Section~\ref{Binders} apply. Internally, abstractions are
 only over one variable. Multiple variable binders are an iteration of
 the single variable abstraction: notation {\tt
 fun}~{\ident$_{1}$}~{\ldots}~{\ident$_{n}$}~{\tt :}~\type~{\tt
 =>}~{\term} stands for {\tt fun}~{\ident$_{1}$}~{\tt :}~\type~{\tt
 =>}~{\ldots}~{\tt fun}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term}.
 Variables with a value expand to a local definition (see
-section~\ref{let-in}).
+Section~\ref{let-in}).
 
-\subsection{Products}
+\subsection{Products
 \label{products}
-\index{products}
+\index{products}}
 
 The expression ``{\tt forall}~{\ident}~{\tt :}~\type~{\tt ,}~{\term}''
 denotes the {\em product} of the variable {\ident} of type {\type},
@@ -448,9 +445,9 @@ Non dependent product types have a special notation ``$A$ {\tt ->}
 $B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. This is to stress
 on the fact that non dependent produt types are usual functional types.
 
-\subsection{Applications}
+\subsection{Applications
 \label{applications}
-\index{applications}
+\index{applications}}
 
 {\tt (}\term$_0$ \term$_1${\tt)} denotes the application of
   term \term$_0$ to \term$_1$.
@@ -464,30 +461,30 @@ associativity is to the left.
 When using implicit arguments mechanism, implicit positions can be
 forced a value with notation {\tt (}\,{\ident}\,{\tt
 :=}\,{\term}\,{\tt )} or {\tt (}\,{\num}\,{\tt
-:=}\,{\term}\,{\tt )}. See section~\ref{Implicits-explicitation} for
+:=}\,{\term}\,{\tt )}. See Section~\ref{Implicits-explicitation} for
 details.
 
-\subsection{Type cast}
+\subsection{Type cast
 \label{typecast}
-\index{Cast}
+\index{Cast}}
 
 The expression ``{\term}~{\tt :}~{\type}'' is a type cast
 expression. It forces checking that {\term} has type {\type}. It is
 identified to {\term}.
 
-\subsection{Inferable subterms}
+\subsection{Inferable subterms
 \label{hole}
-\index{\_}
+\index{\_}}
 
 Since there are redundancies, a term can be type-checked without
 giving it in totality. Subterms that are left to guess by the
 type-checker are replaced by ``\_''.
 
 
-\subsection{Local definitions (let-in)}
+\subsection{Local definitions (let-in)
 \label{let-in}
 \index{Local definitions}
-\index{let-in}
+\index{let-in}}
 
 
 {\tt let}~{\ident}~{\tt :=}~{\term$_1$}~{\tt in}~{\term$_2$} denotes
@@ -500,13 +497,13 @@ let} {\ident} {\binder$_1$} \ldots {\binder$_n$} {\tt :=} {\term$_1$}
 {\binder$_1$} \ldots {\binder$_n$} {\tt in} {\term$_2$}.
 
 
-\subsection{Definition by case analysis}
+\subsection{Definition by case analysis
 \label{caseanalysis}
-\index{match@{\tt match\ldots with\ldots end}}
+\index{match@{\tt match\ldots with\ldots end}}}
 
 
 This paragraph only shows simple variants of case analysis. See
-section~\ref{Mult-match} and chapter~\ref{Mult-match-full} for
+Section~\ref{Mult-match} and Chapter~\ref{Mult-match-full} for
 explanations of the general form.
 
 Objects of inductive types can be destructurated by a case-analysis
@@ -535,18 +532,18 @@ match} depends on the actual {\term$_0$} matched.
 There are specific notations for case analysis on types with one or
 two constructors: {\tt if}\ldots{\tt then}\ldots{\tt else}\ldots and
 {\tt let (}\ldots{\tt ) :=}\ldots{\tt in}\ldots. \SeeAlso
-section~\ref{Mult-match} for details and examples.
+Section~\ref{Mult-match} for details and examples.
 
-\subsection{Recursive functions}
+\subsection{Recursive functions
 \label{fixpoints}
-\index{fix@{fix \ident$_i$\{\dots\}}}
+\index{fix@{fix \ident$_i$\{\dots\}}}}
 
 Expression ``{\tt fix} \ident$_1$ \binder$_1$ {\tt :} {\type$_1$}
 \texttt{:=} \term$_1$ {\tt with} {\ldots} {\tt with} \ident$_n$
 \binder$_n$~{\tt :} {\type$_n$} \texttt{:=} \term$_n$ {\tt for}
 {\ident$_i$}'' denotes the $i$th component of a block of functions
 defined by mutual well-founded recursion. It is the local counterpart
-of the {\tt Fixpoint} command. See section~\ref{Fixpoint} for more
+of the {\tt Fixpoint} command. See Section~\ref{Fixpoint} for more
 details. When $n=1$, the {\tt for}~{\ident$_i$} is omitted.
 
 The expression ``{\tt cofix} \ident$_1$~\binder$_1$ {\tt :}
@@ -554,7 +551,7 @@ The expression ``{\tt cofix} \ident$_1$~\binder$_1$ {\tt :}
 :} {\type$_n$}~{\tt for} {\ident$_i$}'' denotes the $i$th component of
 a block of terms defined by a mutual guarded co-recursion. It is the
 local counterpart of the {\tt CoFixpoint} command. See
-section~\ref{CoFixpoint} for more details. When $n=1$, the {\tt
+Section~\ref{CoFixpoint} for more details. When $n=1$, the {\tt
 for}~{\ident$_i$} is omitted.
 
 The association of a single fixpoint and a local
@@ -564,12 +561,11 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
   applies for co-fixpoints.
 
 
-\section{The Vernacular}
-\label{Vernacular}
+\section{The Vernacular
+\label{Vernacular}}
 
 \begin{figure}[tbp]
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
+\begin{centerframe}
 \begin{tabular}{lcl}
 {\sentence} & ::= & {\declaration} \\
             & $|$ & {\definition} \\
@@ -616,16 +612,25 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
    & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Defined} {\tt .}\\
    & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .}
 \end{tabular}
-\end{minipage}}
-\end{center}
+\end{centerframe}
 \caption{Syntax of sentences}
 \label{sentences-syntax}
 \end{figure}
 
+Figure \ref{sentences-syntax} describes {\em The Vernacular} which is the
+language of commands of \gallina.  A sentence of the vernacular
+language, like in many natural languages, begins with a capital letter
+and ends with a dot.
+
+The different kinds of command are described hereafter. They all suppose
+that the terms occurring in the sentences are well-typed.
+
 %%
 %% Axioms and Parameters
 %%
-\subsection{Declarations}\index{Declarations}\label{Declarations}
+\subsection{Declarations
+\index{Declarations}
+\label{Declarations}}
 
 The declaration mechanism allows the user to specify his own basic
 objects. Declared objects play the role of axioms or parameters in
@@ -635,11 +640,11 @@ correct type in the current context of the declaration and \ident\ was
 not previously defined in the same module. This {\term} is considered
 to be the type, or specification, of the \ident.
 
-\subsubsection{{\tt Axiom {\ident} :{\term} .}}
+\subsubsection{{\tt Axiom {\ident} :{\term} .}
 \comindex{Axiom}
 \comindex{Parameter}\comindex{Parameters}
 \comindex{Conjecture}
-\label{Axiom}
+\label{Axiom}}
 
 This command links {\term} to the name {\ident} as its specification
 in the global context. The fact asserted by {\term} is thus assumed as
@@ -671,14 +676,14 @@ a postulate.
 {\tt Parameters}.
 
 
-\subsubsection{{\tt Variable {\ident} :{\term}}.}
+\subsubsection{{\tt Variable {\ident} :{\term}}.
 \comindex{Variable}
 \comindex{Variables}
 \comindex{Hypothesis}
-\comindex{Hypotheses}
+\comindex{Hypotheses}}
 
 This command links {\term} to the name {\ident} in the context of the
-current section (see~\ref{Section} for a description of the section
+current section (see Section~\ref{Section} for a description of the section
 mechanism). When the current section is closed, name {\ident} will be
 unknown and every object using this variable will be explicitly
 parameterized (the variable is {\em discharged}). Using the {\tt
@@ -702,7 +707,7 @@ Variable} command out of any section is equivalent to {\tt Axiom}.
 \end{Variants}
 
 \noindent {\bf Remark: } It is possible to replace {\tt Variable} by
-{\tt Variables} and \ml{Hypothesis} by {\tt Hypotheses}.
+{\tt Variables} and {\tt Hypothesis} by {\tt Hypotheses}.
 
 It is advised to use the keywords \verb:Axiom: and \verb:Hypothesis:
 for logical postulates (i.e. when the assertion {\term} is of sort
@@ -713,13 +718,16 @@ abstract mathematical entity).
 %%
 %% Definitions
 %%
-\subsection{Definitions}\index{Definitions}\label{Simpl-definitions}
+\subsection{Definitions
+\index{Definitions}
+\label{Simpl-definitions}}
+
 Definitions differ from declarations in allowing to give a name to a
 term whereas declarations were just giving a type to a name. That is
 to say that the name of a defined object can be replaced at any time
 by its definition.  This replacement is called
 $\delta$-conversion\index{delta-reduction@$\delta$-reduction} (see
-section~\ref{delta}).  A defined object is accepted by the system if
+Section~\ref{delta}).  A defined object is accepted by the system if
 and only if the defining term is well-typed in the current context of
 the definition.  Then the type of the name is the type of term. The
 defined name is called a {\em constant}\index{Constant} and one says
@@ -727,11 +735,12 @@ that {\it the constant is added to the
 environment}\index{Environment}.
 
 A formal presentation of constants and environments is given in
-section \ref{Typed-terms}.
+Section~\ref{Typed-terms}.
+
 
+\subsubsection{\tt Definition {\ident} := {\term}.
+\comindex{Definition}}
 
-\subsubsection{\tt Definition {\ident} := {\term}.}
-\comindex{Definition}
 This command binds the value {\term} to the name {\ident} in the
 environment, provided that {\term} is well-typed.
 
@@ -759,9 +768,11 @@ environment, provided that {\term} is well-typed.
     \texttt{Actually, it has type {\term$_3$}}.
 \end{ErrMsgs}
 
-\SeeAlso sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
+\SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
+
+\subsubsection{\tt Local {\ident} := {\term}.
+\comindex{Local}}
 
-\subsubsection{\tt Local {\ident} := {\term}.}\comindex{Local}
 This command binds the value {\term} to the name {\ident} in the
 environment of the current section. The name {\ident} will be unknown
 when the current section will be closed and all occurrences of
@@ -777,15 +788,17 @@ definition is a kind of {\em macro}.
 \item {\tt Local {\ident} : {\term$_1$} := {\term$_2$}.}
 \end{Variants}
 
-\SeeAlso \ref{Section} (section mechanism), \ref{Opaque},
+\SeeAlso Sections \ref{Section} (section mechanism), \ref{Opaque},
 \ref{Transparent} (opaque/transparent constants), \ref{unfold}
 
 %%
 %% Inductive Types
 %%
-\subsection{Inductive definitions}
-\index{Inductive definitions} \label{gal_Inductive_Definitions}
-\comindex{Inductive}\label{Inductive}
+\subsection{Inductive definitions
+\index{Inductive definitions} 
+\label{gal_Inductive_Definitions}
+\comindex{Inductive}
+\label{Inductive}}
 
 We gradually explain simple inductive types, simple
 annotated inductive types, simple parametric inductive types, 
@@ -813,7 +826,7 @@ The name {\ident} is the name of the inductively defined type and
 The names {\ident$_1$}, {\ldots}, {\ident$_n$}
 are the names of its constructors and {\type$_1$}, {\ldots},
 {\type$_n$} their respective types. The types of the constructors have
-to satisfy a {\em positivity condition} (see section \ref{Positivity})
+to satisfy a {\em positivity condition} (see Section~\ref{Positivity})
 for {\ident}.  This condition ensures the soundness of the inductive
 definition.  If this is the case, the constants {\ident},
 {\ident$_1$}, {\ldots}, {\ident$_n$} are added to the environment with
@@ -954,11 +967,12 @@ This is an alternative definition of lists where we specify the
 arguments of the constructors rather than their full type.
 \end{Variants}
 
-\SeeAlso sections \ref{Cic-inductive-definitions} and~\ref{elim}.
+\SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{elim}.
 
 
-\subsubsection{Mutually defined inductive types}
-\comindex{Mutual Inductive}\label{Mutual-Inductive}
+\subsubsection{Mutually defined inductive types
+\comindex{Mutual Inductive}
+\label{Mutual-Inductive}}
 
 The definition of a block of mutually inductive types has the form:
 
@@ -1061,11 +1075,11 @@ section is closed, the variables declared in the section and occurring
 free in the declaration are added as parameters to the inductive
 definition. 
 
-\SeeAlso \ref{Section}
+\SeeAlso Section~\ref{Section}
 
-\subsubsection{Co-inductive types}
+\subsubsection{Co-inductive types
 \label{CoInductiveTypes}
-\comindex{CoInductive}
+\comindex{CoInductive}}
 
 The objects of an inductive type are well-founded with respect to the
 constructors of the type. In other words, such objects contain only a
@@ -1084,7 +1098,7 @@ CoInductive Stream : Set :=
 \end{coq_example}
 
 The syntax of this command is the same as the command \texttt{Inductive}
-(cf. section \ref{gal_Inductive_Definitions}). Notice that no
+(cf. Section~\ref{gal_Inductive_Definitions}). Notice that no
 principle of induction is derived from the definition of a
 co-inductive type, since such principles only make sense for inductive
 ones. For co-inductive ones, the only elimination principle is case
@@ -1110,17 +1124,17 @@ CoInductive EqSt : Stream -> Stream -> Prop :=
 In order to prove the extensionally equality of two streams $s_1$ and
 $s_2$ we have to construct and infinite proof of equality, that is,
 an infinite object of type $(\texttt{EqSt}\;s_1\;s_2)$. We will see
-how to introduce infinite objects in section \ref{CoFixpoint}.
+how to introduce infinite objects in Section~\ref{CoFixpoint}.
 
 %%
 %% (Co-)Fixpoints
 %%
 \subsection{Definition of recursive functions}
 
-\subsubsection{\tt Fixpoint
-   {\ident} {\params} {\tt \{struct} \ident$_0$ {\tt \}} : type$_0$ :=
-   \term$_0$}
-\comindex{Fixpoint}\label{Fixpoint}
+\subsubsection{\tt Fixpoint {\ident} {\params} {\tt \{struct}
+  \ident$_0$ {\tt \}} : type$_0$ := \term$_0$ 
+\comindex{Fixpoint}
+\label{Fixpoint}}
 
 This command allows to define inductive objects using a fixed point
 construction. The meaning of this declaration is to define {\it ident}
@@ -1156,7 +1170,7 @@ equals \verb:O: we return \verb:m:, and when \verb:n: equals
 \verb:(S p): we return \verb:(S (add p m)):.
 
 The {\tt match} operator is formally described
-in detail in section \ref{Caseexpr}.  The system recognizes that in
+in detail in Section~\ref{Caseexpr}.  The system recognizes that in
 the inductive call {\tt (add p m)} the first argument actually
 decreases because it is a {\em pattern variable} coming from {\tt match
   n with}.
@@ -1253,16 +1267,17 @@ Fixpoint tree_size (t:tree) : nat :=
   end.
 \end{coq_example*}
 A generic command {\tt Scheme} is useful to build automatically various
-mutual induction principles. It is described in section \ref{Scheme}.
+mutual induction principles. It is described in Section~\ref{Scheme}.
 
-\subsubsection{\tt CoFixpoint {\ident} : \type$_0$ := \term$_0$.}
-\comindex{CoFixpoint}\label{CoFixpoint}
+\subsubsection{\tt CoFixpoint {\ident} : \type$_0$ := \term$_0$.
+\comindex{CoFixpoint}
+\label{CoFixpoint}}
 
 The {\tt CoFixpoint} command introduces a method for constructing an
 infinite object of a coinduc\-tive type. For example, the stream
 containing all natural numbers can be introduced applying the
 following method to the number \texttt{O} (see
-section~\ref{CoInductiveTypes} for the definition of {\tt Stream},
+Section~\ref{CoInductiveTypes} for the definition of {\tt Stream},
 {\tt hd} and {\tt tl}):
 \begin{coq_eval}
 Reset Initial.
@@ -1321,7 +1336,7 @@ Eval compute in (tl (from 0)).
      with\\
         \mbox{}\hspace{0.1cm} $\ldots$  \\
         with {\ident$_m$}   : {\type$_m$} := {\term$_m$}}\\
-As in the \texttt{Fixpoint} command (cf. section~\ref{Fixpoint}), it
+As in the \texttt{Fixpoint} command (cf. Section~\ref{Fixpoint}), it
 is possible to introduce a block of mutually dependent methods.
 \end{Variants}
 
@@ -1334,11 +1349,11 @@ A statement claims a goal of which the proof is then interactively done
 using tactics. More on the proof editing mode, statements and proofs can be
 found in chapter \ref{Proof-handling}.
 
-\subsubsection{\tt Theorem {\ident} : {\type}.}
+\subsubsection{\tt Theorem {\ident} : {\type}.
 \comindex{Theorem}
 \comindex{Lemma}
 \comindex{Remark}
-\comindex{Fact}
+\comindex{Fact}}
 
 This command binds {\type} to the name {\ident} in the
 environment, provided that a proof of {\type} is next given.
@@ -1368,13 +1383,13 @@ definition of expression which computational behaviour will be used by
 further commands. \SeeAlso~\ref{Transparent} and \ref{unfold}. 
 \end{Variants}
 
-\subsubsection{{\tt Proof} {\tt .} \dots {\tt Qed} {\tt .}}
+\subsubsection{{\tt Proof} {\tt .} \dots {\tt Qed} {\tt .}
 \comindex{Proof}
 \comindex{Qed}
 \comindex{Defined}
 \comindex{Save}
 \comindex{Goal}
-\comindex{Admitted}
+\comindex{Admitted}}
 
 A proof starts by the keyword {\tt Proof}.  Then {\Coq} enters the
 proof editing mode until the proof is completed. The proof editing
diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex
index d0d9b1ee3..148121324 100644
--- a/doc/RefMan-ide.tex
+++ b/doc/RefMan-ide.tex
@@ -8,12 +8,12 @@ purpose is to allow the user to navigate forward and backward into a
 \Coq{} vernacular file, executing corresponding commands or undoing
 them respectively. % CREDITS ? Proof general, lablgtk, ...
 
-\coqide{} is run by typing the command \verb|coqide| on the command
+\CoqIDE{} is run by typing the command \verb|coqide| on the command
 line. Without argument, the main screen is displayed with an ``unnamed
 buffer'', and with a file name as argument, another buffer displaying
 the contents of that file. Additionally, coqide accepts the same
 options as coqtop, given in Chapter~\ref{Addoc-coqc}, the ones having
-obviously no meaning for \coqide{} being ignored.
+obviously no meaning for \CoqIDE{} being ignored.
 
 \begin{figure}[t]
 \begin{center}
@@ -26,11 +26,11 @@ obviously no meaning for \coqide{} being ignored.
 \fi
 %END LATEX
 \end{center}
-\caption{\coqide{} main screen}
+\caption{\CoqIDE{} main screen}
 \label{fig:coqide}
 \end{figure}
 
-A sample \coqide{} main screen, while navigating into a file
+A sample \CoqIDE{} main screen, while navigating into a file
 \verb|Fermat.v|, is shown on Figure~\ref{fig:coqide}.  At
 the top is a menu bar, and a tool bar below it. The large window on
 the left is displaying the various \emph{script buffers}. The upper right
@@ -50,7 +50,7 @@ one where Coq commands are currently executed.
 
 Buffers may be edited as in any text editor, and classical basic
 editing commands (Copy/Paste, \ldots) are available in the \emph{Edit}
-menu. \coqide{} offers only basic editing commands, so if you need
+menu. \CoqIDE{} offers only basic editing commands, so if you need
 more complex editing commands, you may launch your favorite text
 editor on the current buffer, using the \emph{Edit/External Editor}
 menu. 
@@ -131,7 +131,7 @@ arguments.
 \fi
 %END LATEX
 \end{center}
-\caption{\coqide{}: the query window}
+\caption{\CoqIDE{}: the query window}
 \label{fig:querywindow}
 \end{figure}
 
@@ -140,10 +140,10 @@ We call \emph{query} any vernacular command that do not change the
 current state, such as \verb|Check|, \verb|SearchAbout|, etc. Those
 commands are of course useless during compilation of a file, hence
 should not be included in scripts. To run such commands without
-writing them in the script, \coqide{} offers another input window
+writing them in the script, \CoqIDE{} offers another input window
 called the \emph{query window}. This window can be displayed on
 demand, either by using the \texttt{Window} menu, or directly using
-shortcuts given in the \texttt{Queries} menu. Indeed, with \coqide{}
+shortcuts given in the \texttt{Queries} menu. Indeed, with \CoqIDE{}
 the simplest way to perform a \texttt{SearchAbout} on some identifier
 is to select it using the mouse, and pressing \verb|F2|. This will
 both make appear the query window and run the \texttt{SearchAbout} in
@@ -176,7 +176,7 @@ The second section is devoted to file management: you may
 configure automatic saving of files, by periodically saving the
 contents into files named \verb|#f#| for each opened file
 \verb|f|. You may also activate the \emph{revert} feature: in case a
-opened file is modified on the disk by a third party, \coqide{} may read
+opened file is modified on the disk by a third party, \CoqIDE{} may read
 it again for you. Note that in the case you edited that same file, you
 will be prompt to choose to either discard your changes or not.
 
@@ -207,7 +207,7 @@ resources syntax
 \url{http://developer.gnome.org/doc/API/2.0/gtk/gtk-Resource-Files.html}.
 Such a default resource file exists in the \Coq{} library, you may
 copy this file into your home directory, and edit it using any text
-editor, \coqide{} itself for example.
+editor, \CoqIDE{} itself for example.
 
   
 % $Id$ 
diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex
index 2331b6226..b1f4b26b8 100755
--- a/doc/RefMan-int.tex
+++ b/doc/RefMan-int.tex
@@ -102,7 +102,7 @@ corresponds to the Chapter~\ref{Addoc-syntax}.
 \end{itemize}
 
 At the end of the document, after the global index, the user can find
-a tactic index and a vernacular command index, and an index of error
+specific indexes for tactics, vernacular commands, and error
 messages. 
 
 \section*{List of additional documentation}
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index f9b4d2ae0..4df89ddf3 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -76,7 +76,7 @@ Notation & Precedence & Associativity \\
 \verb!_ / _!   & 40 & left \\
 \verb!- _!  & 35 & right \\
 \verb!/ _!  & 35 & right \\
-\verb!_ ^ _!   & 30 & left \\
+\verb!_ ^ _!   & 30 & right \\
 \hline
 \end{tabular}
 \end{center}
@@ -84,18 +84,12 @@ Notation & Precedence & Associativity \\
 \label{init-notations}
 \end{figure}
 
-\subsection{Logic} \label{Logic}
-
-The basic library of {\Coq} comes with the definitions of standard
-(intuitionistic) logical connectives (they are defined as inductive
-constructions). They are equipped with an appealing syntax enriching the
-(subclass {\form}) of the syntactic class {\term}. The syntax
-extension is shown on figure \ref{formulas-syntax}.
+\subsection{Logic} 
+\label{Logic}
 
 \begin{figure}
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
-\begin{tabular}{rclr}
+\begin{centerframe}
+\begin{tabular}{lclr}
 {\form} & ::= & {\tt True} & ({\tt True})\\
   & $|$ & {\tt False} & ({\tt False})\\
   & $|$ & {\tt\char'176} {\form} & ({\tt not})\\
@@ -112,8 +106,7 @@ extension is shown on figure \ref{formulas-syntax}.
   & $|$ & {\term} {\tt =} {\term} & ({\tt eq})\\
   & $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq})
 \end{tabular}
-\end{minipage}}
-\end{center}
+\end{centerframe}
 \caption{Syntax of formulas}
 \label{formulas-syntax}
 \end{figure}
@@ -122,16 +115,20 @@ The basic library of {\Coq} comes with the definitions of standard
 (intuitionistic) logical connectives (they are defined as inductive
 constructions). They are equipped with an appealing syntax enriching the
 (subclass {\form}) of the syntactic class {\term}. The syntax
-extension
-\footnote{This syntax is defined in module {\tt LogicSyntax}}
- is shown on figure \ref{formulas-syntax}.
+extension is shown on figure \ref{formulas-syntax}.
 
-\Rem Implication is not defined but primitive
-(it is a non-dependent product of a proposition over another proposition).
-There is also a primitive universal quantification (it is a
-dependent product over a proposition). The primitive universal
-quantification allows both first-order and higher-order
-quantification. 
+% The basic library of {\Coq} comes with the definitions of standard
+% (intuitionistic) logical connectives (they are defined as inductive
+% constructions). They are equipped with an appealing syntax enriching
+% the (subclass {\form}) of the syntactic class {\term}. The syntax
+% extension \footnote{This syntax is defined in module {\tt
+%     LogicSyntax}} is shown on Figure~\ref{formulas-syntax}.
+ 
+\Rem Implication is not defined but primitive (it is a non-dependent
+product of a proposition over another proposition).  There is also a
+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}
@@ -231,7 +228,9 @@ Inductive eq (A:Type) (x:A) : A -> Prop :=
     refl_equal : eq A x x.
 \end{coq_example*}
 
-\subsubsection{Lemmas} \label{PreludeLemmas}
+\subsubsection{Lemmas} 
+\label{PreludeLemmas}
+
 Finally, a few easy lemmas are provided.
 
 \ttindex{absurd}
@@ -300,17 +299,43 @@ Theorem f_equal3 :
 Abort.
 \end{coq_eval}
 
-\subsection{Datatypes} \label{Datatypes}
+\subsection{Datatypes}
+\label{Datatypes}
+\index{Datatypes}
+
+\begin{figure}
+\begin{centerframe}
+\begin{tabular}{rclr}
+{\specif} & ::= & {\specif} {\tt *} {\specif} & ({\tt prod})\\
+  & $|$ & {\specif} {\tt +} {\specif} & ({\tt sum})\\
+  & $|$ & {\specif} {\tt + \{} {\specif} {\tt \}} & ({\tt sumor})\\
+  & $|$ & {\tt \{} {\specif} {\tt \} + \{} {\specif} {\tt \}} &
+  ({\tt sumbool})\\  
+  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form} {\tt \}}
+  & ({\tt sig})\\
+  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form}  {\tt \&}
+  {\form} {\tt \}} & ({\tt sig2})\\
+  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
+    \}} & ({\tt sigS})\\
+  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
+    \&} {\specif} {\tt \}} & ({\tt sigS2})\\
+  &  & & \\
+{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair})
+\end{tabular}
+\end{centerframe}
+\caption{Syntax of datatypes and specifications}
+\label{specif-syntax}
+\end{figure}
+
 
 In the basic library, we find the definition\footnote{They are in {\tt
     Datatypes.v}} of the basic data-types of programming, again
 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} 
+\label{Programming}
 \index{Programming}
-\index{Datatypes}
-
 \label{libnats}
 
 \ttindex{unit}
@@ -457,32 +482,6 @@ in the \verb"Set" \verb"A+{B}".
 Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B).
 \end{coq_example*}
 
-\begin{figure}
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
-\begin{tabular}{rclr}
-{\specif} & ::= & {\specif} {\tt *} {\specif} & ({\tt prod})\\
-  & $|$ & {\specif} {\tt +} {\specif} & ({\tt sum})\\
-  & $|$ & {\specif} {\tt + \{} {\specif} {\tt \}} & ({\tt sumor})\\
-  & $|$ & {\tt \{} {\specif} {\tt \} + \{} {\specif} {\tt \}} &
-  ({\tt sumbool})\\  
-  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form} {\tt \}}
-  & ({\tt sig})\\
-  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form}  {\tt \&}
-  {\form} {\tt \}} & ({\tt sig2})\\
-  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
-    \}} & ({\tt sigS})\\
-  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
-    \&} {\specif} {\tt \}} & ({\tt sigS2})\\
-  &  & & \\
-{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair})
-\end{tabular}
-\end{minipage}}
-\end{center}
-\caption{Syntax of datatypes and specifications}
-\label{specif-syntax}
-\end{figure}
-
 We may define variants of the axiom of choice, like in Martin-Löf's
 Intuitionistic Type Theory.
 \ttindex{Choice}
diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index 3e3a93e7f..06307a030 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -27,9 +27,9 @@ problems.
 \def\tacarg{\nterm{tacarg}}
 \def\cpattern{\nterm{cpattern}}
 
-The syntax of the tactic language is given in tables~\ref{ltac}
-and~\ref{ltac_aux}. See section~\ref{BNF-syntax} for a description of
-the BNF metasyntax used in these tables. Various already defined
+The syntax of the tactic language is given Figures~\ref{ltac}
+and~\ref{ltac_aux}. See page~\pageref{BNF-syntax} for a description of
+the BNF metasyntax used in these grammar rules. Various already defined
 entries will be used in this chapter: entries {\naturalnumber},
 {\integer}, {\ident}, {\qualid}, {\term}, {\cpattern} and {\atomictac}
 represent respectively the natural and integer numbers, the authorized
@@ -44,7 +44,7 @@ side, they are used without the question mark.
 
 The main entry of the grammar is {\tacexpr}. This language is used in
 proof mode but it can also be used in toplevel definitions as shown in
-table~\ref{ltactop}.
+Figure~\ref{ltactop}.
 
 \begin{Remarks}
 \item The infix tacticals ``\dots\ {\tt ||} \dots'' and ``\dots\ {\tt
@@ -57,21 +57,20 @@ prefix tacticals {\tt try}, {\tt repeat}, {\tt do}, {\tt info} and
 \dots''.
 
 For instance
-\begin{tabbing}
+\begin{quote}
 {\tt try repeat \tac$_1$ ||
   \tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.}
-\end{tabbing}
+\end{quote}
 is understood as 
-\begin{tabbing}
+\begin{quote}
 {\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\
 {\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).}
-\end{tabbing}
+\end{quote}
 \end{Remarks}
 
 
 \begin{figure}[htbp]
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
+\begin{centerframe}
 \begin{tabular}{lcl}
 {\tacexpr} & ::= &
            {\tacexpr} {\tt ;} {\tacexpr}\\
@@ -104,28 +103,27 @@ is understood as
 {\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
 & | &
 {\tt match} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\
-& \cn{}| & {\tt abstract} {\atom}\\
-& \cn{}| & {\tt abstract} {\atom} {\tt using} {\ident} \\
-& \cn{}| & {\tt first [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
-& \cn{}| & {\tt solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
-& \cn{}| & {\tt idtac} ~|~ {\tt idtac} {\qstring}\\
-& \cn{}| & {\tt fail} ~|~ {\tt fail} {\naturalnumber} {\qstring}\\
-& \cn{}| & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\
-& \cn{}| & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\
-& \cn{}| & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
-& \cn{}| & {\tt type of} {\term}\\
-& \cn{}| & {\tt constr :} {\term}\\
-& \cn{}| & \atomictac\\
-& \cn{}| & {\qualid} \nelist{\tacarg}{}\\
-& \cn{}| & {\atom}\\
+& | & {\tt abstract} {\atom}\\
+& | & {\tt abstract} {\atom} {\tt using} {\ident} \\
+& | & {\tt first [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
+& | & {\tt solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
+& | & {\tt idtac} ~|~ {\tt idtac} {\qstring}\\
+& | & {\tt fail} ~|~ {\tt fail} {\naturalnumber} {\qstring}\\
+& | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\
+& | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\
+& | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
+& | & {\tt type of} {\term}\\
+& | & {\tt constr :} {\term}\\
+& | & \atomictac\\
+& | & {\qualid} \nelist{\tacarg}{}\\
+& | & {\atom}\\
 \\
 {\atom} & ::= &
            {\qualid} \\
 & | & ()\\
 & | & {\tt (} {\tacexpr} {\tt )}\\
 \end{tabular}
-\end{minipage}}
-\end{center}
+\end{centerframe}
 \caption{Syntax of the tactic language}
 \label{ltac}
 \end{figure}
@@ -133,8 +131,7 @@ is understood as
 
 
 \begin{figure}[htbp]
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
+\begin{centerframe}
 \begin{tabular}{lcl}
 \tacarg & ::= & 
         {\qualid}\\
@@ -158,22 +155,19 @@ is understood as
 & $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\
 & $|$ & {\tt \_ =>} {\tacexpr}\\
 \end{tabular}
-\end{minipage}}
-\end{center}
+\end{centerframe}
 \caption{Syntax of the tactic language (continued)}
 \label{ltac_aux}
 \end{figure}
 
 \begin{figure}[ht]
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
+\begin{centerframe}
 \begin{tabular}{lcl}
 \nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
 \\
 \nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr}
 \end{tabular}
-\end{minipage}}
-\end{center}
+\end{centerframe}
 \caption{Tactic toplevel definitions}
 \label{ltactop}
 \end{figure}
@@ -183,7 +177,9 @@ is understood as
 %% Semantics
 %%
 \section{Semantics}
-\index[tactic]{Tacticals}\index{Tacticals}\label{Tacticals}
+%\index[tactic]{Tacticals}
+\index{Tacticals}
+%\label{Tacticals}
 
 Tactic expressions can only be applied in the context of a goal.  The
 evaluation yields either a term, an integer or a tactic. Intermediary
@@ -201,7 +197,7 @@ of Ltac.
 
 %% \subsection{Values}
 
-%% Values are given by table~\ref{ltacval}. All these values are tactic values,
+%% Values are given by Figure~\ref{ltacval}. All these values are tactic values,
 %% i.e. to be applied to a goal, except {\tt Fun}, {\tt Rec} and $arg$ values.
 
 %% \begin{figure}[ht]
@@ -209,30 +205,30 @@ of Ltac.
 %% {\parbox{6in}
 %% {\begin{center}
 %% \begin{tabular}{lp{0.1in}l}
-%% $vexpr$ & \cn{}::= & $vexpr$ {\tt ;} $vexpr$\\
-%% & \cn{}| & $vexpr$ {\tt ; [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt
+%% $vexpr$ & ::= & $vexpr$ {\tt ;} $vexpr$\\
+%% & | & $vexpr$ {\tt ; [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt
 %% ]}\\
-%% & \cn{}| & $vatom$\\
+%% & | & $vatom$\\
 %% \\
-%% $vatom$ & \cn{}::= & {\tt Fun} \nelist{\inputfun}{}  {\tt ->} {\tacexpr}\\
-%% %& \cn{}| & {\tt Rec} \recclause\\
-%% & \cn{}| &
+%% $vatom$ & ::= & {\tt Fun} \nelist{\inputfun}{}  {\tt ->} {\tacexpr}\\
+%% %& | & {\tt Rec} \recclause\\
+%% & | &
 %% {\tt Rec} \nelist{\recclause}{\tt And} {\tt In}
 %% {\tacexpr}\\
-%% & \cn{}| &
+%% & | &
 %% {\tt Match Context With} {\it (}$context\_rule$ {\tt |}{\it )}$^*$
 %% $context\_rule$\\
-%% & \cn{}| & {\tt (} $vexpr$ {\tt )}\\
-%% & \cn{}| & $vatom$ {\tt Orelse} $vatom$\\
-%% & \cn{}| & {\tt Do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} $vatom$\\
-%% & \cn{}| & {\tt Repeat} $vatom$\\
-%% & \cn{}| & {\tt Try} $vatom$\\
-%% & \cn{}| & {\tt First [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt ]}\\
-%% & \cn{}| & {\tt Solve [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt ]}\\
-%% & \cn{}| & {\tt Idtac}\\
-%% & \cn{}| & {\tt Fail}\\
-%% & \cn{}| & {\primitivetactic}\\
-%% & \cn{}| & $arg$
+%% & | & {\tt (} $vexpr$ {\tt )}\\
+%% & | & $vatom$ {\tt Orelse} $vatom$\\
+%% & | & {\tt Do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} $vatom$\\
+%% & | & {\tt Repeat} $vatom$\\
+%% & | & {\tt Try} $vatom$\\
+%% & | & {\tt First [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt ]}\\
+%% & | & {\tt Solve [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt ]}\\
+%% & | & {\tt Idtac}\\
+%% & | & {\tt Fail}\\
+%% & | & {\primitivetactic}\\
+%% & | & $arg$
 %% \end{tabular}
 %% \end{center}}}
 %% \caption{Values of ${\cal L}_{tac}$}
@@ -243,30 +239,28 @@ of Ltac.
 
 \subsubsection{Sequence}
 \tacindex{;}
-\index{;@{\tt ;}}
 \index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}}
 
-\begin{tabbing}
+A sequence is an expression of the following form:
+\begin{quote}
 {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
-\end{tabbing}
+\end{quote}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
 $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 associating.
 
 \subsubsection{General sequence}
-
 \tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}
-\tacindex{; [ | ]}
-\index{; [ | ]@{\tt ;[\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$]}}
 
-
 We can generalize the previous sequence operator as
-\begin{tabbing}
+\begin{quote}
 {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
 {\tacexpr}$_n$ {\tt ]}
-\end{tabbing}
+\end{quote}
 {\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is
 applied and $v_i$ is applied to the $i$-th generated subgoal by the
 application of $v_0$, for $=1,...,n$. It fails if the application of
@@ -277,9 +271,9 @@ $v_0$ does not generate exactly $n$ subgoals.
 \index{Tacticals!do@{\tt do}}
 
 There is a for loop that repeats a tactic {\num} times:
-\begin{tabbing}
+\begin{quote}
 {\tt do} {\num} {\tacexpr}
-\end{tabbing}
+\end{quote}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied {\num} times. Supposing ${\num}>1$, after the first
 application of $v$, $v$ is applied, at least once, to the generated
@@ -291,9 +285,9 @@ the {\num} applications have been completed.
 \index{Tacticals!repeat@{\tt repeat}}
 
 We have a repeat loop with:
-\begin{tabbing}
+\begin{quote}
 {\tt repeat} {\tacexpr}
-\end{tabbing}
+\end{quote}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied until it fails. Supposing $n>1$, after the first application
 of $v$, $v$ is applied, at least once, to the generated subgoals and
@@ -305,9 +299,9 @@ fails.
 \index{Tacticals!try@{\tt try}}
 
 We can catch the tactic errors with:
-\begin{tabbing}
+\begin{quote}
 {\tt try} {\tacexpr}
-\end{tabbing}
+\end{quote}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied. If the application of $v$ fails, it catches the error and
 leaves the goal unchanged. If the level of the exception is positive,
@@ -317,9 +311,9 @@ then the exception is re-raised with its level decremented.
 \tacindex{progress}
 
 We can check if a tactic made progress with:
-\begin{tabbing}
+\begin{quote}
 {\tt progress} {\tacexpr}
-\end{tabbing}
+\end{quote}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied. If the application of $v$ produced one subgoal equal to the
 initial goal (up to syntactical equality), then an error of level 0 is
@@ -328,13 +322,13 @@ raised.
 \ErrMsg \errindex{Failed to progress}
 
 \subsubsection{Branching}
-\tacindex{||}
-\index{Tacticals!orelse@{\tt ||}}
+\tacindex{$\mid\mid$}
+\index{Tacticals!orelse@{\tt $\mid\mid$}}
 
 We can easily branch with the following structure:
-\begin{tabbing}
+\begin{quote}
 {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$
-\end{tabbing}
+\end{quote}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
 $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if
 it fails then $v_2$ is applied. Branching is left associating.
@@ -345,9 +339,9 @@ it fails then $v_2$ is applied. Branching is left associating.
 
 We may consider the first tactic to work (i.e. which does not fail) among a
 panel of tactics:
-\begin{tabbing}
+\begin{quote}
 {\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
-\end{tabbing}
+\end{quote}
 {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for 
 $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it works, it stops else it
 tries to apply $v_2$ and so on. It fails when there is no applicable tactic.
@@ -360,9 +354,9 @@ tries to apply $v_2$ and so on. It fails when there is no applicable tactic.
 
 We may consider the first to solve (i.e. which generates no subgoal) among a
 panel of tactics:
-\begin{tabbing}
+\begin{quote}
 {\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
-\end{tabbing}
+\end{quote}
 {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for 
 $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it solves, it stops else it
 tries to apply $v_2$ and so on. It fails if there is no solving tactic.
@@ -375,9 +369,9 @@ tries to apply $v_2$ and so on. It fails if there is no solving tactic.
 
 The constant {\tt idtac} is the identity tactic: it leaves any goal
 unchanged but it appears in the proof script.
-\begin{tabbing}
+\begin{quote}
 {\tt idtac} and {\tt idtac "message"}
-\end{tabbing}
+\end{quote}
 The latter variant prints the string on the standard output.
 
 
@@ -388,9 +382,9 @@ The latter variant prints the string on the standard output.
 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
 catched by {\tt try} or {\tt match goal}. There are three variants:
-\begin{tabbing}
+\begin{quote}
 {\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"}
-\end{tabbing}
+\end{quote}
 The number $n$ is the failure level. If no level is specified, it
 defaults to $0$.  The level is used by {\tt try} and {\tt match goal}.
 If $0$, it makes {\tt match goal} considering the next clause
@@ -406,13 +400,13 @@ If $0$, it makes {\tt match goal} considering the next clause
 \index{let rec!in Ltac}
 
 Local definitions can be done as follows:
-\begin{tabbing}
+\begin{quote}
 {\tt let} {\ident}$_1$ {\tt :=} {\tacexpr}$_1$\\
 {\tt with} {\ident}$_2$ {\tt :=} {\tacexpr}$_2$\\
 ...\\
 {\tt with} {\ident}$_n$ {\tt :=} {\tacexpr}$_n$ {\tt in}\\
 {\tacexpr}
-\end{tabbing}
+\end{quote}
 each {\tacexpr}$_i$ is evaluated to $v_i$, then, {\tacexpr} is
 evaluated by substituting $v_i$ to each occurrence of {\ident}$_i$,
 for $i=1,...,n$. There is no dependencies between the {\tacexpr}$_i$
@@ -425,9 +419,9 @@ argument is required.
 \subsubsection{Application}
 
 An application is an expression of the following form:
-\begin{tabbing}
+\begin{quote}
 {\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$
-\end{tabbing}
+\end{quote}
 The reference {\qualid} must be bound to some defined tactic
 definition expecting at least $n$ arguments.  The expressions
 {\tacexpr}$_i$ are evaluated to $v_i$, for $i=1,...,n$.
@@ -444,9 +438,9 @@ definition expecting at least $n$ arguments.  The expressions
 
 A parameterized tactic can be built anonymously (without resorting to
 local definitions) with:
-\begin{tabbing}
+\begin{quote}
 {\tt fun} {\ident${}_1$} ... {\ident${}_n$} {\tt =>} {\tacexpr}
-\end{tabbing}
+\end{quote}
 Indeed, local definitions of functions are a syntactic sugar for
 binding a {\tt fun} tactic to an identifier.
 
@@ -455,7 +449,7 @@ binding a {\tt fun} tactic to an identifier.
 \index{match!in Ltac}
 
 We can carry out pattern matching on terms with:
-\begin{tabbing}
+\begin{quote}
 {\tt match} {\tacexpr} {\tt with}\\
 ~~~{\cpattern}$_1$ {\tt =>} {\tacexpr}$_1$\\
 ~{\tt |} {\cpattern}$_2$ {\tt =>} {\tacexpr}$_2$\\
@@ -463,7 +457,7 @@ We can carry out pattern matching on terms with:
 ~{\tt |} {\cpattern}$_n$ {\tt =>} {\tacexpr}$_n$\\
 ~{\tt |} {\tt \_} {\tt =>} {\tacexpr}$_{n+1}$\\
 {\tt end}
-\end{tabbing}
+\end{quote}
 The {\tacexpr} is evaluated and should yield a term which is matched
 (non-linear first order unification) against {\cpattern}$_1$ then
 {\tacexpr}$_1$ is evaluated into some value by substituting the
@@ -490,9 +484,9 @@ then a no-matching error is raised.
 \index{context!in pattern}
 There is a special form of patterns to match a subterm against the
 pattern:
-\begin{tabbing}
+\begin{quote}
 {\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}
-\end{tabbing}
+\end{quote}
 It matches any term which one subterm matches {\cpattern}. If there is
 a match, the optional {\ident} is assign the ``matched context'', that
 is the initial term where the matched subterm is replaced by a
@@ -512,6 +506,7 @@ the order of matching is left unspecified.
 \index{match reverse goal!in Ltac}
 
 We can make pattern matching on goals using the following expression:
+\begin{quote}
 \begin{tabbing}
 {\tt match goal with}\\
 ~~\={\tt |} $hyp_{1,1}${\tt ,}...{\tt ,}$hyp_{1,m_1}$
@@ -524,7 +519,7 @@ We can make pattern matching on goals using the following expression:
   \>{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\
 {\tt end}
 \end{tabbing}
-
+\end{quote}
 
 % TODO: specify order of hypothesis and explain reverse...
 
@@ -563,9 +558,9 @@ the {\tt match reverse goal with} variant.
 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
 expressions:
-\begin{tabbing}
+\begin{quote}
 {\tt context} {\ident} {\tt [} {\tacexpr} {\tt ]}
-\end{tabbing}
+\end{quote}
 {\ident} must denote a context variable bound by a {\tt context}
 pattern of a {\tt match} expression. This expression evaluates
 replaces the hole of the value of {\ident} by the value of
@@ -583,9 +578,9 @@ the system decide a name with the {\tt intro} tactic is not so good
 since it is very awkward to retrieve the name the system gave.
 
 As before, the following expression returns a term:
-\begin{tabbing}
+\begin{quote}
 {\tt fresh} {\qstring}
-\end{tabbing}
+\end{quote}
 It evaluates to an identifier unbound in the goal, which is obtained
 by padding {\qstring} with a number if necessary. If no name is given,
 the prefix is {\tt H}.
@@ -602,9 +597,9 @@ This tactic computes the type of {\term}.
 \index{eval!in Ltac}
 
 Evaluation of a term can be performed with:
-\begin{tabbing}
+\begin{quote}
 {\tt eval} {\nterm{redexpr}} {\tt in} {\term}
-\end{tabbing}
+\end{quote}
 where \nterm{redexpr} is a reduction tactic among {\tt red}, {\tt
 hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold},
 {\tt fold}, {\tt pattern}.
@@ -640,7 +635,7 @@ without having to cut manually the proof in smaller lemmas.
 
 \ErrMsg \errindex{Proof is not complete}
 
-\subsection{Tactic toplevel definitions}
+\section{Tactic toplevel definitions}
 \comindex{Ltac}
 
 Basically, tactics toplevel definitions are made as follows:
@@ -650,21 +645,21 @@ Basically, tactics toplevel definitions are made as follows:
 %script is evaluated by substituting $v$ to {\ident}.
 %
 %We can define functional definitions by:\\
-\begin{tabbing}
+\begin{quote}
 {\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=}
 {\tacexpr}
-\end{tabbing}
+\end{quote}
 This defines a new tactic that can be used in any tactic script or new
 tactic toplevel definition.
 
 \Rem The preceding definition can equivalently be written:
-\begin{tabbing}
+\begin{quote}
 {\tt Ltac} {\ident} {\tt := fun} {\ident}$_1$ ... {\ident}$_n$
 {\tt =>} {\tacexpr}
-\end{tabbing}
+\end{quote}
 Recursive and mutual recursive function definitions are also
 possible with the syntax:
-\begin{tabbing}
+\begin{quote}
 {\tt Ltac} {\ident}$_1$ {\ident}$_{1,1}$ ...
 {\ident}$_{1,m_1}$~~{\tt :=} {\tacexpr}$_1$\\
 {\tt with} {\ident}$_2$ {\ident}$_{2,1}$ ... {\ident}$_{2,m_2}$~~{\tt :=}
@@ -672,7 +667,7 @@ possible with the syntax:
 ...\\
 {\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=}
 {\tacexpr}$_n$
-\end{tabbing}
+\end{quote}
 
 %This definition bloc is a set of definitions (use of
 %the same previous syntactical sugar) and the other scripts are evaluated as
@@ -681,44 +676,6 @@ possible with the syntax:
 
 \endinput
 
-\section{Examples}
-
-\subsection{About the cardinality of the natural number set}
-
-\begin{figure}
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
-\begin{coq_eval}
-Reset Initial.
-Require Import Arith.
-Require Import List.
-\end{coq_eval}
-\begin{coq_example*}
-Lemma card_nat :
- ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z).
-Proof.
-red; intros (x, (y, Hy)).
-elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
- match goal with
- | [_:(?a = ?b),_:(?a = ?c) |- _ ] =>
-     cut (b = c); [ discriminate | apply trans_equal with a; auto ]
- end.
-Qed.
-\end{coq_example*}
-\end{minipage}}
-\end{center}
-\caption{A proof on cardinality of natural numbers}
-\label{cnatltac}
-\end{figure}
-
-A first example which shows how to use the pattern matching over the proof
-contexts is the proof that natural numbers have more than two elements. The
-proof of such a lemma can be done as shown in table~\ref{cnatltac}.
-
-We can notice that all the (very similar) cases coming from the three
-eliminations (with three distinct natural numbers) are successfully solved by
-a {\tt match goal} structure and, in particular, with only one pattern (use
-of non-linear matching).
 
 \subsection{Permutation on closed lists}
 
@@ -737,7 +694,6 @@ Inductive permut : list A -> list A -> Prop :=
       forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2.
 End Sort.
 \end{coq_example*}
-\end{minipage}}
 \end{center}
 \caption{Definition of the permutation predicate}
 \label{permutpred}
@@ -746,8 +702,8 @@ End Sort.
 
 Another more complex example is the problem of permutation on closed
 lists. The aim is to show that a closed list is a permutation of
-another one.  First, we define the permutation predicate as shown in
-table~\ref{permutpred}.
+another one.  First, we define the permutation predicate as shown on
+Figure~\ref{permutpred}.
  
 \begin{figure}[p]
 \begin{center}
@@ -806,8 +762,8 @@ Qed.
 \label{permutlem}
 \end{figure}
 
-Next, we can write naturally the tactic and the result can be seen in
-table~\ref{permutltac}. We can notice that we use two toplevel
+Next, we can write naturally the tactic and the result can be seen on
+Figure~\ref{permutltac}. We can notice that we use two toplevel
 definitions {\tt PermutProve} and {\tt Permut}. The function to be
 called is {\tt PermutProve} which computes the lengths of the two
 lists and calls {\tt Permut} with the length if the two lists have the
@@ -823,7 +779,7 @@ an argument for {\tt Permut} and this length is decremented for each
 rotation down to, but not including, 1 because for a list of length
 $n$, we can make exactly $n-1$ rotations to generate at most $n$
 distinct lists. Here, it must be noticed that we use the natural
-numbers of {\Coq} for the rotation counter. In table~\ref{ltac}, we
+numbers of {\Coq} for the rotation counter. On Figure~\ref{ltac}, we
 can see that it is possible to use usual natural numbers but they are
 only used as arguments for primitive tactics and they cannot be
 handled, in particular, we cannot make computations with them. So, a
@@ -831,13 +787,13 @@ natural choice is to use {\Coq} data structures so that {\Coq} makes
 the computations (reductions) by {\tt eval compute in} and we can get
 the terms back by {\tt match}.
 
-With {\tt PermutProve}, we can now prove lemmas such those shown in
-table~\ref{permutlem}.
+With {\tt PermutProve}, we can now prove lemmas such those shown on
+Figure~\ref{permutlem}.
 
 
 \subsection{Deciding intuitionistic propositional logic}
 
-\begin{figure}[b]
+\begin{figure}[tbp]
 \begin{center}
 \fbox{\begin{minipage}{0.95\textwidth}
 \begin{coq_example}
@@ -913,10 +869,10 @@ backtracking when returning tactic values. An interesting application
 is the problem of deciding intuitionistic propositional logic.
 Considering the contraction-free sequent calculi {\tt LJT*} of
 Roy~Dyckhoff (\cite{Dyc92}), it is quite natural to code such a tactic
-using the tactic language. In Table~\ref{tautoltaca}, the tactic {\tt
+using the tactic language. On Figure~\ref{tautoltaca}, the tactic {\tt
   Axioms} tries to conclude using usual axioms. The {\tt DSimplif}
 tactic applies all the reversible rules of Dyckhoff's system.
-Finally, in Table~\ref{tautoltacb}, the {\tt TautoProp} tactic (the
+Finally, on Figure~\ref{tautoltacb}, the {\tt TautoProp} tactic (the
 main tactic to be called) simplifies with {\tt DSimplif}, tries to
 conclude with {\tt Axioms} and tries several paths using the
 backtracking rules (one of the four Dyckhoff's rules for the left
@@ -943,8 +899,8 @@ Qed.
 \label{tautolem}
 \end{figure}
 
-For example, with {\tt TautoProp}, we can prove tautologies like those in
-table~\ref{tautolem}.
+For example, with {\tt TautoProp}, we can prove tautologies like those of
+Figure~\ref{tautolem}.
 
 
 \subsection{Deciding type isomorphisms}
@@ -953,7 +909,7 @@ A more tricky problem is to decide equalities between types and modulo
 isomorphisms. Here, we choose to use the isomorphisms of the simply typed
 $\lb{}$-calculus with Cartesian product and $unit$ type (see, for example,
 \cite{RC95}). The axioms of this $\lb{}$-calculus are given by
-table~\ref{isosax}.
+Figure~\ref{isosax}.
 
 \begin{figure}
 \begin{center}
@@ -985,7 +941,7 @@ End Iso_axioms.
 \end{figure}
 
 The tactic to judge equalities modulo this axiomatization can be written as
-shown in tables~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite
+shown on Figures~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite
 simple. Types are reduced using axioms that can be oriented (this done by {\tt
 MainSimplif}). The normal forms are sequences of Cartesian
 products without Cartesian product in the left component. These normal forms
@@ -1068,7 +1024,7 @@ Ltac IsoProve := MainSimplif; CompareStruct.
 \label{isosltac2}
 \end{figure}
 
-Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
+Figure~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
 
 \begin{figure}
 \begin{center}
diff --git a/doc/RefMan-mod.tex b/doc/RefMan-mod.tex
index 1999d47dd..490d21fd8 100644
--- a/doc/RefMan-mod.tex
+++ b/doc/RefMan-mod.tex
@@ -1,13 +1,12 @@
-\section{Module system}
+\section{Module system
 \index{Modules}
-\label{section:Modules}
+\label{section:Modules}}
 
 The module system provides a way of packaging related elements
 together, as well as a mean of massive abstraction.
 
 \begin{figure}[t]
-\begin{center}
-\fbox{\begin{minipage}{0.95\textwidth}
+\begin{centerframe}
 \begin{tabular}{rcl}
 {\modtype}  & ::= & {\ident} \\
  & $|$ & {\modtype} \texttt{ with Definition }{\ident} := {\term} \\
@@ -22,13 +21,12 @@ together, as well as a mean of massive abstraction.
 
 {\modexpr} & ::= & \nelist{\qualid}{} 
 \end{tabular}
-\end{minipage}}
-\end{center}
-\caption{Syntax of modules.}
+\end{centerframe}
+\caption{Syntax of modules}
 \end{figure}
 
-\subsection{\tt Module {\ident}}
-\comindex{Module}
+\subsection{\tt Module {\ident}
+\comindex{Module}}
 
 This command is used to start an interactive module named {\ident}.
 
@@ -59,8 +57,8 @@ This command is used to start an interactive module named {\ident}.
 
 \end{Variants}
 
-\subsection{\tt End {\ident}}
-\comindex{End}
+\subsection{\tt End {\ident}
+\comindex{End}}
 
 This command closes the interactive module {\ident}. If the module type
 was given the content of the module is matched against it and an error
@@ -75,8 +73,8 @@ now available through the dot notation.
 \end{ErrMsgs}
 
 
-\subsection{\tt Module {\ident} := {\modexpr}}
-\comindex{Module}
+\subsection{\tt Module {\ident} := {\modexpr}
+\comindex{Module}}
 
 This command defines the module identifier {\ident} to be equal to
 {\modexpr}. 
@@ -108,7 +106,8 @@ This command defines the module identifier {\ident} to be equal to
 
 \end{Variants}
 
-\subsection{\tt Module Type {\ident}}\comindex{Module Type}
+\subsection{\tt Module Type {\ident}
+\comindex{Module Type}}
 
 This command is used to start an interactive module type {\ident}.
 
@@ -120,8 +119,8 @@ This command is used to start an interactive module type {\ident}.
 
 \end{Variants}
 
-\subsection{\tt End {\ident}}
-\comindex{End}
+\subsection{\tt End {\ident}
+\comindex{End}}
 
 This command closes the interactive module type {\ident}.
 
@@ -141,6 +140,7 @@ Defines a module type {\ident} equal to {\modtype}.
 \end{Variants}
 
 \subsection{\tt Declare Module {\ident}}
+
 Starts an interactive module declaration. This command is available
 only in module types. 
 
@@ -329,7 +329,10 @@ Reset Initial.
 
 \end{Remarks}
 
-\subsection{Import {\qualid}}\comindex{Import}\label{Import}
+\subsection{Import {\qualid}
+\comindex{Import}
+\label{Import}}
+
 If {\qualid} denotes a valid basic module (i.e. its module type is a
 signature), makes its components available by their short names.
 
@@ -371,13 +374,13 @@ Reset Mod.
   \item Warning: Trying to mask the absolute name {\qualid} !
 \end{Warnings}
 
-\subsection{\tt Print Module {\ident}}
-\comindex{Print Module}
+\subsection{\tt Print Module {\ident}
+\comindex{Print Module}}
 
 Prints the module type and (optionally) the body of the module {\ident}.
 
-\subsection{\tt Print Module Type {\ident}}
-\comindex{Print Module Type}
+\subsection{\tt Print Module Type {\ident}
+\comindex{Print Module Type}}
 
 Prints the module type corresponding to {\ident}.
 
diff --git a/doc/RefMan-modr.tex b/doc/RefMan-modr.tex
index 055e2313f..66895f204 100644
--- a/doc/RefMan-modr.tex
+++ b/doc/RefMan-modr.tex
@@ -77,8 +77,8 @@ module type $T_2$.
   $\Spec_1$ is more precise that a specification $\Spec_2$.
 \end{itemize}
 The rules for forming module types are the following:
-\begin{itemize}
-\item [] WF-SIG
+\begin{description}
+\item[WF-SIG]
 \inference{%
   \frac{
     \WF{E;E'}{}
@@ -86,7 +86,7 @@ The rules for forming module types are the following:
     \WFT{E}{\sig{E'}}
   }
 }
-\item [] WF-FUN
+\item[WF-FUN]
 \inference{%
   \frac{
     \WFT{E;\ModS{X}{T}}{T'}
@@ -94,10 +94,10 @@ The rules for forming module types are the following:
     \WFT{E}{\funsig{X}{T}{T'}}
   }
 }
-\end{itemize}
+\end{description}
 Rules for typing module expressions:
-\begin{itemize}
-\item [] MT-STRUCT
+\begin{description}
+\item[MT-STRUCT]
 \inference{%
   \frac{
     \begin{array}{c}
@@ -109,7 +109,7 @@ Rules for typing module expressions:
     \WTM{E}{\struct{\Impl_1;\dots;\Impl_n}}{\sig{\Spec_1;\dots;\Spec_n}}
   }
 }
-\item [] MT-FUN
+\item[MT-FUN]
 \inference{%
   \frac{
     \WTM{E;\ModS{X}{T}}{M}{T'}
@@ -117,7 +117,7 @@ Rules for typing module expressions:
     \WTM{E}{\functor{X}{T}{M}}{\funsig{X}{T}{T'}}
   }
 }
-\item [] MT-APP
+\item[MT-APP]
 \inference{%
   \frac{
     \begin{array}{c}
@@ -129,7 +129,7 @@ Rules for typing module expressions:
     \WTM{E}{p\; p_1 \dots p_n}{T'\{X_1/p_1\dots X_n/p_n\}}
   }
 }
-\item [] MT-SUB
+\item[MT-SUB]
 \inference{%
   \frac{
     \WTM{E}{M}{T}~~~~~~~~~~~~\WS{E}{T}{T'}
@@ -137,7 +137,7 @@ Rules for typing module expressions:
     \WTM{E}{M}{T'}
   }
 }
-\item [] MT-STR
+\item[MT-STR]
 \inference{%
   \frac{
     \WTM{E}{p}{T}
@@ -145,7 +145,7 @@ Rules for typing module expressions:
     \WTM{E}{p}{T/p}
   }
 }
-\end{itemize}
+\end{description}
 The last rule, called strengthening is used to make all module fields
 manifestly equal to themselves. The notation $T/p$ has the following
 meaning:
@@ -174,8 +174,8 @@ for $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$ below as well as
 the equality rules on inductive types and constructors. 
 
 The module subtyping rules:
-\begin{itemize}
-\item[] MSUB-SIG
+\begin{description}
+\item[MSUB-SIG]
 \inference{%
   \frac{
     \begin{array}{c}
@@ -187,7 +187,7 @@ The module subtyping rules:
     \WS{E}{\sig{\Spec_1;\dots;\Spec_n}}{\sig{\Spec'_1;\dots;\Spec'_m}}
   }
 }
-\item[] MSUB-FUN
+\item[MSUB-FUN]
 \inference{%       T_1 -> T_2 <: T_1' -> T_2'
   \frac{
     \WS{E}{T_1'}{T_1}~~~~~~~~~~\WS{E;\ModS{X}{T_1'}}{T_2}{T_2'}
@@ -196,7 +196,7 @@ The module subtyping rules:
   }
 }
 % these are derived rules
-% \item[] MSUB-EQ
+% \item[MSUB-EQ]
 % \inference{%
 %   \frac{
 %     \WS{E}{T_1}{T_2}~~~~~~~~~~\WTERED{}{T_1}{=}{T_1'}~~~~~~~~~~\WTERED{}{T_2}{=}{T_2'}
@@ -204,7 +204,7 @@ The module subtyping rules:
 %     \WS{E}{T_1'}{T_2'}
 %   }
 % }
-% \item[] MSUB-REFL
+% \item[MSUB-REFL]
 % \inference{%
 %   \frac{
 %     \WFT{E}{T}
@@ -212,10 +212,10 @@ The module subtyping rules:
 %     \WS{E}{T}{T}
 %   }
 % }
-\end{itemize}
+\end{description}
 Specification subtyping rules:
-\begin{itemize}
-\item []ASSUM-ASSUM
+\begin{description}
+\item[ASSUM-ASSUM]
 \inference{%
   \frac{
     \WTELECONV{}{U_1}{U_2}
@@ -223,7 +223,7 @@ Specification subtyping rules:
     \WSE{\Assum{}{c}{U_1}}{\Assum{}{c}{U_2}}
   }
 }
-\item []DEF-ASSUM
+\item[DEF-ASSUM]
 \inference{%
   \frac{
     \WTELECONV{}{U_1}{U_2}
@@ -231,7 +231,7 @@ Specification subtyping rules:
     \WSE{\Def{}{c}{U_1}{t}}{\Assum{}{c}{U_2}}
   }
 }
-\item []ASSUM-DEF
+\item[ASSUM-DEF]
 \inference{%
   \frac{
     \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{c}{t_2}
@@ -239,7 +239,7 @@ Specification subtyping rules:
     \WSE{\Assum{}{c}{U_1}}{\Def{}{c}{U_2}{t_2}}
   }
 }
-\item []DEF-DEF
+\item[DEF-DEF]
 \inference{%
   \frac{
     \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{t_1}{t_2}
@@ -247,7 +247,7 @@ Specification subtyping rules:
     \WSE{\Def{}{c}{U_1}{t_1}}{\Def{}{c}{U_2}{t_2}}
   }
 }
-\item []IND-IND
+\item[IND-IND]
 \inference{%
   \frac{
     \WTECONV{}{\Gamma_P}{\Gamma_P'}%
@@ -258,7 +258,7 @@ Specification subtyping rules:
         {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
   }
 }
-\item []INDP-IND
+\item[INDP-IND]
 \inference{%
   \frac{
     \WTECONV{}{\Gamma_P}{\Gamma_P'}%
@@ -269,7 +269,7 @@ Specification subtyping rules:
         {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
   }
 }
-\item []INDP-INDP
+\item[INDP-INDP]
 \inference{%
   \frac{
     \WTECONV{}{\Gamma_P}{\Gamma_P'}%
@@ -282,7 +282,7 @@ Specification subtyping rules:
   }
 }
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\item []MODS-MODS
+\item[MODS-MODS]
 \inference{%
   \frac{
     \WSE{T_1}{T_2}
@@ -290,7 +290,7 @@ Specification subtyping rules:
     \WSE{\ModS{m}{T_1}}{\ModS{m}{T_2}}
   }
 }
-\item []MODEQ-MODS
+\item[MODEQ-MODS]
 \inference{%
   \frac{
     \WSE{T_1}{T_2}
@@ -298,7 +298,7 @@ Specification subtyping rules:
     \WSE{\ModSEq{m}{T_1}{p}}{\ModS{m}{T_2}}
   }
 }
-\item []MODS-MODEQ
+\item[MODS-MODEQ]
 \inference{%
   \frac{
     \WSE{T_1}{T_2}~~~~~~~~\WTECONV{}{m}{p_2}
@@ -306,7 +306,7 @@ Specification subtyping rules:
     \WSE{\ModS{m}{T_1}}{\ModSEq{m}{T_2}{p_2}}
   }
 }
-\item []MODEQ-MODEQ
+\item[MODEQ-MODEQ]
 \inference{%
   \frac{
     \WSE{T_1}{T_2}~~~~~~~~\WTECONV{}{p_1}{p_2}
@@ -314,7 +314,7 @@ Specification subtyping rules:
     \WSE{\ModSEq{m}{T_1}{p_1}}{\ModSEq{m}{T_2}{p_2}}
   }
 }
-\item []MODTYPE-MODTYPE
+\item[MODTYPE-MODTYPE]
 \inference{%
   \frac{
     \WSE{T_1}{T_2}~~~~~~~~\WSE{T_2}{T_1}
@@ -322,10 +322,10 @@ Specification subtyping rules:
     \WSE{\ModType{S}{T_1}}{\ModType{S}{T_2}}
   }
 }
-\end{itemize}
+\end{description}
 Verification of the specification
-\begin{itemize}
-\item []IMPL-SPEC
+\begin{description}
+\item[IMPL-SPEC]
 \inference{%
   \frac{
     \begin{array}{c}
@@ -336,7 +336,7 @@ Verification of the specification
     \WTE{}{\Spec}{\Spec}
   }
 }
-\item []MOD-MODS
+\item[MOD-MODS]
 \inference{%
   \frac{
     \WF{E;\ModS{m}{T}}{}~~~~~~~~\WTE{}{M}{T}
@@ -344,7 +344,7 @@ Verification of the specification
     \WTE{}{\Mod{m}{T}{M}}{\ModS{m}{T}}
   }
 }
-\item []MOD-MODEQ
+\item[MOD-MODEQ]
 \inference{%
   \frac{
     \WF{E;\ModSEq{m}{T}{p}}{}~~~~~~~~~~~\WTECONV{}{p}{p'}
@@ -352,11 +352,10 @@ Verification of the specification
     \WTE{}{\Mod{m}{T}{p'}}{\ModSEq{m}{T}{p'}}
   }
 }
-
-\end{itemize}
+\end{description}
 New environment formation rules
-\begin{itemize}
-\item []WF-MODS
+\begin{description}
+\item[WF-MODS]
 \inference{%
   \frac{
     \WF{E}{}~~~~~~~~\WFT{E}{T}
@@ -364,7 +363,7 @@ New environment formation rules
     \WF{E;\ModS{m}{T}}{}
   }
 }
-\item []WF-MODEQ
+\item[WF-MODEQ]
 \inference{%
   \frac{
     \WF{E}{}~~~~~~~~~~~\WTE{}{p}{T}
@@ -372,7 +371,7 @@ New environment formation rules
     \WF{E,\ModSEq{m}{T}{p}}{}
   }
 }
-\item []WF-MODTYPE
+\item[WF-MODTYPE]
 \inference{%
   \frac{
     \WF{E}{}~~~~~~~~~~~\WFT{E}{T}
@@ -380,7 +379,7 @@ New environment formation rules
     \WF{E,\ModType{S}{T}}{}
   }
 }
-\item []WF-IND
+\item[WF-IND]
 \inference{%
   \frac{
     \begin{array}{c}
@@ -390,13 +389,13 @@ New environment formation rules
       \in \lab{Spec_1;\dots;Spec_n}}}{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}
     \end{array}
   }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-    \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}\\
+    \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
   }
 }
-\end{itemize}
+\end{description}
 Component access rules
-\begin{itemize}
-\item []ACC-TYPE
+\begin{description}
+\item[ACC-TYPE]
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Assum{}{c}{U};\dots}}
@@ -404,7 +403,7 @@ Component access rules
     \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\item []
+\\
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{U}{t};\dots}}
@@ -412,9 +411,9 @@ Component access rules
     \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\item[] Notice that the following rule extends the delta rule defined in
+\item[ACC-DELTA]
+Notice that the following rule extends the delta rule defined in
 section~\ref{delta}
-\item [] ACC-DELTA
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{U}{t};\dots}}
@@ -422,10 +421,11 @@ section~\ref{delta}
     \WTEGRED{p.c}{\triangleright_\delta}{\subst{t}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\item [] in the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
+\\
+In the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
   $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
   $[c_1:C_1;\ldots;c_n:C_n]$
-\item []ACC-IND
+\item[ACC-IND]
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;\Spec_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
@@ -441,7 +441,7 @@ section~\ref{delta}
        p_r)}_{j=1\ldots k}}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\item []ACC-INDP
+\item[ACC-INDP]
 \inference{%
   \frac{
     \WT{E}{}{p}{\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
@@ -457,7 +457,7 @@ section~\ref{delta}
   }
 }
 %%%%%%%%%%%%%%%%%%%%%%%%%%% MODULES
-\item []ACC-MOD
+\item[ACC-MOD]
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModS{m}{T};\dots}}
@@ -465,7 +465,7 @@ section~\ref{delta}
     \WTEG{p.m}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\item []
+\\
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModSEq{m}{T}{p'};\dots}}
@@ -473,7 +473,7 @@ section~\ref{delta}
     \WTEG{p.m}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\item []ACC-MODEQ
+\item[ACC-MODEQ]
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModSEq{m}{T}{p'};\dots}}
@@ -481,7 +481,7 @@ section~\ref{delta}
     \WTEGRED{p.m}{\triangleright_\delta}{\subst{p'}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\item []ACC-MODTYPE
+\item[ACC-MODTYPE]
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModType{S}{T};\dots}}
@@ -489,7 +489,7 @@ section~\ref{delta}
     \WTEGRED{p.S}{\triangleright_\delta}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\end{itemize}
+\end{description}
 The function $\lab{}$ is used to calculate the set of label of
 the set of specifications. It is defined by
 $\lab{\Spec_1;\dots;\Spec_n}=\lab{\Spec_1}\cup\dots;\cup\lab{\Spec_n}$
@@ -504,8 +504,8 @@ where $\lab{\Spec}$ is defined as follows:
 \item $\lab{\ModType{S}{T}}=\{S\}$
 \end{itemize}
 Environment access for modules and module types
-\begin{itemize}
-\item []ENV-MOD
+\begin{description}
+\item[ENV-MOD]
 \inference{%
   \frac{
     \WF{E;\ModS{m}{T};E'}{\Gamma}
@@ -513,7 +513,7 @@ Environment access for modules and module types
     \WT{E;\ModS{m}{T};E'}{\Gamma}{m}{T}
   }
 }
-\item []
+\item[]
 \inference{%
   \frac{
     \WF{E;\ModSEq{m}{T}{p};E'}{\Gamma}
@@ -521,7 +521,7 @@ Environment access for modules and module types
     \WT{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{T}
   }
 }
-\item []ENV-MODEQ
+\item[ENV-MODEQ]
 \inference{%
   \frac{
     \WF{E;\ModSEq{m}{T}{p};E'}{\Gamma}
@@ -529,7 +529,7 @@ Environment access for modules and module types
     \WTRED{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{\triangleright_\delta}{p}
   }
 }
-\item []ENV-MODTYPE
+\item[ENV-MODTYPE]
 \inference{%
   \frac{
     \WF{E;\ModType{S}{T};E'}{\Gamma}
@@ -537,7 +537,7 @@ Environment access for modules and module types
     \WTRED{E;\ModType{S}{T};E'}{\Gamma}{S}{\triangleright_\delta}{T}
   }
 }
-\item []ENV-INDP
+\item[ENV-INDP]
 \inference{%
   \frac{
     \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
@@ -552,7 +552,7 @@ Environment access for modules and module types
     \WTRED{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}{c_i}{\triangleright_\delta}{p.c_i}
   }
 }
-\end{itemize}
+\end{description}
 % %%% replaced by \triangle_\delta
 % Module path equality is a transitive and reflexive closure of the
 % relation generated by ACC-MODEQ and ENV-MODEQ.
diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex
index 3603c95b2..11cc8ce5c 100755
--- a/doc/RefMan-pre.tex
+++ b/doc/RefMan-pre.tex
@@ -450,11 +450,11 @@ integer numbers. Finally, the names of the standard properties of
 numbers now follow a standard pattern and the symbolic
 notations for the standard definitions as well.
 
-The fourth point is the release of \CoqIde{}, a new graphical
+The fourth point is the release of \CoqIDE{}, a new graphical
 gtk2-based interface fully integrated to {\Coq}. Close in style from
 the Proof General Emacs interface, it is faster and its integration
 with {\Coq} makes interactive developments more friendly. All
-mathematical Unicode symbols are usable within \CoqIde{}.
+mathematical Unicode symbols are usable within \CoqIDE{}.
 
 Finally, the module system of {\Coq} completes the picture of {\Coq}
 version 8.0. Though released with an experimental status in the previous
@@ -483,7 +483,7 @@ tactic for solving first-order statements in presence of inductive
 types. He is also the maintainer of the non-domain specific automation
 tactics.
 
-Benjamin Monate is the developer of the \CoqIde{} graphical
+Benjamin Monate is the developer of the \CoqIDE{} graphical
 interface with contributions by Jean-Christophe Filliâtre, Pierre
 Letouzey and Claude Marché.
 
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index 6872f971d..12ca5fc10 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -340,35 +340,28 @@ where "n + m" := (plus n m).
 \subsection{Displaying informations about notations}
 
 To deactivate the printing of all notations, use the command
-
-\medskip
-{\tt Unset Printing Notation}.
-\medskip
-
+\begin{quote}
+\tt Unset Printing Notation.
+\end{quote}
 To reactivate it, use the command
-
-\medskip
-{\tt Set Printing Notation}.
-\medskip
-
+\begin{quote}
+\tt Set Printing Notation.
+\end{quote}
 The default is to use notations for printing terms wherever possible.
 
-\subsection{Locating notations}
+\subsection{Locating notations
 \comindex{Locate}
-\label{LocateSymbol}
+\label{LocateSymbol}}
 
 To know to which notations a given symbol belongs to, use the command
-
-\bigskip
-{\tt Locate {\symbolentry}}
-\bigskip
-
+\begin{quote}
+\tt Locate {\symbolentry}
+\end{quote}
 where symbol is any (composite) symbol surrounded by quotes. To locate
 a particular notation, use a string where the variables of the
 notation are replaced by ``\_''.
 
 \Example
-
 \begin{coq_example}
 Locate "exists".
 Locate "'exists' _ , _".
@@ -377,17 +370,17 @@ Locate "'exists' _ , _".
 \SeeAlso Section \ref{Locate}.
 
 \begin{figure}
-\begin{tabular}{|lcl|}
-\hline
+\begin{centerframe}
+\begin{tabular}{lcl}
 {\sentence} & ::= &
    \texttt{Notation} \zeroone{\tt Local} {\str} \texttt{:=} {\term} 
-   \zeroone{\modifiers} \zeroone{:{\scope}} \verb=.=\\
+   \zeroone{\modifiers} \zeroone{:{\scope}} .\\
   & $|$ & 
    \texttt{Infix} \zeroone{\tt Local} {\str} \texttt{:=} {\qualid} 
-   \zeroone{\modifiers} \zeroone{:{\scope}} \verb=.=\\
+   \zeroone{\modifiers} \zeroone{:{\scope}} .\\
   & $|$ & 
    \texttt{Reserved Notation} \zeroone{\tt Local} {\str}
-   \zeroone{\modifiers} \verb=.=\\
+   \zeroone{\modifiers} .\\
   & $|$ & {\tt Inductive}
    \nelist{{\inductivebody} \zeroone{\declnotation}}{with}{\tt .}\\
   & $|$ & {\tt CoInductive}
@@ -398,7 +391,7 @@ Locate "'exists' _ , _".
    \nelist{{\cofixpointbody} \zeroone{\declnotation}}{with} {\tt .} \\
 \\
 {\declnotation} & ::= & 
-  \zeroone{{\tt where} {\str} {\tt :=} {\term} \zeroone{:{\scope}}} \verb=.=
+  \zeroone{{\tt where} {\str} {\tt :=} {\term} \zeroone{:{\scope}}} .
 \\
 \\
 {\modifiers}
@@ -412,9 +405,9 @@ Locate "'exists' _ , _".
   & $|$ & {\ident} {\tt global} \\
   & $|$ & {\ident} {\tt bigint} \\
   & $|$ & {\tt only parsing} \\
-  & $|$ & {\tt format} {\str} \\
-\hline
+  & $|$ & {\tt format} {\str} 
 \end{tabular}
+\end{centerframe}
 \caption{Syntax of the variants of {\tt Notation}}
 \label{notation-syntax}
 \end{figure}
@@ -488,18 +481,14 @@ core\_scope}, {\tt type\_scope} and {\tt nat\_scope}.
 The command to add a scope to the interpretation scope stack is
 \comindex{Open Scope}
 \comindex{Close Scope}
-
-\bigskip
+\begin{quote}
 {\tt Open Scope} {\scope}.
-\bigskip
-
+\end{quote}
 It is also possible to remove a scope from the interpretation scope
 stack by using the command
-
-\bigskip
+\begin{quote}
 {\tt Close Scope} {\scope}.
-\bigskip
-
+\end{quote}
 Notice that this command does not only cancel the last {\tt Open Scope
 {\scope}} but all the invocation of it.
 
@@ -508,12 +497,14 @@ sections where they occur. When defined outside of a section, they are
 exported to the modules that import the module where they occur.
 
 \begin{Variants}
-\item
-{\tt Open Local Scope} {\scope}.
-\item
-{\tt Close Local Scope} {\scope}.\\
+
+\item {\tt Open Local Scope} {\scope}.
+
+\item {\tt Close Local Scope} {\scope}.
+
 These variants are not exported to the modules that import the module
 where they occur, even if outside a section.
+
 \end{Variants}
 
 \subsection{Local interpretation rules for notations}
@@ -521,13 +512,13 @@ where they occur, even if outside a section.
 In addition to the global rules of interpretation of notations, some
 ways to change the interpretation of subterms are available.
 
-\subsubsection{Local opening of an interpretation scope} 
+\subsubsection{Local opening of an interpretation scope 
 \label{scopechange}
 \index{\%}
-\comindex{Delimit Scope}
+\comindex{Delimit Scope}}
 
 It is possible to locally extend the interpretation scope stack using
-the syntax {(\term)\%{\nterm{key} (or simply {\term}\%{\nterm{key}}
+the syntax ({\term})\%{\nterm{key}} (or simply {\term}\%{\nterm{key}}
 for atomic terms), where {\nterm{key}} is a special identifier called
 {\em delimiting key} and bound to a given scope.
 
@@ -536,21 +527,18 @@ interpreted in the scope stack extended with the scope bound to
 {\nterm{key}}.
 
 To bind a delimiting key to a scope, use the command
+\begin{quote}
+\texttt{Delimit Scope} {\scope} \texttt{with} {\ident} 
+\end{quote}
 
-\bigskip
-\texttt{Delimit Scope} {\scope} \texttt{with} {\ident} \\
-\bigskip
-
-\subsubsection{Binding arguments of a constant to an interpretation scope}
-\comindex{Arguments Scope}
+\subsubsection{Binding arguments of a constant to an interpretation scope
+\comindex{Arguments Scope}}
 
 It is possible to set in advance that some arguments of a given
 constant have to be interpreted in a given scope. The command is
-
-\bigskip
-{\tt Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}\\
-\bigskip
-
+\begin{quote}
+{\tt Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
+\end{quote}
 where the list is a list made either of {\tt \_} or of a scope name.
 Each scope in the list is bound to the corresponding parameter of
 {\qualid} in order.  When interpreting a term, if some of the
@@ -577,13 +565,11 @@ type that would trigger the same scope).
 \comindex{Bind Scope}
 More generally, any {\class} (see chapter \ref{Coercions-full}) can be
 bound to an interpretation scope. The command to do it is
-
-\bigskip
+\begin{quote}
 {\tt Bind Scope} {\scope} \texttt{with} {\class}
-\bigskip
+\end{quote}
 
 \Example
-
 \begin{coq_example}
 Parameter U : Set.
 Bind Scope U_scope with U.
@@ -737,15 +723,12 @@ expressions which are not typed at the time of the definition of the
 abbreviation but at the time it is used. Especially, abbreviation can
 be bound to terms with holes (i.e. with ``\_''). The general syntax
 for abbreviations is
-
-\bigskip
-\texttt{Notation} \zeroone{\tt Local} {\ident} \texttt{:=} {\term} 
- \zeroone{\tt (only parsing)} \verb=.=
-\bigskip
-
+\begin{quote}
+\texttt{Notation} \zeroone{{\tt Local}} {\ident} \texttt{:=} {\term} 
+ \zeroone{{\tt (only parsing)}} \verb=.=
+\end{quote}
 
 \Example
-
 \begin{coq_eval}
 Set Strict Implicit.
 Reset Initial.
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 21479ca4b..dd5a8b05f 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1,6 +1,6 @@
-\chapter{Tactics}
+\chapter{Tactics
 \index{Tactics}
-\label{Tactics}
+\label{Tactics}}
 
 A deduction rule is a link between some (unique) formula, that we call
 the {\em conclusion} and (several) formul{\ae} that we call the {\em
@@ -22,8 +22,8 @@ Each (sub)goal is denoted with a number. The current goal is numbered
 1. By default, a tactic is applied to the current goal, but one can
 address a particular goal in the list by writing {\sl n:\tac} which
 means {\it ``apply tactic {\tac} to goal number {\sl n}''}.
-We can show the list of subgoals by typing {\tt Show} (see section
-\ref{Show}).
+We can show the list of subgoals by typing {\tt Show} (see
+Section~\ref{Show}). 
 
 Since not every rule applies to a given statement, every tactic cannot be
 used to reduce any goal. In other words, before applying a tactic to a
@@ -41,9 +41,9 @@ the one of {\em derived rules} which are built by combination of other
 tactics. The third one implements heuristics or decision procedures to
 build a complete proof of a goal.
 
-\section{Invocation of tactics}
+\section{Invocation of tactics
 \label{tactic-syntax}
-\index{tactic@{\tac}}
+\index{tactic@{\tac}}}
 
 A tactic is applied as an ordinary command. If the tactic does not
 address the first subgoal, the command may be preceded by the wished
@@ -56,23 +56,24 @@ subgoal number as shown below:
 
 \section{Explicit proof as a term}
 
-\subsection{\tt exact \term}
+\subsection{\tt exact \term
 \tacindex{exact}
-\label{exact}
+\label{exact}}
+
 This tactic applies to any goal. It gives directly the exact proof
 term of the goal. Let {\T} be our goal, let {\tt p} be a term of type
 {\tt U} then {\tt exact p} succeeds iff {\tt T} and {\tt U} are
-convertible (see section \ref{conv-rules}).
+convertible (see Section~\ref{conv-rules}).
 
 \begin{ErrMsgs}
 \item \errindex{Not an exact proof}
 \end{ErrMsgs}
 
 
-\subsection{\tt refine \term}
+\subsection{\tt refine \term
 \tacindex{refine}
 \label{refine}
-\index{?@{\texttt{?}}}
+\index{?@{\texttt{?}}}}
 
 This tactic allows to give an exact proof but still with some
 holes. The holes are noted ``\texttt{\_}''.
@@ -91,28 +92,30 @@ holes. The holes are noted ``\texttt{\_}''.
 \end{ErrMsgs}
 
 This tactic is currently given as an experiment. An example of use is given
-in section~\ref{refine-example}.
+in Section~\ref{refine-example}.
+
+\section{Basics
+\index{Typing rules}}
 
-\section{Basics}
-\index{Typing rules}
 Tactics presented in this section implement the basic typing rules of
-{\sc Cic} given in chapter \ref{Cic}.
+{\sc Cic} given in Chapter~\ref{Cic}.
+
+\subsection{{\tt assumption}
+\tacindex{assumption}}
 
-\subsection{{\tt assumption}}
-\tacindex{assumption}
 This tactic applies to any goal. It implements the
-``Var''\index{Typing rules!Var} rule given in section
-\ref{Typed-terms}. It looks in the local context for an hypothesis
-which type is equal to the goal.  If it is the case, the subgoal is
-proved. Otherwise, it fails.
+``Var''\index{Typing rules!Var} rule given in
+Section~\ref{Typed-terms}. It looks in the local context for an
+hypothesis which type is equal to the goal.  If it is the case, the
+subgoal is proved. Otherwise, it fails.
 
 \begin{ErrMsgs}
 \item  \errindex{No such assumption}
 \end{ErrMsgs}
 
-\subsection{\tt clear {\ident}}
+\subsection{\tt clear {\ident}
 \tacindex{clear}
-\label{clear}
+\label{clear}}
 
 This tactic erases the hypothesis named {\ident} in the local context
 of the current goal. Then {\ident} is no more displayed and no more
@@ -141,8 +144,8 @@ usable in the proof development.
     used in the hypothesis} 
 \end{ErrMsgs}
 
-\subsection{\tt move {\ident$_1$} after {\ident$_2$}}
-\tacindex{move}
+\subsection{\tt move {\ident$_1$} after {\ident$_2$}
+\tacindex{move}}
 
 This moves the hypothesis named {\ident$_1$} in the local context
 after the hypothesis named {\ident$_2$}.
@@ -167,8 +170,8 @@ then all hypotheses between {\ident$_1$} and {\ident$_2$} which
 
 \end{ErrMsgs}
 
-\subsection{\tt rename {\ident$_1$} into {\ident$_2$}}
-\tacindex{rename}
+\subsection{\tt rename {\ident$_1$} into {\ident$_2$}
+\tacindex{rename}}
 
 This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current
 context\footnote{but it does not rename the hypothesis in the
@@ -182,9 +185,9 @@ context\footnote{but it does not rename the hypothesis in the
 
 \end{ErrMsgs}
 
-\subsection{\tt intro}
+\subsection{\tt intro
 \tacindex{intro}
-\label{intro}
+\label{intro}}
 
 This tactic applies to a goal which is either a product or starts with
 a let binder. If the goal is a product, the tactic implements the
@@ -296,8 +299,9 @@ the tactic {\tt intro} applies the tactic {\tt red} until the tactic
 
 \end{Variants}
 
-\subsection{\tt apply \term}
-\tacindex{apply}\label{apply}
+\subsection{\tt apply \term
+\tacindex{apply}
+\label{apply}}
 
 This tactic applies to any goal.  The argument {\term} is a term
 well-formed in the local context.  The tactic {\tt apply} tries to
@@ -312,8 +316,8 @@ instantiations of the premises of the type of {\term}.
   tactic may fail when you think it should work.  In this case, if you
   know that the conclusion of {\term} and the current goal are
   unifiable, you can help the {\tt apply} tactic by transforming your
-  goal with the {\tt change} or {\tt pattern} tactics (see sections
-  \ref{pattern}, \ref{change}).
+  goal with the {\tt change} or {\tt pattern} tactics (see
+  Sections~\ref{pattern},~\ref{change}). 
 
 \item \errindex{Cannot refine to conclusions with meta-variables}
 
@@ -342,9 +346,9 @@ instantiations of the premises of the type of {\term}.
   
   This also provides {\tt apply} with values for instantiating
   premises. But variables are referred by names and non dependent
-  products by order (see syntax in the section~\ref{Binding-list}).
+  products by order (see syntax in Section~\ref{Binding-list}).
 
-\item{\tt eapply \term}\tacindex{eapply}\label{eapply}
+\item {\tt eapply \term}\tacindex{eapply}\label{eapply}
   
   The tactic {\tt eapply} behaves as {\tt apply} but does not fail
   when no instantiation are deducible for some variables in the
@@ -354,10 +358,10 @@ instantiations of the premises of the type of {\term}.
   where $n$ is a number.  The instantiation is intended to be found
   later in the proof.
 
-  An example of use of {\tt eapply} is given in section
-  \ref{eapply-example}.
+  An example of use of {\tt eapply} is given in
+  Section~\ref{eapply-example}. 
 
-\item{\tt lapply {\term}} \tacindex{lapply} 
+\item {\tt lapply {\term}} \tacindex{lapply} 
 
   This tactic applies to any goal, say {\tt G}.  The argument {\term}
   has to be well-formed in the current context, its type being
@@ -374,9 +378,9 @@ instantiations of the premises of the type of {\term}.
 
 \end{Variants}
 
-\subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )}}
+\subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )}
 \tacindex{set}
-\tacindex{pose}
+\tacindex{pose}}
 
 This replaces {\term} by {\ident} in the conclusion or in the
 hypotheses of the current goal and adds the new definition {\ident
@@ -434,8 +438,8 @@ should not be substituted.
 
 \end{Variants}
 
-\subsection{{\tt assert ( {\ident} : {\form} \tt )}}
-\tacindex{assert}
+\subsection{{\tt assert ( {\ident} : {\form} \tt )}
+\tacindex{assert}}
 
 This tactic applies to any goal. {\tt assert (H : U)} adds a new
 hypothesis of name \texttt{H} asserting \texttt{U} to the current goal
@@ -466,11 +470,11 @@ in the list of subgoals remaining to prove.
 \item {\tt cut {\form}}\tacindex{cut} 
   
   This tactic applies to any goal. It implements the non dependent
-  case of the ``App''\index{Typing rules!App} rule given in section
-  \ref{Typed-terms}. (This is Modus Ponens inference rule.)  {\tt cut
-    U} transforms the current goal \texttt{T} into the two following
-  subgoals: {\tt U -> T} and \texttt{U}.  The subgoal {\tt U -> T}
-  comes first in the list of remaining subgoal to prove.
+  case of the ``App''\index{Typing rules!App} rule given in
+  Section~\ref{Typed-terms}. (This is Modus Ponens inference rule.)
+  {\tt cut U} transforms the current goal \texttt{T} into the two
+  following subgoals: {\tt U -> T} and \texttt{U}.  The subgoal {\tt U
+    -> T} comes first in the list of remaining subgoal to prove.
 
 \end{Variants}
 
@@ -508,8 +512,9 @@ in the list of subgoals remaining to prove.
 %  \term\ will be kept.
 %\end{Variants}
 
-\subsection{\tt generalize \term}
-\tacindex{generalize}\label{generalize}
+\subsection{\tt generalize \term
+\tacindex{generalize}
+\label{generalize}}
 
 This tactic applies to any goal. It generalizes the conclusion w.r.t.
 one subterm of it. For example:
@@ -547,11 +552,12 @@ to $T$.
 
 \end{Variants}
 
-\subsection{\tt change \term}
-\tacindex{change}\label{change}
+\subsection{\tt change \term
+\tacindex{change}
+\label{change}}
 
 This tactic applies to any goal. It implements the rule
-``Conv''\index{Typing rules!Conv} given in section \ref{Conv}.  {\tt
+``Conv''\index{Typing rules!Conv} given in Section~\ref{Conv}.  {\tt
   change U} replaces the current goal \T\ with a \U\ providing that
 \U\ is well-formed and that \T\ and \U\ are convertible.
 
@@ -589,8 +595,9 @@ This tactic applies to any goal. It implements the rule
 
 \SeeAlso \ref{Conversion-tactics}
 
-\subsection{Bindings list}
-\index{Binding list}\label{Binding-list}
+\subsection{Bindings list
+\index{Binding list}
+\label{Binding-list}}
 
 A bindings list is generally used after the keyword {\tt with} in
 tactics.  The general shape of a bindings list is {\tt (\vref$_1$ :=
@@ -605,7 +612,7 @@ product {\tt \ident$_i$:T} (for some type \T); if \vref$_i$ is
 A bindings list can also be a simple list of terms {\tt \term$_1$
   \term$_2$ \dots\term$_n$}. In that case the references to which
 these terms correspond are determined by the tactic. In case of {\tt
-  elim \term} (see section \ref{elim}) the terms should correspond to
+  elim \term} (see Section~\ref{elim}) the terms should correspond to
 all the dependent products in the type of \term\ while in the case of
 {\tt apply \term} only the dependent products which are not bound in
 the conclusion of the type are given.
@@ -613,8 +620,9 @@ the conclusion of the type are given.
 
 \section{Negation and contradiction}
 
-\subsection{\tt absurd \term}
-\tacindex{absurd}\label{absurd}
+\subsection{\tt absurd \term
+\tacindex{absurd}
+\label{absurd}}
 
 This tactic applies to any goal. The argument {\term} is any
 proposition {\tt P} of type {\tt Prop}. This tactic applies {\tt
@@ -624,9 +632,9 @@ very useful in proofs by cases, where some cases are impossible. In
 most cases, \texttt{P} or $\sim$\texttt{P} is one of the hypotheses of
 the local context.
 
-\subsection{\tt contradiction}
+\subsection{\tt contradiction
 \label{contradiction}
-\tacindex{contradiction}
+\tacindex{contradiction}}
 
 This tactic applies to any goal. The {\tt contradiction} tactic
 attempts to find in the current context (after all {\tt intros}) one
@@ -639,9 +647,9 @@ cases.  This tactic is a macro for the tactics sequence {\tt intros;
 \end{ErrMsgs}
 
 
-\section{Conversion tactics}
+\section{Conversion tactics
 \index{Conversion tactics}
-\label{Conversion-tactics}
+\label{Conversion-tactics}}
 
 This set of tactics implements different specialized usages of the
 tactic \texttt{change}.
@@ -651,8 +659,10 @@ tactic \texttt{change}.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$
-\dots\ \flag$_n$} and {\tt compute}}
-\tacindex{cbv}\tacindex{lazy}
+\dots\ \flag$_n$} and {\tt compute}
+\tacindex{cbv}
+\tacindex{lazy}
+\tacindex{compute}}
 
 These parameterized reduction tactics apply to any goal and perform
 the normalization of the goal according to the specified flags. Since
@@ -704,8 +714,8 @@ computational expressions (i.e. with few dead code).
 \end{ErrMsgs}
 
 
-\subsection{{\tt red}}
-\tacindex{red}
+\subsection{{\tt red}
+\tacindex{red}}
 
 This tactic applies to a goal which have form {\tt
   forall (x:T1)\dots(xk:Tk), c t1 \dots\ tn} where {\tt c} is a constant.  If
@@ -717,8 +727,8 @@ $\beta\iota$-reduction rules.
 \item \errindex{Not reducible}
 \end{ErrMsgs}
 
-\subsection{{\tt hnf}}
-\tacindex{hnf}
+\subsection{{\tt hnf}
+\tacindex{hnf}}
 
 This tactic applies to any goal. It replaces the current goal with its
 head normal form according to the $\beta\delta\iota$-reduction rules.
@@ -730,10 +740,10 @@ The term \verb+forall (n:nat), (plus (S n) (S n))+ is not reduced by {\tt hnf}.
 
 \Rem The $\delta$ rule will only be applied to transparent constants
 (i.e. which have not been frozen with an {\tt Opaque} command; see
-section \ref{Opaque}).
+Section~\ref{Opaque}).
 
-\subsection{\tt simpl}
-\tacindex{simpl}
+\subsection{\tt simpl
+\tacindex{simpl}}
 
 This tactic applies to any goal. The tactic {\tt simpl} first applies
 $\beta\iota$-reduction rule.  Then it expands transparent constants
@@ -768,12 +778,12 @@ applicative subterms whose head occurrence is {\ident}.
 
 \end{Variants}
 
-\subsection{\tt unfold \qualid}
-\tacindex{unfold}\label{unfold}
+\subsection{\tt unfold \qualid
+\tacindex{unfold}
+\label{unfold}}
 
 This tactic applies to any goal. The argument {\qualid} must denote a
-defined transparent constant or local definition (see section
-\ref{Simpl-definitions} and \ref{Transparent}).  The tactic {\tt
+defined transparent constant or local definition (see Sections~\ref{Simpl-definitions} and~\ref{Transparent}).  The tactic {\tt
   unfold} applies the $\delta$ rule to each occurrence of the constant
 to which {\qualid} refers in the current goal and then replaces it
 with its $\beta\iota$-normal form.
@@ -805,8 +815,8 @@ is printed.
 
 \end{Variants}
 
-\subsection{{\tt fold} \term}
-\tacindex{fold}
+\subsection{{\tt fold} \term
+\tacindex{fold}}
 
 This tactic applies to any goal. \term\ is reduced using the {\tt red}
 tactic. Every occurrence of the resulting term in the goal is then
@@ -818,8 +828,9 @@ substituted for \term.
   Equivalent to {\tt fold} \term$_1${\tt;}\ldots{\tt; fold} \term$_n$.
 \end{Variants}
 
-\subsection{{\tt pattern {\term}}}
-\tacindex{pattern}\label{pattern}
+\subsection{{\tt pattern {\term}}
+\tacindex{pattern}
+\label{pattern}}
 
 This command applies to any goal. The argument {\term} must be a free
 subterm of the current goal.  The command {\tt pattern} performs
@@ -875,13 +886,14 @@ local definition. Example: {\tt unfold not in (Type of H1) (Type of H3).}
 
 
 \section{Introductions}
+
 Introduction tactics address goals which are inductive constants.
 They are used when one guesses that the goal can be obtained with one
 of its constructors' type.
 
-\subsection{\tt constructor \num}
+\subsection{\tt constructor \num
 \label{constructor}
-\tacindex{constructor}
+\tacindex{constructor}}
 
 This tactic applies to a goal such that the head of its conclusion is
 an inductive constant (say {\tt I}).  The argument {\num} must be less
@@ -943,10 +955,10 @@ equivalent to {\tt intros; apply ci}.
 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
-section~\ref{Cic-inductive-definitions}).
+Section~\ref{Cic-inductive-definitions}).
 
-\subsection{\tt induction \term}
-\tacindex{induction}
+\subsection{\tt induction \term
+\tacindex{induction}}
 
 This tactic applies to any goal. The type of the argument {\term} must
 be an inductive constant. Then, the tactic {\tt induction}
@@ -988,25 +1000,25 @@ induction n.
 \item \errindex{Not an inductive product}
 \item \errindex{Cannot refine to conclusions with meta-variables}
   
-  As {\tt induction} uses {\tt apply}, see section \ref{apply} and
+  As {\tt induction} uses {\tt apply}, see Section~\ref{apply} and
   the variant {\tt elim \dots\ with \dots} below.
 \end{ErrMsgs}
 
 \begin{Variants}
 \item{\tt induction {\term} as {\intropattern}}
-
+  
   This behaves as {\tt induction {\term}} but uses the names in
-  {\intropattern} to names the variables introduced in the context. The
-  {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
+  {\intropattern} to names the variables introduced in the context.
+  The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
   $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
-  ]} with $m$ being the number of constructors of the type of
-  {\term}. Each variable introduced by {\tt induction} in the context of
-  the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
+    ]} with $m$ being the number of constructors of the type of
+  {\term}. Each variable introduced by {\tt induction} in the context
+  of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
   $p_{in_i}$ in order. If there are not enough names, {\tt induction}
   invents names for the remaining variables to introduce. More
-  generally, the $p$'s can be any introduction patterns (see section
-  \ref{intros-pattern}). This provides a concise notation for nested
-  induction.
+  generally, the $p$'s can be any introduction patterns (see
+  Section~\ref{intros-pattern}). This provides a concise notation for
+  nested induction.
 
 \Rem for an inductive type with one constructeur, the pattern notation
 {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
@@ -1109,8 +1121,8 @@ a simple term or a term with a bindings list (see \ref{Binding-list}).
 
 \end{Variants}
 
-\subsection{\tt destruct \term}
-\tacindex{destruct}
+\subsection{\tt destruct \term
+\tacindex{destruct}}
 
 The tactic {\tt destruct} is used to perform case analysis without
 recursion. Its behavior is similar to {\tt induction} except
@@ -1134,19 +1146,19 @@ last introduced hypothesis.
 
 \begin{Variants}
 \item{\tt destruct {\term} as {\intropattern}}
-
+  
   This behaves as {\tt destruct {\term}} but uses the names in
-  {\intropattern} to names the variables introduced in the context. The
-  {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
+  {\intropattern} to names the variables introduced in the context.
+  The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
   $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
-  ]} with $m$ being the number of constructors of the type of
-  {\term}. Each variable introduced by {\tt destruct} in the context of
-  the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
+    ]} with $m$ being the number of constructors of the type of
+  {\term}. Each variable introduced by {\tt destruct} in the context
+  of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
   $p_{in_i}$ in order. If there are not enough names, {\tt destruct}
   invents names for the remaining variables to introduce. More
-  generally, the $p$'s can be any introduction patterns (see section
-  \ref{intros-pattern}). This provides a concise notation for nested
-  destruction.
+  generally, the $p$'s can be any introduction patterns (see
+  Section~\ref{intros-pattern}). This provides a concise notation for
+  nested destruction.
 
 %  It is recommended to use this variant of {\tt destruct} for 
 %  robust proof scripts.
@@ -1190,9 +1202,9 @@ last introduced hypothesis.
 
 \end{Variants}
 
-\subsection{\tt intros {\intropattern} {\ldots} {\intropattern}}
+\subsection{\tt intros {\intropattern} {\ldots} {\intropattern}
 \label{intros-pattern}
-\tacindex{intros \intropattern}
+\tacindex{intros \intropattern}}
 
 The tactic {\tt intros} applied to introduction patterns performs both
 introduction of variables and case analysis in order to give names to
@@ -1251,17 +1263,17 @@ Proof c.
 %\subsection{\tt FixPoint \dots}\tacindex{Fixpoint}
 %Not yet documented.
 
-\subsection {\tt double induction \ident$_1$ \ident$_2$}
-\tacindex{double induction}
-This tactic applies to any goal. If the variables {\ident$_1$} and {\ident$_2$}
-of the goal have an inductive type, then this tactic
-performs double induction on these variables.
-For instance, if the current goal is \verb+(n,m:nat)(P n m)+ then,
-{\tt double induction n m} yields the four cases with their respective
-inductive hypotheses. In particular the case for
-\verb+(P (S n) (S m))+
-with the induction hypotheses \verb+(P (S n) m)+ and 
-\verb+(m:nat)(P n m)+ (hence \verb+(P n m)+ and \verb+(P n (S m))+).
+\subsection {\tt double induction \ident$_1$ \ident$_2$
+\tacindex{double induction}}
+
+This tactic applies to any goal. If the variables {\ident$_1$} and
+{\ident$_2$} of the goal have an inductive type, then this tactic
+performs double induction on these variables.  For instance, if the
+current goal is \verb+(n,m:nat)(P n m)+ then, {\tt double induction n
+  m} yields the four cases with their respective inductive hypotheses.
+In particular the case for \verb+(P (S n) (S m))+ with the induction
+hypotheses \verb+(P (S n) m)+ and \verb+(m:nat)(P n m)+ (hence
+\verb+(P n m)+ and \verb+(P n (S m))+).
 
 \Rem When the induction hypothesis \verb+(P (S n) m)+ is not
 needed, {\tt induction \ident$_1$; destruct \ident$_2$} produces
@@ -1269,16 +1281,18 @@ more concise subgoals.
 
 \begin{Variant}
 
-\item {\tt double induction \num$_1$ \num$_2$}\\
+\item {\tt double induction \num$_1$ \num$_2$}
+
 This applies double induction on the \num$_1^{th}$ and \num$_2^{th}$ {\it
 non dependent} premises of the goal. More generally, any combination of an
 {\ident} and an {\num} is valid.
 
 \end{Variant}
 
-\subsection{\tt decompose [ {\ident$_1$} \dots\ {\ident$_n$} ] \term}
+\subsection{\tt decompose [ {\ident$_1$} \dots\ {\ident$_n$} ] \term
 \label{decompose}
-\tacindex{decompose}
+\tacindex{decompose}}
+
 This tactic allows to recursively decompose a
 complex proposition in order to obtain atomic ones.
 Example: 
@@ -1307,9 +1321,9 @@ Qed.
 \end{Variants}
 
 
-\subsection{\tt functional induction \ident\ \term$_1$ \dots\ \term$_n$.}
+\subsection{\tt functional induction \ident\ \term$_1$ \dots\ \term$_n$.
 \tacindex{functional induction}
-\label{FunInduction}
+\label{FunInduction}}
 
 The tactic \texttt{functional induction} performs case analysis
 and induction following the definition of a function.
@@ -1340,13 +1354,14 @@ functions built by certain tactics.
 \section{Equality}
 
 These tactics use the equality {\tt eq:forall A:Type, A->A->Prop}
-defined in file {\tt Logic.v} (see section \ref{Equality}). The
+defined in file {\tt Logic.v} (see Section~\ref{Equality}). The
 notation for {\tt eq}~$T~t~u$ is simply {\tt $t$=$u$} dropping the
 implicit type of $t$ and $u$.
 
-\subsection{\tt rewrite \term}
+\subsection{\tt rewrite \term
 \label{rewrite}
-\tacindex{rewrite}
+\tacindex{rewrite}}
+
 This tactic applies to any goal. The type of {\term}
 must have the form
 
@@ -1393,15 +1408,16 @@ This happens if \term$_1$ does not occur in the goal.
 \end{Variants}
 
 
-\subsection{\tt cutrewrite -> \term$_1$ = \term$_2$}
+\subsection{\tt cutrewrite -> \term$_1$ = \term$_2$
 \label{cutrewrite}
-\tacindex{cutrewrite}
+\tacindex{cutrewrite}}
 
 This tactic acts like {\tt replace {\term$_1$} with {\term$_2$}}
 (see below).
 
-\subsection{\tt replace {\term$_1$} with {\term$_2$}}
-\tacindex{replace \dots\ with}
+\subsection{\tt replace {\term$_1$} with {\term$_2$}
+\tacindex{replace \dots\ with}}
+
 This tactic applies to any goal. It replaces all free occurrences of
 {\term$_1$} in the current goal with {\term$_2$} and generates the
 equality {\term$_2$}{\tt =}{\term$_1$} as a subgoal. It is equivalent
@@ -1420,9 +1436,10 @@ to {\tt cut \term$_2$=\term$_1$; intro H{\sl n}; rewrite <- H{\sl n};
 %
 %\end{Variants}
 
-\subsection{\tt reflexivity}
+\subsection{\tt reflexivity
 \label{reflexivity}
-\tacindex{reflexivity}
+\tacindex{reflexivity}}
+
 This tactic applies to a goal which has the form {\tt t=u}. It checks
 that {\tt t} and {\tt u} are convertible and then solves the goal.
 It is equivalent to {\tt apply refl\_equal}.
@@ -1432,9 +1449,10 @@ It is equivalent to {\tt apply refl\_equal}.
 \item \errindex{Impossible to unify \dots\ with ..}
 \end{ErrMsgs}
 
-\subsection{\tt symmetry}
+\subsection{\tt symmetry
 \tacindex{symmetry}
-\tacindex{symmetry in}
+\tacindex{symmetry in}}
+
 This tactic applies to a goal which has form {\tt t=u} and changes it
 into {\tt u=t}.
 
@@ -1442,12 +1460,16 @@ into {\tt u=t}.
 If the statement of the hypothesis {\ident} has the form {\tt t=u},
 the tactic changes it to {\tt u=t}.
 
-\subsection{\tt transitivity \term}\tacindex{transitivity}
+\subsection{\tt transitivity \term
+\tacindex{transitivity}}
+
 This tactic applies to a goal which have form {\tt t=u}
 and transforms it into the two subgoals 
 {\tt t={\term}} and {\tt {\term}=u}.
 
-\subsection{\tt subst {\ident}}\tacindex{subst}
+\subsection{\tt subst {\ident}
+\tacindex{subst}}
+
 This tactic applies to a goal which have \ident\ in its context and
 (at least) one hypothesis, say {\tt H}, of type {\tt
   \ident=t} or {\tt t=\ident}. Then it replaces 
@@ -1468,14 +1490,16 @@ When several hypotheses have the form {\tt \ident=t} or {\tt
 
 
 \section{Equality and inductive sets}
+
 We describe in this section some special purpose tactics dealing with
 equality and inductive sets or types. These tactics use the equality
 {\tt eq:forall (A:Type), A->A->Prop}, simply written with the
 infix symbol {\tt =}.
 
-\subsection{\tt decide equality}
+\subsection{\tt decide equality
 \label{decideequality}
-\tacindex{decide equality}
+\tacindex{decide equality}}
+
 This tactic solves a goal of the form
 {\tt forall $x$ $y$:$R$, \{$x$=$y$\}+\{\verb|~|$x$=$y$\}}, where $R$
 is an inductive type such that its constructors do not take proofs or
@@ -1487,8 +1511,9 @@ functions as arguments, nor objects in dependent types.
 \}+\{\verb|~|}\term$_1${\tt =}\term$_2${\tt \}}.
 \end{Variants}
 
-\subsection{\tt compare \term$_1$ \term$_2$}
-\tacindex{compare}
+\subsection{\tt compare \term$_1$ \term$_2$
+\tacindex{compare}}
+
 This tactic compares two given objects \term$_1$ and \term$_2$ 
 of an inductive datatype. If $G$ is the current goal, it leaves the sub-goals
 \term$_1${\tt =}\term$_2$ {\tt ->} $G$ and \verb|~|\term$_1${\tt =}\term$_2$
@@ -1496,24 +1521,24 @@ 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}
-This tactic proves any goal from an absurd
-hypothesis stating that two structurally different terms of an
-inductive set are equal. For example, from the hypothesis {\tt (S (S
-  O))=(S O)} we can derive by absurdity any proposition.  Let {\ident}
-be a hypothesis of type {\tt{\term$_1$} = {\term$_2$}} in the local
-context, {\term$_1$} and {\term$_2$} being elements of an inductive set.
-To build the proof, the tactic traverses the normal
-forms\footnote{Recall: opaque constants will not be expanded by
-  $\delta$ reductions} of {\term$_1$} and {\term$_2$} looking for a
-couple of subterms {\tt u} and {\tt w} ({\tt u} subterm of the normal
-form of {\term$_1$} and {\tt w} subterm of the normal form of
-{\term$_2$}), placed at the same positions and whose
-head symbols are two different constructors. If such a couple of subterms
-exists, then the proof of the current goal is completed,
-otherwise the tactic fails.
+\tacindex{discriminate}}
+
+This tactic proves any goal from an absurd hypothesis stating that two
+structurally different terms of an inductive set are equal. For
+example, from the hypothesis {\tt (S (S O))=(S O)} we can derive by
+absurdity any proposition.  Let {\ident} be a hypothesis of type
+{\tt{\term$_1$} = {\term$_2$}} in the local context, {\term$_1$} and
+{\term$_2$} being elements of an inductive set.  To build the proof,
+the tactic traverses the normal forms\footnote{Recall: opaque
+  constants will not be expanded by $\delta$ reductions} of
+{\term$_1$} and {\term$_2$} looking for a couple of subterms {\tt u}
+and {\tt w} ({\tt u} subterm of the normal form of {\term$_1$} and
+{\tt w} subterm of the normal form of {\term$_2$}), placed at the same
+positions and whose head symbols are two different constructors. If
+such a couple of subterms exists, then the proof of the current goal
+is completed, otherwise the tactic fails.
 
 \Rem If {\ident} does not denote an hypothesis in the local context
 but refers to an hypothesis quantified in the goal, then the
@@ -1542,9 +1567,10 @@ introduced hypothesis.
   \end{ErrMsgs}
 \end{Variants}
 
-\subsection{\tt injection {\ident}}
+\subsection{\tt injection {\ident}
 \label{injection}
-\tacindex{injection}
+\tacindex{injection}}
+
 The {\tt injection} tactic is based on the fact that constructors of
 inductive sets are injections. That means that if $c$ is a constructor
 of an inductive set, and if $(c~\vec{t_1})$ and $(c~\vec{t_2})$ are two
@@ -1625,9 +1651,10 @@ introduced hypothesis.
   \ErrMsg \errindex{goal does not satisfy the expected preconditions}
 \end{Variants}
 
-\subsection{\tt simplify\_eq {\ident}}
+\subsection{\tt simplify\_eq {\ident}
 \tacindex{simplify\_eq}
-\label{simplify-eq}
+\label{simplify-eq}}
+
 Let {\ident} be the name of an hypothesis of type {\tt
   {\term$_1$}={\term$_2$}} in the local context. If {\term$_1$} and
 {\term$_2$} are structurally different (in the sense described for the
@@ -1650,9 +1677,10 @@ If the current goal has form $\verb=~=t_1=t_2$, then this tactic does
 \texttt{hnf; intro {\ident}; simplify\_eq {\ident}}.
 \end{Variants}
 
-\subsection{\tt dependent rewrite -> {\ident}}
+\subsection{\tt dependent rewrite -> {\ident}
 \tacindex{dependent rewrite ->}
-\label{dependent-rewrite}
+\label{dependent-rewrite}}
+
 This tactic applies to any goal.  If \ident\ has type 
 \verb+(existS A B a b)=(existS A B a' b')+ 
 in the local context (i.e. each term of the
@@ -1669,10 +1697,11 @@ Analogous to {\tt dependent rewrite ->} but uses the equality from
 right to left.
 \end{Variants}
 
-\section{inversion}
-\label{inversion}
+\section{inversion
+\label{inversion}}
 
-\subsection{\tt inversion {\ident}}\tacindex{inversion}
+\subsection{\tt inversion {\ident}
+\tacindex{inversion}}
 
 Let the type of \ident~ in the local context be $(I~\vec{t})$,
 where $I$ is a (co)inductive predicate. Then,
@@ -1687,24 +1716,27 @@ latter is first introduced in the local context using
 \texttt{intros until \ident}.
 
 \begin{Variants}
-\item \texttt{inversion} \num\\
+\item \texttt{inversion} \num
+  
   This does the same thing as \texttt{intros until \num} then
-\texttt{inversion \ident} where {\ident} is the identifier for the last
-introduced hypothesis.
-\item \texttt{inversion\_clear} \ident\\
-  \tacindex{inversion\_clear}
+  \texttt{inversion \ident} where {\ident} is the identifier for the
+  last introduced hypothesis.
+
+\item \tacindex{inversion\_clear} \texttt{inversion\_clear} \ident
+
   This behaves as \texttt{inversion} and then erases \ident~ from the
   context.
-\item \texttt{inversion} {\ident} \texttt{as} {\intropattern} \\
-  \tacindex{inversion \dots\ as} 
+
+\item \tacindex{inversion \dots\ as} \texttt{inversion} {\ident} \texttt{as} {\intropattern}
+  
   This behaves as \texttt{inversion} but using names in
-  {\intropattern} for naming hypotheses. The {\intropattern}
-  must have the form {\tt [} $p_{11}$ \ldots $p_{1n_1}$ {\tt |}
-  {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt ]} with $m$ being
-  the number of constructors of the type of {\ident}. Be careful that
-  the list must be of length $m$ even if {\tt inversion} discards some
-  cases (which is precisely one of its roles): for the discarded cases, just use an empty list
-  (i.e. $n_i=0$). 
+  {\intropattern} for naming hypotheses. The {\intropattern} must have
+  the form {\tt [} $p_{11}$ \ldots $p_{1n_1}$ {\tt |} {\ldots} {\tt |}
+  $p_{m1}$ \ldots $p_{mn_m}$ {\tt ]} with $m$ being the number of
+  constructors of the type of {\ident}. Be careful that the list must
+  be of length $m$ even if {\tt inversion} discards some cases (which
+  is precisely one of its roles): for the discarded cases, just use an
+  empty list (i.e. $n_i=0$).
 
   The arguments of the $i^{th}$ constructor and the
   equalities that {\tt inversion} introduces in the context of the
@@ -1735,99 +1767,136 @@ intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ].
 Abort.
 \end{coq_eval}
 
-\item \texttt{inversion} {\num} {\tt as} {\intropattern} \\
+\item \texttt{inversion} {\num} {\tt as} {\intropattern} 
+
   This allows to name the hypotheses introduced by
   \texttt{inversion} {\num} in the context.
-\item \texttt{inversion\_clear} {\ident} {\tt as} {\intropattern} \\
-  \tacindex{inversion\_cleardots\ as}
+
+\item \tacindex{inversion\_cleardots\ as} \texttt{inversion\_clear}
+  {\ident} {\tt as} {\intropattern}  
+
   This allows to name the hypotheses introduced by
   \texttt{inversion\_clear} in the context.
-\item \texttt{inversion } {\ident} \texttt{in} \ident$_1$ \dots\ \ident$_n$\\
-  \tacindex{inversion \dots\ in}
+  
+\item \tacindex{inversion \dots\ in} \texttt{inversion } {\ident}
+  \texttt{in} \ident$_1$ \dots\ \ident$_n$
+
   Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This
   tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and
   then performing \texttt{inversion}.
-\item \texttt{inversion } {\ident}  {\tt as} {\intropattern}
-\texttt{in} \ident$_1$ \dots\ \ident$_n$\\
-  \tacindex{inversion \dots\ as \dots\ in}
+  
+\item \tacindex{inversion \dots\ as \dots\ in} \texttt{inversion }
+  {\ident} {\tt as} {\intropattern} \texttt{in} \ident$_1$ \dots\ 
+  \ident$_n$
+  
   This allows to name the hypotheses introduced in the context by
-  \texttt{inversion} {\ident} \texttt{in} \ident$_1$ \dots\ \ident$_n$.
-\item \texttt{inversion\_clear} {\ident} \texttt{in} \ident$_1$ \ldots
-  \ident$_n$\\ 
-  \tacindex{inversion\_clear \dots\ in}
+  \texttt{inversion} {\ident} \texttt{in} \ident$_1$ \dots\ 
+  \ident$_n$.
+  
+\item \tacindex{inversion\_clear \dots\ in} \texttt{inversion\_clear}
+  {\ident} \texttt{in} \ident$_1$ \ldots \ident$_n$
+ 
   Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This
   tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and
   then performing {\tt inversion\_clear}.
-\item \texttt{inversion\_clear} {\ident} \texttt{as} {\intropattern}
-  \texttt{in} \ident$_1$ \ldots \ident$_n$\\ 
-  \tacindex{inversion\_clear \dots\ as \dots\ in}
+  
+\item \tacindex{inversion\_clear \dots\ as \dots\ in}
+  \texttt{inversion\_clear} {\ident} \texttt{as} {\intropattern}
+  \texttt{in} \ident$_1$ \ldots \ident$_n$
+
   This allows to name the hypotheses introduced in the context by
-  \texttt{inversion\_clear} {\ident} \texttt{in} \ident$_1$ \ldots \ident$_n$.
-\item \texttt{dependent inversion} {\ident}\\
-  \tacindex{dependent inversion}
-  That must be used when \ident\ appears in the current goal. 
-  It acts like \texttt{inversion} and then substitutes \ident\ for the
+  \texttt{inversion\_clear} {\ident} \texttt{in} \ident$_1$ \ldots
+  \ident$_n$.
+
+\item \tacindex{dependent inversion} \texttt{dependent inversion}
+  {\ident}  
+  
+  That must be used when \ident\ appears in the current goal.  It acts
+  like \texttt{inversion} and then substitutes \ident\ for the
   corresponding term in the goal.
-\item \texttt{dependent inversion} {\ident} \texttt{as} {\intropattern} \\
-  \tacindex{dependent inversion \dots\ as }
+  
+\item \tacindex{dependent inversion \dots\ as } \texttt{dependent
+    inversion} {\ident} \texttt{as} {\intropattern} 
+  
   This allows to name the hypotheses introduced in the context by
   \texttt{dependent inversion} {\ident}.
-\item \texttt{dependent inversion\_clear} {\ident}\\
-  \tacindex{dependent inversion\_clear}
+
+\item \tacindex{dependent inversion\_clear} \texttt{dependent
+    inversion\_clear} {\ident} 
+  
   Like \texttt{dependent inversion}, except that {\ident} is cleared
   from the local context.
-\item \texttt{dependent inversion\_clear} {\ident}\texttt{as} {\intropattern}\\
-  \tacindex{dependent inversion\_clear \dots\ as}
+
+\item \tacindex{dependent inversion\_clear \dots\ as}
+  \texttt{dependent inversion\_clear} {\ident}\texttt{as} {\intropattern}
+  
   This allows to name the hypotheses introduced in the context by
   \texttt{dependent inversion\_clear} {\ident}
-\item \texttt{dependent inversion } {\ident} \texttt{ with } \term \\
-  \tacindex{dependent inversion \dots\ with}
+
+\item \tacindex{dependent inversion \dots\ with} \texttt{dependent
+    inversion } {\ident} \texttt{ with } \term  
+  
   This variant allow to give the good generalization of the goal. It
   is useful when the system fails to generalize the goal automatically. If
   {\ident} has type $(I~\vec{t})$ and $I$ has type
   $forall (\vec{x}:\vec{T}), s$,   then \term~  must be of type
   $I:forall (\vec{x}:\vec{T}), I~\vec{x}\to s'$ where $s'$ is the
   type of the goal.
-\item \texttt{dependent inversion } {\ident} \texttt{as} {\intropattern} \texttt{ with } \term \\
-  \tacindex{dependent inversion \dots\ as \dots\ with}
+
+\item \tacindex{dependent inversion \dots\ as \dots\ with}
+  \texttt{dependent inversion } {\ident} \texttt{as} {\intropattern}
+  \texttt{ with } \term  
+  
   This allows to name the hypotheses introduced in the context by
   \texttt{dependent inversion } {\ident} \texttt{ with } \term.
-\item \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term\\
-  \tacindex{dependent inversion\_clear \dots\ with}
+
+\item \tacindex{dependent inversion\_clear \dots\ with}
+  \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term 
+  
   Like \texttt{dependent inversion \dots\ with} but clears \ident from
   the local context.
-\item \texttt{dependent inversion\_clear } {\ident} \texttt{as} {\intropattern} \texttt{ with } \term\\
-  \tacindex{dependent inversion\_clear \dots\ as \dots\ with}
+
+\item \tacindex{dependent inversion\_clear \dots\ as \dots\ with}
+  \texttt{dependent inversion\_clear } {\ident} \texttt{as}
+  {\intropattern} \texttt{ with } \term 
+  
   This allows to name the hypotheses introduced in the context by
   \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term.
-\item \texttt{simple inversion} {\ident}\\
-  \tacindex{simple inversion}
+
+\item \tacindex{simple inversion} \texttt{simple inversion} {\ident}
+  
   It is a very primitive inversion tactic that derives all the necessary
   equalities  but it does not simplify the  constraints as
   \texttt{inversion} do.
-\item \texttt{simple inversion} {\ident} \texttt{as} {\intropattern}\\
-  \tacindex{simple inversion \dots\ as}
+
+\item \tacindex{simple inversion \dots\ as} \texttt{simple inversion}
+  {\ident} \texttt{as} {\intropattern} 
+  
   This allows to name the hypotheses introduced in the context by
   \texttt{simple inversion}.
-\item \texttt{inversion} \ident \texttt{ using} \ident$'$ \\
-  \tacindex{inversion \dots\ using}
+
+\item \tacindex{inversion \dots\ using} \texttt{inversion} \ident
+  \texttt{ using} \ident$'$  
+  
   Let {\ident} have type $(I~\vec{t})$ ($I$ an inductive
   predicate) in the local context, and \ident$'$ be a (dependent) inversion
   lemma. Then, this tactic refines the current goal with the specified
   lemma.
-\item \texttt{inversion} {\ident} \texttt{using} \ident$'$ 
-  \texttt{in} \ident$_1$\dots\ \ident$_n$\\
-  \tacindex{inversion \dots\ using \dots\ in}
+
+\item \tacindex{inversion \dots\ using \dots\ in} \texttt{inversion}
+  {\ident} \texttt{using} \ident$'$ \texttt{in} \ident$_1$\dots\ \ident$_n$
+  
   This tactic behaves as generalizing \ident$_1$\dots\ \ident$_n$,
   then doing \texttt{inversion}{\ident}\texttt{using} \ident$'$.
+
 \end{Variants}
 
 \SeeAlso~\ref{inversion-examples} for detailed examples
 
 \subsection{\tt Derive Inversion {\ident} with
-  ${\tt forall (}\vec{x}{\tt :}\vec{T}{\tt),} I~\vec{t}$ Sort \sort}
+  ${\tt forall (}\vec{x}{\tt :}\vec{T}{\tt),} I~\vec{t}$ Sort \sort
 \label{Derive-Inversion}
-\comindex{Derive Inversion}
+\comindex{Derive Inversion}}
 
 This command generates an inversion principle for the
 \texttt{inversion \dots\ using} tactic.
@@ -1860,8 +1929,9 @@ the instance with the tactic {\tt inversion}.
 
 \SeeAlso \ref{inversion-examples} for examples
 
-\subsection{\tt quote \ident}\tacindex{quote}
-\index{2-level approach}
+\subsection{\tt quote \ident
+\tacindex{quote}
+\index{2-level approach}}
 
 This kind of inversion has nothing to do with the tactic
 \texttt{inversion} above. This tactic does \texttt{change (\ident\
@@ -1884,11 +1954,13 @@ 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{Automatizing}
-\label{Automatizing}
+\section{Automatizing
+\label{Automatizing}}
+
+\subsection{\tt auto
+\label{auto}
+\tacindex{auto}}
 
-\subsection{\tt auto}
-\label{auto}\tacindex{auto}
 This tactic implements a Prolog-like resolution procedure to solve the
 current goal. It first tries to solve the goal using the {\tt
   assumption} tactic, then it reduces the goal to an atomic one using
@@ -1909,11 +1981,11 @@ hints of the database named {\tt core}.
   default. 
 
 \item {\tt auto with \ident$_1$ \dots\ \ident$_n$}
-
+  
   Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to
-  the database {\tt core}. See section \ref{Hints-databases} for the list
-  of pre-defined databases and the way to create or extend a database.
-  This option can be combined with the previous one.
+  the database {\tt core}. See Section~\ref{Hints-databases} for the
+  list of pre-defined databases and the way to create or extend a
+  database.  This option can be combined with the previous one.
 
 \item {\tt auto with *}
 
@@ -1935,9 +2007,11 @@ hints of the database named {\tt core}.
 \Rem {\tt auto} either solves completely the goal or else leave it
 intact. \texttt{auto} and \texttt{trivial} never fail.
 
-\SeeAlso section \ref{Hints-databases}
+\SeeAlso Section~\ref{Hints-databases}
 
-\subsection{\tt eauto}\tacindex{eauto}\label{eauto}
+\subsection{\tt eauto
+\tacindex{eauto}
+\label{eauto}}
 
 This tactic generalizes {\tt auto}. In contrast with 
 the latter, {\tt eauto} uses unification of the goal
@@ -1958,7 +2032,7 @@ Abort.
 Note that {\tt ex\_intro} should be declared as an
 hint.
 
-\SeeAlso section~\ref{Hints-databases}
+\SeeAlso Section~\ref{Hints-databases}
 
 % EXISTE ENCORE ?
 % 
@@ -1979,8 +2053,9 @@ hint.
 %   The Prolog tactic was not able to prove the subgoal.
 % \end{ErrMsgs}
 
-\subsection{\tt tauto}
-\tacindex{tauto}\label{tauto}
+\subsection{\tt tauto
+\tacindex{tauto}
+\label{tauto}}
 
 This tactic implements a decision procedure for intuitionistic propositional
 calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
@@ -2028,8 +2103,9 @@ Abort.
 because \verb=(forall x:nat, ~ A -> P x)= cannot be treated as atomic and an
 instantiation of \verb=x= is necessary.
 
-\subsection{\tt intuition {\tac}}
-\tacindex{intuition}\label{intuition}
+\subsection{\tt intuition {\tac}
+\tacindex{intuition}
+\label{intuition}}
 
 The tactic \texttt{intuition} takes advantage of the search-tree builded
 by the decision procedure involved in the tactic {\tt tauto}. It uses
@@ -2065,9 +2141,9 @@ incompatibilities.
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
-\subsection{{\tt firstorder}}
+\subsection{{\tt firstorder}
 \tacindex{firstorder}
-\label{firstorder}
+\label{firstorder}}
 
 The tactic \texttt{firstorder} is an {\it experimental} extension of
 \texttt{tauto} to  
@@ -2098,9 +2174,9 @@ Proof-search is bounded by a depth parameter which can be set by typing the
 {\nobreak \tt Set Firstorder Depth $n$} \comindex{Set Firstorder Depth} 
 vernacular command.
 
-\subsection{{\tt jp} {\em (Jprover)}}
+\subsection{{\tt jp} {\em (Jprover)}
 \tacindex{jp}
-\label{jprover}
+\label{jprover}}
 
 The tactic \texttt{jp}, due to Huang Guan-Shieng, is an experimental
 port of the {\em Jprover}\cite{SLKN01} semi-decision procedure for
@@ -2203,9 +2279,9 @@ the proof process, its absence may lead to non-termination of the tactic.
 %   intuitionistic ones.
 % \end{ErrMsgs}
 
-\subsection{\tt congruence}
+\subsection{\tt congruence
 \tacindex{congruence}
-\label{congruence}
+\label{congruence}}
 
 The tactic {\tt congruence}, by Pierre Corbineau, implements the standard Nelson and Oppen
 congruence closure algorithm, which is a decision procedure for ground
@@ -2253,9 +2329,9 @@ congruence.
     a discriminable equality.
 \end{ErrMsgs}
 
-\subsection{\tt omega}
+\subsection{\tt omega
 \tacindex{omega}
-\label{omega}
+\label{omega}}
 
 The tactic \texttt{omega}, due to Pierre Cr{\'e}gut,
 is an automatic decision procedure for Prestburger
@@ -2267,10 +2343,10 @@ integers. This tactic must be loaded by the command \texttt{Require Import
   Omega}. See the additional documentation about \texttt{omega}
 (chapter~\ref{OmegaChapter}).
 
-\subsection{\tt ring \term$_1$ \dots\ \term$_n$}
+\subsection{\tt ring \term$_1$ \dots\ \term$_n$
 \tacindex{ring}
 \comindex{Add Ring}
-\comindex{Add Semi Ring}
+\comindex{Add Semi Ring}}
 
 This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
 associative commutative rewriting on every ring.  The tactic must be
@@ -2322,8 +2398,8 @@ You can have a look at the files \texttt{Ring.v},
 
 \SeeAlso Chapter~\ref{ring} for more detailed explanations about this tactic.
 
-\subsection{\tt field}
-\tacindex{field}
+\subsection{\tt field
+\tacindex{field}}
 
 This tactic written by David~Delahaye and Micaela~Mayero solves equalities
 using commutative field theory. Denominators have to be non equal to zero and,
@@ -2349,8 +2425,8 @@ intros; field.
 Reset Initial.
 \end{coq_eval}
 
-\subsection{\tt Add Field}
-\comindex{Add Field}
+\subsection{\tt Add Field
+\comindex{Add Field}}
 
 This vernacular command adds a commutative field theory to the database for the
 tactic {\tt field}. You must provide this theory as follows:
@@ -2401,8 +2477,8 @@ field}.
 \SeeAlso \cite{DelMay01} for more details regarding the implementation of {\tt
 field}.
 
-\subsection{\tt fourier}
-\tacindex{fourier}
+\subsection{\tt fourier
+\tacindex{fourier}}
 
 This tactic written by Lo{\"\i}c Pottier solves linear inequations on
 real numbers using Fourier's method~\cite{Fourier}. This tactic must
@@ -2423,8 +2499,8 @@ intros; fourier.
 Reset Initial.
 \end{coq_eval}
 
-\subsection{\tt autorewrite  [ \ident$_1$ \dots \ident$_n$ ]}
-\tacindex{autorewrite}
+\subsection{\tt autorewrite  [ \ident$_1$ \dots \ident$_n$ ]
+\tacindex{autorewrite}}
 
 This tactic \footnote{The behavior of this tactic has much changed compared to
 the versions available in the previous distributions (V6). This may cause
@@ -2451,8 +2527,8 @@ Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$
 $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
 \end{Variant}
 
-\subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident}
-\comindex{Hint Rewrite}
+\subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident
+\comindex{Hint Rewrite}}
 
 This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$}
 (their types must be equalities) in the rewriting base {\tt \ident}
@@ -2480,39 +2556,30 @@ be used, the tactic {\tt \tac} will be applied to the generated subgoals, the
 main subgoal excluded.
 \end{Variants}
 
-\SeeAlso \ref{autorewrite-example} for examples showing the use of this tactic.
+\SeeAlso \ref{autorewrite-example} for examples showing the use of
+this tactic. 
 
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v}
 
-\section{The hints databases for {\tt auto} and {\tt eauto}ê}
-\index{Hints databases}\label{Hints-databases}\comindex{Hint}
-
-The hints for \texttt{auto} and \texttt{eauto} are stored in databases.
-Each databases maps head
-symbols to list of hints. One can use the command \texttt{Print Hint \ident}
-to display the hints associated to the head symbol \ident{}
-(see \ref{PrintHint}). Each hint has 
-a cost that is an nonnegative integer, and a pattern. The hint is
-tried by \texttt{auto} if the conclusion of current goal matches its
-pattern, and after hints with a lower cost. The general command to add
-a hint to some databases \ident$_1$, \dots, \ident$_n$ is:
-
-The hints for \texttt{auto} and \texttt{eauto} have been reorganized
-since \Coq{} 6.2.3. They are stored in several databases. Each
-databases maps head symbols to list of hints. One can use the command
-\texttt{Print Hint \ident} to display the hints associated to the head
-symbol \ident{} (see \ref{PrintHint}). Each hint has a cost that is an
-nonnegative integer, and a pattern. The hint is tried by \texttt{auto}
-if the conclusion of current goal matches its pattern, and after hints
-with a lower cost. The general command to add a hint to some databases
-\ident$_1$, \dots, \ident$_n$ is:
-
-\begin{quotation}
+\section{The hints databases for {\tt auto} and {\tt eauto}
+\index{Hints databases}
+\label{Hints-databases}
+\comindex{Hint}}
+
+The hints for \texttt{auto} and \texttt{eauto} are stored in
+databases.  Each databases maps head symbols to list of hints. One can
+use the command \texttt{Print Hint \ident} to display the hints
+associated to the head symbol \ident{} (see \ref{PrintHint}). Each
+hint has a cost that is an nonnegative integer, and a pattern. The
+hint is tried by \texttt{auto} if the conclusion of current goal
+matches its pattern, and after hints with a lower cost. The general
+command to add a hint to some databases \ident$_1$, \dots, \ident$_n$
+is:
+\begin{tabbing}
   \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$
-\end{quotation}
-
-\noindent where {\sl hint\_definition} is one of the following expressions:
+\end{tabbing}
+where {\sl hint\_definition} is one of the following expressions:
 
 \begin{itemize}
 \item \texttt{Resolve} {\term} 
@@ -2753,10 +2820,9 @@ Furthermore, you are advised not to put your own hints in the
 {\tt core} database, but use one or several databases specific to your
 development.
 
-\subsection{\tt Print Hint}
+\subsection{\tt Print Hint
 \label{PrintHint}
-\comindex{Print Hint}
-%\index[tactic]{Hint!\texttt{Print Hint}}
+\comindex{Print Hint}}
 
 This command displays all hints that apply to the current goal. It
 fails if no proof is being edited, while the two variants can be used at
@@ -2783,42 +2849,8 @@ every moment.
 \end{Variants}
 
 
-\subsection{Hints and sections}
-\label{Hint-and-Section}
-
-Like grammar rules and structures for the \texttt{ring} tactic, things 
-added by the \texttt{Hint} command will be erased when closing a
-section.
-
-Conversely, when the user does \texttt{Require A.}, all hints 
-of the module \texttt{A} that are not defined inside a section are
-loaded.
-
-\section{Tacticals}
-\label{Tacticals}
-\index{Tacticals}
-
-We describe in this section how to combine the tactics provided by the
-system to write synthetic proof scripts called {\em tacticals}. The
-tacticals are built using tactic operators we present below.
-
-\subsection{\tt idtac}
-\tacindex{idtac}
-\index{Tacticals!idtac@{\tt idtac}} 
-
-The constant {\tt idtac} is the identity tactic: it leaves any goal
-unchanged.
-
-\subsection{\tt fail}
-\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.
-
-\subsection{\tt do {\num} {\tac}}
-\tacindex{do}
-\index{Tacticals!do@{\tt do}}
+\subsection{Hints and sections
+\label{Hint-and-Section}}
 
 Hints provided by the \texttt{Hint} commands are erased when closing a
 section. Conversely, all hints of a module \texttt{A} that are not
@@ -2826,103 +2858,9 @@ defined inside a section (and not defined with option {\tt Local}) become
 available when the module {\tt A} is imported (using
 e.g. \texttt{Require Import A.}).
 
-\subsection{\tt \tac$_1$ {\tt ||} \tac$_2$}
-\tacindex{||}
-\index{Tacticals!orelse@{\tt ||}}
-
-The tactical \tac$_1$ {\tt ||} \tac$_2$ tries to apply \tac$_1$
-and, in case of a failure, applies \tac$_2$. It associates to the
-left.
-
-\subsection{\tt repeat {\tac}}
-\tacindex{repeat}
-\index{Tacticals!repeat@{\tt repeat}}
-
-This tactic operator repeats {\tac} as long as it does not fail.
-
-\subsection{\tt {\tac}$_1$ {\tt ;} \tac$_2$}
-\tacindex{;}
-\index{Tacticals!yy@{\tt {\tac$_1$};\tac$_2$}}
-
-This tactic operator is a generalized composition for sequencing.  The
-tactical {\tac}$_1$ {\tt ;} \tac$_2$ first applies \tac$_1$ and then
-applies \tac$_2$ to any subgoal generated by \tac$_1$. {\tt ;}
-associates to the left.
-
-\subsection{\tt \tac$_0$; [ \tac$_1$ | \dots\ | \tac$_n$ ]}
-\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}
-\index{Tacticals!zz@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
-
-This tactic operator is a generalization of the precedent tactics
-operator. The tactical {\tt \tac$_0$ ; [ \tac$_1$ | \dots\ | \tac$_n$
-  ]} first applies \tac$_0$ and then applies \tac$_i$ to the i-th
-subgoal generated by \tac$_0$. It fails if $n$ is not the exact number
-of remaining subgoals.
-
-\subsection{\tt try {\tac}}
-\tacindex{try}
-\index{Tacticals!try@{\tt try}}
-
-This tactic operator applies tactic \tac, and catches the possible
-failure of \tac. It never fails.
-
-\subsection{\tt first [ \tac$_0$ | \dots\ | \tac$_n$ ]}
-\tacindex{first}
-\index{Tacticals!first@{\tt first}}
-
-This tactic operator tries to apply the tactics \tac$_i$ with $i=0\ldots{}n$,
-starting from $i=0$, until one of them does not fail. It fails if all the
-tactics fail.
-
-\begin{ErrMsgs}
-\item \errindex{No applicable tactic.}
-\end{ErrMsgs}
-
-\subsection{\tt solve [ \tac$_0$ | \dots\ | \tac$_n$ ]}
-\tacindex{solve}
-\index{Tacticals!solve@{\tt solve}}
-
-This tactic operator tries to solve the current goal with the tactics \tac$_i$
-with $i=0\ldots{}n$, starting from $i=0$, until one of them solves. It fails if
-no tactic can solve.
-
-\begin{ErrMsgs}
-\item \errindex{Cannot solve the goal.}
-\end{ErrMsgs}
-
-\subsection{\tt info {\tac}}
-\tacindex{info}
-\index{Tacticals!info@{\tt info}}
-
-This is not really a tactical. For elementary tactics, this is
-equivalent to \tac. For complex tactic like \texttt{auto}, it displays
-the operations performed by the tactic.
-
-\subsection{\tt abstract {\tac}}
-\tacindex{abstract}
-\index{Tacticals!abstract@{\tt abstract}}
-
-From outside, typing \texttt{abstract \tac} is the same that
-typing \tac. Internally it saves an auxiliary lemma called 
-{\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
-current goal and \textit{n} is chosen so that this is a fresh name.
-
-This tactical is useful with tactics such \texttt{omega} or
-\texttt{discriminate} that generate big proof terms. With that tool
-the user can avoid the explosion at time of the \texttt{Save} command
-without having to cut ``by hand'' the proof in smaller lemmas.
-
-\begin{Variants}
-
-\item \texttt{abstract {\tac} using {\ident}}.
-
-  Give explicitly the name of the auxiliary lemma.
-
-\end{Variants}
-
-\section{Generation of induction principles with {\tt Scheme}}
+\section{Generation of induction principles with {\tt Scheme}
 \label{Scheme}
-\comindex{Scheme}
+\comindex{Scheme}}
 
 The {\tt Scheme} command is a high-level tool for generating
 automatically (possibly mutual) induction principles for given types
@@ -2953,9 +2891,9 @@ general principle of mutual induction for objects in type {\term$_i$}.
 
 \SeeAlso Section~\ref{Scheme-examples}
 
-\section{Generation of induction principles with {\tt Functional Scheme}}
+\section{Generation of induction principles with {\tt Functional Scheme}
 \label{FunScheme}
-\comindex{Functional Scheme}
+\comindex{Functional Scheme}}
 
 The {\tt Functional Scheme} command is a high-level experimental
 tool for generating automatically induction principles
@@ -2987,10 +2925,10 @@ This variant can be used for non mutually recursive functions only.
 \SeeAlso Section~\ref{FunScheme-examples}
 
 
-\section{Simple tactic macros}
+\section{Simple tactic macros
 \index{tactic macros}
 \comindex{Tactic Definition}
-\label{TacticDefinition}
+\label{TacticDefinition}}
 
 A simple example has more value than a long explanation: 
 
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index def17e717..05156ba5f 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -809,25 +809,21 @@ is undecidable in general case, don't expect miracles from it!
 
 \SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring})
 
-
 \section{Using the tactical language}
 
-\subsection{About the cardinality of the natural number set}
+\subsection{About the cardinality of the set of natural numbers}
 
 A first example which shows how to use the pattern matching over the proof
 contexts is the proof that natural numbers have more than two elements. The
-proof of such a lemma can be done as shown in table~\ref{cnatltac}.
-
+proof of such a lemma can be done as %shown on Figure~\ref{cnatltac}.
+follows:
+%\begin{figure}
+%\begin{centerframe}
 \begin{coq_eval}
 Reset Initial.
 Require Import Arith.
 Require Import List.
 \end{coq_eval}
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
 \begin{coq_example*}
 Lemma card_nat :
  ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z).
@@ -840,10 +836,10 @@ elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
  end.
 Qed.
 \end{coq_example*}
-}}
-\caption{A proof on cardinality of natural numbers}
-\label{cnatltac}
-\end{table}
+%\end{centerframe}
+%\caption{A proof on cardinality of natural numbers}
+%\label{cnatltac}
+%\end{figure}
 
 We can notice that all the (very similar) cases coming from the three
 eliminations (with three distinct natural numbers) are successfully solved by
@@ -852,15 +848,8 @@ of non-linear matching).
 
 \subsection{Permutation on closed lists}
 
-Another more complex example is the problem of permutation on closed lists. The
-aim is to show that a closed list is a permutation of another one.
-
-First, we define the permutation predicate as shown in table~\ref{permutpred}.
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
+\begin{figure}
+\begin{centerframe}
 \begin{coq_example*}
 Section Sort.
 Variable A : Set.
@@ -873,37 +862,18 @@ Inductive permut : list A -> list A -> Prop :=
       forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2.
 End Sort.
 \end{coq_example*}
-}}
+\end{centerframe}
 \caption{Definition of the permutation predicate}
 \label{permutpred}
-\end{table}
-
-Next, we can write naturally the tactic and the result can be seen in
-table~\ref{permutltac}. We can notice that we use two toplevel definitions {\tt
-PermutProve} and {\tt Permut}. The function to be called is {\tt PermutProve}
-which computes the lengths of the two lists and calls {\tt Permut} with the
-length if the two lists have the same length. {\tt Permut} works as expected.
-If the two lists are equal, it concludes. Otherwise, if the lists have
-identical first elements, it applies {\tt Permut} on the tail of the lists.
-Finally, if the lists have different first elements, it puts the first element
-of one of the lists (here the second one which appears in the {\tt permut}
-predicate) at the end if that is possible, i.e., if the new first element has
-been at this place previously. To verify that all rotations have been done for
-a list, we use the length of the list as an argument for {\tt Permut} and this
-length is decremented for each rotation down to, but not including, 1 because
-for a list of length $n$, we can make exactly $n-1$ rotations to generate at
-most $n$ distinct lists. Here, it must be noticed that we use the natural
-numbers of {\Coq} for the rotation counter. In table~\ref{ltac}, we can see
-that it is possible to use usual natural numbers but they are only used as
-arguments for primitive tactics and they cannot be handled, in particular, we
-cannot make computations with them. So, a natural choice is to use {\Coq} data
-structures so that {\Coq} makes the computations (reductions) by {\tt eval
-compute in} and we can get the terms back by {\tt match}.
- 
-\begin{table}[p]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
+\end{figure}
+
+A more complex example is the problem of permutation on closed lists.
+The aim is to show that a closed list is a permutation of another one.
+First, we define the permutation predicate as shown on
+Figure~\ref{permutpred}.
+
+\begin{figure}
+\begin{centerframe}
 \begin{coq_example}
 Ltac Permut n :=
   match goal with
@@ -928,58 +898,61 @@ Ltac PermutProve :=
       end
   end.
 \end{coq_example}
-}}
+\end{centerframe}
 \caption{Permutation tactic}
 \label{permutltac}
-\end{table}
-
-With {\tt PermutProve}, we can now prove lemmas such those shown in
-table~\ref{permutlem}.
-
-\begin{table}[p]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
+\end{figure}
+
+Next, we can write naturally the tactic and the result can be seen on
+Figure~\ref{permutltac}. We can notice that we use two toplevel
+definitions {\tt PermutProve} and {\tt Permut}. The function to be
+called is {\tt PermutProve} which computes the lengths of the two
+lists and calls {\tt Permut} with the length if the two lists have the
+same length. {\tt Permut} works as expected.  If the two lists are
+equal, it concludes. Otherwise, if the lists have identical first
+elements, it applies {\tt Permut} on the tail of the lists.  Finally,
+if the lists have different first elements, it puts the first element
+of one of the lists (here the second one which appears in the {\tt
+  permut} predicate) at the end if that is possible, i.e., if the new
+first element has been at this place previously. To verify that all
+rotations have been done for a list, we use the length of the list as
+an argument for {\tt Permut} and this length is decremented for each
+rotation down to, but not including, 1 because for a list of length
+$n$, we can make exactly $n-1$ rotations to generate at most $n$
+distinct lists. Here, it must be noticed that we use the natural
+numbers of {\Coq} for the rotation counter. On Figure~\ref{ltac}, we
+can see that it is possible to use usual natural numbers but they are
+only used as arguments for primitive tactics and they cannot be
+handled, in particular, we cannot make computations with them. So, a
+natural choice is to use {\Coq} data structures so that {\Coq} makes
+the computations (reductions) by {\tt eval compute in} and we can get
+the terms back by {\tt match}.
+ 
+With {\tt PermutProve}, we can now prove lemmas as 
+% shown on Figure~\ref{permutlem}.
+follows:
+%\begin{figure}
+%\begin{centerframe}
 \begin{coq_example*}
 Lemma permut_ex1 :
   permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
-Proof.
-PermutProve.
-Qed.
-
+Proof. PermutProve. Qed.
 Lemma permut_ex2 :
   permut nat
     (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
     (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
-Proof.
-PermutProve.
-Qed.
+Proof. PermutProve. Qed.
 \end{coq_example*}
-}}
-\caption{Examples of {\tt PermutProve} use}
-\label{permutlem}
-\end{table}
+%\end{centerframe}
+%\caption{Examples of {\tt PermutProve} use}
+%\label{permutlem}
+%\end{figure}
+
 
 \subsection{Deciding intuitionistic propositional logic}
 
-The pattern matching on goals allows a complete and so a powerful
-backtracking when returning tactic values. An interesting application
-is the problem of deciding intuitionistic propositional
-logic. Considering the contraction-free sequent calculi {\tt LJT*} of
-Roy~Dyckhoff (\cite{Dyc92}), it is quite natural to code such a tactic
-using the tactic language as shown in table~\ref{tautoltac}. The
-tactic {\tt Axioms} tries to conclude using usual axioms. The tactic
-{\tt DSimplif} applies all the reversible rules of Dyckhoff's
-system. Finally, the tactic {\tt TautoProp} (the main tactic to be
-called) simplifies with {\tt DSimplif}, tries to conclude with {\tt
-Axioms} and tries several paths using the backtracking rules (one of
-the four Dyckhoff's rules for the left implication to get rid of the
-contraction and the right or).
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
+\begin{figure}[b]
+\begin{centerframe}
 \begin{coq_example}
 Ltac Axioms :=
   match goal with
@@ -987,6 +960,16 @@ Ltac Axioms :=
   | _:False |- _  => elimtype False; assumption
   | _:?A |- ?A  => auto
   end.
+\end{coq_example}
+\end{centerframe}
+\caption{Deciding intuitionistic propositions (1)}
+\label{tautoltaca}
+\end{figure}
+
+
+\begin{figure}
+\begin{centerframe}
+\begin{coq_example}
 Ltac DSimplif :=
   repeat
    (intros;
@@ -1031,47 +1014,46 @@ Ltac TautoProp :=
      | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp)
      end.
 \end{coq_example}
-}}
-\caption{Deciding intuitionistic propositions}
-\label{tautoltac}
-\end{table}
-
-For example, with {\tt TautoProp}, we can prove tautologies like those in
-table~\ref{tautolem}.
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
+\end{centerframe}
+\caption{Deciding intuitionistic propositions (2)}
+\label{tautoltacb}
+\end{figure}
+
+The pattern matching on goals allows a complete and so a powerful
+backtracking when returning tactic values. An interesting application
+is the problem of deciding intuitionistic propositional logic.
+Considering the contraction-free sequent calculi {\tt LJT*} of
+Roy~Dyckhoff (\cite{Dyc92}), it is quite natural to code such a tactic
+using the tactic language as shown on Figures~\ref{tautoltaca}
+and~\ref{tautoltacb}. The tactic {\tt Axioms} tries to conclude using
+usual axioms. The tactic {\tt DSimplif} applies all the reversible
+rules of Dyckhoff's system. Finally, the tactic {\tt TautoProp} (the
+main tactic to be called) simplifies with {\tt DSimplif}, tries to
+conclude with {\tt Axioms} and tries several paths using the
+backtracking rules (one of the four Dyckhoff's rules for the left
+implication to get rid of the contraction and the right or).
+
+For example, with {\tt TautoProp}, we can prove tautologies like
+ those:
+% on Figure~\ref{tautolem}.
+%\begin{figure}[tbp]
+%\begin{centerframe}
 \begin{coq_example*}
 Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
-Proof.
-TautoProp.
-Qed.
-
+Proof. TautoProp. Qed.
 Lemma tauto_ex2 :
    forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
-Proof.
-TautoProp.
-Qed.
+Proof. TautoProp. Qed.
 \end{coq_example*}
-}}
-\caption{Proofs of tautologies with {\tt TautoProp}}
-\label{tautolem}
-\end{table}
+%\end{centerframe}
+%\caption{Proofs of tautologies with {\tt TautoProp}}
+%\label{tautolem}
+%\end{figure}
 
 \subsection{Deciding type isomorphisms}
 
-A more tricky problem is to decide equalities between types and modulo
-isomorphisms. Here, we choose to use the isomorphisms of the simply typed
-$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example,
-\cite{RC95}). The axioms of this $\lb{}$-calculus are given by
-table~\ref{isosax}.
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
+\begin{figure}
+\begin{centerframe}
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
@@ -1092,24 +1074,19 @@ intro Heq; rewrite Heq; apply refl_equal.
 Qed.
 End Iso_axioms.
 \end{coq_example*}
-}}
+\end{centerframe}
 \caption{Type isomorphism axioms}
 \label{isosax}
-\end{table}
+\end{figure}
 
-The tactic to judge equalities modulo this axiomatization can be written as
-shown in tables~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite
-simple. Types are reduced using axioms that can be oriented (this done by {\tt
-MainSimplif}). The normal forms are sequences of Cartesian
-products without Cartesian product in the left component. These normal forms
-are then compared modulo permutation of the components (this is done by {\tt
-CompareStruct}). The main tactic to be called and realizing this algorithm is
-{\tt IsoProve}.
+A more tricky problem is to decide equalities between types and modulo
+isomorphisms. Here, we choose to use the isomorphisms of the simply typed
+$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example,
+\cite{RC95}). The axioms of this $\lb{}$-calculus are given on
+Figure~\ref{isosax}.
 
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
+\begin{figure}[ht]
+\begin{centerframe}
 \begin{coq_example}
 Ltac DSimplif trm :=
   match trm with
@@ -1143,15 +1120,13 @@ Ltac Length trm :=
   end.
 Ltac assoc := repeat rewrite <- Ass.
 \end{coq_example}
-}}
+\end{centerframe}
 \caption{Type isomorphism tactic (1)}
 \label{isosltac1}
-\end{table}
+\end{figure}
 
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
+\begin{figure}[ht]
+\begin{centerframe}
 \begin{coq_example}
 Ltac DoCompare n :=
   match goal with
@@ -1177,17 +1152,24 @@ Ltac CompareStruct :=
   end.
 Ltac IsoProve := MainSimplif; CompareStruct.
 \end{coq_example}
-}}
+\end{centerframe}
 \caption{Type isomorphism tactic (2)}
 \label{isosltac2}
-\end{table}
+\end{figure}
 
-Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
+The tactic to judge equalities modulo this axiomatization can be written as
+shown on Figures~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite
+simple. Types are reduced using axioms that can be oriented (this done by {\tt
+MainSimplif}). The normal forms are sequences of Cartesian
+products without Cartesian product in the left component. These normal forms
+are then compared modulo permutation of the components (this is done by {\tt
+CompareStruct}). The main tactic to be called and realizing this algorithm is
+{\tt IsoProve}.
 
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
+% Figure~\ref{isoslem} gives 
+Here are examples of what can be solved by {\tt IsoProve}.
+%\begin{figure}[ht]
+%\begin{centerframe}
 \begin{coq_example*}
 Lemma isos_ex1 : 
   forall A B:Set, A * unit * B = B * (unit * A).
@@ -1203,10 +1185,10 @@ Proof.
 intros; IsoProve.
 Qed.
 \end{coq_example*}
-}}
-\caption{Type equalities solved by {\tt IsoProve}}
-\label{isoslem}
-\end{table}
+%\end{centerframe}
+%\caption{Type equalities solved by {\tt IsoProve}}
+%\label{isoslem}
+%\end{figure}
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 4d876f71e..a32b27e3f 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -27,7 +27,9 @@
 \input{./headers.tex}% extension .tex pour htmlgen
 
 \begin{document}
+%BEGIN LATEX
 \sloppy\hbadness=5000
+%END LATEX
 
 \tophtml{}
 \coverpage{Reference Manual}{The Coq Development Team}
@@ -89,7 +91,7 @@
 \printindex[error]
 
 \listoffigures
-%\listoftables
+\addcontentsline{toc}{chapter}{\listfigurename}
 
 %BEGIN LATEX
 \RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps}
diff --git a/doc/Translator.tex b/doc/Translator.tex
index 423e22755..8e9f83bae 100644
--- a/doc/Translator.tex
+++ b/doc/Translator.tex
@@ -682,9 +682,6 @@ If the choices made by translation or in the following cases:
 \end{itemize}
 the user should change his development prior to translation.
 
-
-\subsubsection{Syntax extensions}
-
 \subsubsection{{\tt Case} and {\tt Match}}
 
 These very low-level case analysis are no longer supported. The
@@ -892,6 +889,4 @@ In the case you want to adopt the new semantics of {\tt Set Implicit
 Warning: changing the number of implicit arguments can break the
 notations.  Then use the {\tt V8only} modifier of {\tt Notation}.
 
->>>>>>> 1.4
-
 \end{document}
diff --git a/doc/headers.tex b/doc/headers.tex
index 277b62021..c7e46ef5c 100644
--- a/doc/headers.tex
+++ b/doc/headers.tex
@@ -20,21 +20,22 @@
 
 \renewcommand{\chaptermark}[1]{\markboth{{\bf \thechapter~#1}}{}}
 \renewcommand{\sectionmark}[1]{\markright{\thesection~#1}}
+%BEGIN LATEX
 \renewcommand{\contentsname}{%
 \protect\setheaders{Table of contents}Table of contents}
 \renewcommand{\bibname}{\protect\setheaders{Bibliography}%
-%BEGIN LATEX
 \protect\RefManCutCommand{BEGINBIBLIO=\thepage}%
-%ENDLATEX
 \protect\addcontentsline{toc}{chapter}{Bibliography}Bibliography}
+%ENDLATEX
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % For the Addendum table of contents
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \makeatletter
 
-\newcommand{\atableofcontents}{\section*{Contents}\@starttoc{atoc}}
 \newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip \bigskip \bigskip}
+%BEGIN LATEX
+\newcommand{\atableofcontents}{\section*{Contents}\@starttoc{atoc}}
 \newcommand{\achapter}[1]{
   \chapter{#1}\addcontentsline{atoc}{chapter}{#1}}
 \newcommand{\asection}[1]{
@@ -43,17 +44,25 @@
   \subsection{#1}\addcontentsline{atoc}{subsection}{#1}}
 \newcommand{\asubsubsection}[1]{
   \subsubsection{#1}\addcontentsline{atoc}{subsubsection}{#1}}
+%END LATEX
+%HEVEA \newcommand{\atableofcontents}{}
+%HEVEA \newcommand{\achapter}[1]{\chapter{#1}}
+%HEVEA \newcommand{\asection}{\section}
+%HEVEA \newcommand{\asubsection}{\subsection}
+%HEVEA \newcommand{\asubsubsection}{\subsubsection}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Reference-Manual.sh is generated to cut the Postscript
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %\@starttoc{sh}
+%BEGIN LATEX
 \newwrite\RefManCut@out%
 \immediate\openout\RefManCut@out\jobname.sh
 \newcommand{\RefManCutCommand}[1]{%
 \immediate\write\RefManCut@out{#1}}
 \newcommand{\RefManCutClose}{%
 \immediate\closeout\RefManCut@out}
+%END LATEX
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Commands for indexes
diff --git a/doc/macros.tex b/doc/macros.tex
index 71f223ad6..02dd1baef 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -4,7 +4,25 @@
 
 % For commentaries (define \com as {} for the release manual)
 %\newcommand{\com}[1]{{\it(* #1 *)}}
-\newcommand{\com}[1]{}
+%\newcommand{\com}[1]{}
+
+%BEGIN LATEX
+\newenvironment{centerframe}%
+{\bgroup
+\dimen0=\textwidth
+\advance\dimen0 by -2\fboxrule
+\advance\dimen0 by -2\fboxsep
+\setbox0=\hbox\bgroup
+\begin{minipage}{\dimen0}%
+\begin{center}}%
+{\end{center}%
+\end{minipage}\egroup
+\centerline{\fbox{\box0}}\egroup
+}
+%END LATEX
+%HEVEA \newenvironment{centerframe}{\begin{center}}{\end{center}}
+
+%HEVEA \newcommand{\vec}[1]{\textbf{#1}}
 
 %%%%%%%%%%%%%%%%%%%%%%%
 % Formatting commands %
@@ -34,16 +52,12 @@
 \newenvironment{Examples}{\medskip\noindent{\bf Examples:}
 \begin{enumerate}}{\end{enumerate}}
 
-\newcommand{\rr}{\raggedright}
-
-\newcommand{\tinyskip}{\rule{0mm}{4mm}}
-
-\newcommand{\bd}{\noindent\bf}
-\newcommand{\sbd}{\vspace{8pt}\noindent\bf}
-\newcommand{\sdoll}[1]{\begin{small}$ #1~ $\end{small}}
-\newcommand{\sdollnb}[1]{\begin{small}$ #1 $\end{small}}
+%\newcommand{\bd}{\noindent\bf}
+%\newcommand{\sbd}{\vspace{8pt}\noindent\bf}
+%\newcommand{\sdoll}[1]{\begin{small}$ #1~ $\end{small}}
+%\newcommand{\sdollnb}[1]{\begin{small}$ #1 $\end{small}}
 \newcommand{\kw}[1]{\textsf{#1}}
-\newcommand{\spec}[1]{\{\,#1\,\}}
+%\newcommand{\spec}[1]{\{\,#1\,\}}
 
 % Building regular expressions
 \newcommand{\zeroone}[1]{{\sl [}#1{\sl ]}}
@@ -55,8 +69,8 @@
 \newcommand{\sequencewithoutblank}[2]{$[$#1{\tt #2}\ldots{\tt #2}#1$]$}
 
 % Used for RefMan-gal
-\newcommand{\ml}[1]{\hbox{\tt{#1}}}
-\newcommand{\op}{\,|\,}
+%\newcommand{\ml}[1]{\hbox{\tt{#1}}}
+%\newcommand{\op}{\,|\,}
 
 %%%%%%%%%%%%%%%%%%%%%%%%
 % Trademarks and so on %
@@ -65,8 +79,6 @@
 \newcommand{\Coq}{\textsc{Coq}}
 \newcommand{\gallina}{\textsc{Gallina}}
 \newcommand{\Gallina}{\textsc{Gallina}}
-\newcommand{\coqide}{\textsc{CoqIDE}}
-\newcommand{\CoqIde}{\textsc{CoqIDE}}
 \newcommand{\CoqIDE}{\textsc{CoqIDE}}
 \newcommand{\ocaml}{\textsc{Objective Caml}}
 \newcommand{\camlpppp}{\textsc{Camlp4}}
@@ -81,7 +93,7 @@
 % Name of tactics %
 %%%%%%%%%%%%%%%%%%%
 
-\newcommand{\Natural}{\mbox{\tt Natural}}
+%\newcommand{\Natural}{\mbox{\tt Natural}}
 
 %%%%%%%%%%%%%%%%%
 % \rm\sl series %
@@ -160,7 +172,10 @@
 \newcommand{\pat}{\textrm{\textsl{pat}}}
 \newcommand{\pgs}{\textrm{\textsl{pgms}}}
 \newcommand{\pg}{\textrm{\textsl{pgm}}}
+%BEGIN LATEX
 \newcommand{\proof}{\textrm{\textsl{proof}}}
+%END LATEX
+%HEVEA \renewcommand{\proof}{\textrm{\textsl{proof}}}
 \newcommand{\record}{\textrm{\textsl{record}}}
 \newcommand{\rewrule}{\textrm{\textsl{rewriting\_rule}}}
 \newcommand{\sentence}{\textrm{\textsl{sentence}}}
@@ -246,7 +261,7 @@
 \newcommand{\Where}{{\textbf{where rec }}}
 \newcommand{\Function}{{\textbf{function }}}
 \newcommand{\Rec}{{\textbf{rec }}}
-\newcommand{\cn}{\centering}
+%\newcommand{\cn}{\centering}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Math commands and symbols %
@@ -277,31 +292,31 @@
 \newcommand{\sm}{\mbox{ }}
 \newcommand{\mx}{\mbox}
 
-\newcommand{\nq}{\neq}
-\newcommand{\eq}{\equiv}
+%\newcommand{\nq}{\neq}
+%\newcommand{\eq}{\equiv}
 \newcommand{\fa}{\forall}
-\newcommand{\ex}{\exists}
+%\newcommand{\ex}{\exists}
 \newcommand{\impl}{\rightarrow}
-\newcommand{\Or}{\vee}
-\renewcommand{\And}{\wedge}
+%\newcommand{\Or}{\vee}
+%\newcommand{\And}{\wedge}
 \newcommand{\ms}{\models}
 \newcommand{\bw}{\bigwedge}
 \newcommand{\ts}{\times}
 \newcommand{\cc}{\circ}
-\newcommand{\es}{\emptyset}
-\newcommand{\bs}{\backslash}
+%\newcommand{\es}{\emptyset}
+%\newcommand{\bs}{\backslash}
 \newcommand{\vd}{\vdash}
-\newcommand{\lan}{{\langle }}
-\newcommand{\ran}{{\rangle }}
+%\newcommand{\lan}{{\langle }}
+%\newcommand{\ran}{{\rangle }}
 
-\newcommand{\al}{\alpha}
+%\newcommand{\al}{\alpha}
 \newcommand{\bt}{\beta}
-\newcommand{\io}{\iota}
+%\newcommand{\io}{\iota}
 \newcommand{\lb}{\lambda}
-\newcommand{\sg}{\sigma}
-\newcommand{\sa}{\Sigma}
-\newcommand{\om}{\Omega}
-\newcommand{\tu}{\tau}
+%\newcommand{\sg}{\sigma}
+%\newcommand{\sa}{\Sigma}
+%\newcommand{\om}{\Omega}
+%\newcommand{\tu}{\tau}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%
 % Custom maths commands %
@@ -337,10 +352,15 @@
 \newcommand{\CIPV}[1]{\CIP{#1}{I_1.. I_k}{P_1.. P_k}}
 \newcommand{\CIPI}[1]{\CIP{#1}{I}{P}}
 \newcommand{\CIF}[1]{\mbox{$\{#1\}_{f_1.. f_n}$}}
+%BEGIN LATEX
 \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(\begin{array}[t]{l}#2:=#3
                                               \,)\end{array}$}}
 \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](\begin{array}[t]{l}#3:=#4
                                                  \,)\end{array}$}}
+%END LATEX
+%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}}
+%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}}
+
 \newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{l}#3:=#4
                                                  \,)\end{array}$}}
 \newcommand{\Def}[4]{\mbox{{\sf Def}$(#1)(#2:=#3:#4)$}}
@@ -358,6 +378,7 @@
 \newcommand{\leconvert}{\leq_{\beta\delta\iota\zeta}}
 \newcommand{\NN}{\mathbb{N}}
 \newcommand{\inference}[1]{$${#1}$$}
+
 \newcommand{\compat}[2]{\mbox{$[#1|#2]$}}
 \newcommand{\tristackrel}[3]{\mathrel{\mathop{#2}\limits_{#3}^{#1}}}
 
@@ -372,25 +393,25 @@
 \newcommand{\struct}[1]{\ensuremath{{\sf Struct}~#1~{\sf End}}}
 
 
-\newbox\tempa
-\newbox\tempb
-\newdimen\tempc
-\newcommand{\mud}[1]{\hfil $\displaystyle{\mathstrut #1}$\hfil}
-\newcommand{\rig}[1]{\hfil $\displaystyle{#1}$}
-\newcommand{\irulehelp}[3]{\setbox\tempa=\hbox{$\displaystyle{\mathstrut #2}$}%
-                        \setbox\tempb=\vbox{\halign{##\cr
-        \mud{#1}\cr
-        \noalign{\vskip\the\lineskip}
-        \noalign{\hrule height 0pt}
-        \rig{\vbox to 0pt{\vss\hbox to 0pt{${\; #3}$\hss}\vss}}\cr
-        \noalign{\hrule}
-        \noalign{\vskip\the\lineskip}
-        \mud{\copy\tempa}\cr}}
-                      \tempc=\wd\tempb
-                      \advance\tempc by \wd\tempa
-                      \divide\tempc by 2 }
-\newcommand{\irule}[3]{{\irulehelp{#1}{#2}{#3}
-                     \hbox to \wd\tempa{\hss \box\tempb \hss}}}
+%\newbox\tempa
+%\newbox\tempb
+%\newdimen\tempc
+%\newcommand{\mud}[1]{\hfil $\displaystyle{\mathstrut #1}$\hfil}
+%\newcommand{\rig}[1]{\hfil $\displaystyle{#1}$}
+% \newcommand{\irulehelp}[3]{\setbox\tempa=\hbox{$\displaystyle{\mathstrut #2}$}%
+%                         \setbox\tempb=\vbox{\halign{##\cr
+%         \mud{#1}\cr
+%         \noalign{\vskip\the\lineskip}
+%         \noalign{\hrule height 0pt}
+%         \rig{\vbox to 0pt{\vss\hbox to 0pt{${\; #3}$\hss}\vss}}\cr
+%         \noalign{\hrule}
+%         \noalign{\vskip\the\lineskip}
+%         \mud{\copy\tempa}\cr}}
+%                       \tempc=\wd\tempb
+%                       \advance\tempc by \wd\tempa
+%                       \divide\tempc by 2 }
+% \newcommand{\irule}[3]{{\irulehelp{#1}{#2}{#3}
+%                      \hbox to \wd\tempa{\hss \box\tempb \hss}}}
 
 \newcommand{\sverb}[1]{{\tt #1}}
 \newcommand{\mover}[2]{{#1\over #2}}
@@ -405,10 +426,12 @@
 
 % placement of figures
 
+%BEGIN LATEX
 \renewcommand{\topfraction}{.99}
 \renewcommand{\bottomfraction}{.99}
 \renewcommand{\textfraction}{.01}
 \renewcommand{\floatpagefraction}{.9}
+%END LATEX
 
 % Macros Bruno pour description de la syntaxe