modif generales claude

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

25 files changed, 1494 insertions, 654 deletions

diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex
index bd661aeef..29632d67f 100644
--- a/doc/AddRefMan-pre.tex
+++ b/doc/AddRefMan-pre.tex
@@ -33,7 +33,7 @@ Manual.
 %  manual of the tools he wrote for printing proofs in natural
 %  language. At this time, French and English languages are supported.
 
-\item[Omega] \texttt{Omega}, written by Pierre Crégut, solves a whole
+\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole
   class of arithmetic problems.
 
 %\item[Program] The \texttt{Program} technology intends to inverse the
@@ -41,7 +41,7 @@ Manual.
 %  programs in \Coq. This chapter is due to Catherine Parent. {\bf This
 %  feature is not available in {\Coq} version 7.}
 
-\item[The {\tt Ring} tactic] This is a tactic to do AC rewriting. This
+\item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This
   chapter explains how to use it and how it works.
   The chapter is contributed by Patrick Loiseleur.
 
diff --git a/doc/Cases.tex b/doc/Cases.tex
index aacdd0c80..a8ab494c7 100644
--- a/doc/Cases.tex
+++ b/doc/Cases.tex
@@ -409,7 +409,8 @@ Set Printing Depth 50.
 
 \begin{coq_example}
 Fixpoint concat
- (n: nat) (l:listn n) (m:nat) (l':listn m) {struct l} : listn (n + m) :=
+ (n:nat) (l:listn n) (m:nat)
+ (l':listn m) {struct l} : listn (n + m) :=
   match l, l' with
   | niln, x => x
   | consn n' a y, x => consn (n' + m) a (concat n' y m x)
diff --git a/doc/Coercion.tex b/doc/Coercion.tex
index 7a248f47f..be496adb2 100644
--- a/doc/Coercion.tex
+++ b/doc/Coercion.tex
@@ -358,7 +358,8 @@ We give an example of coercion between classes with parameters.
 
 %\begin{\small}
 \begin{coq_example}
-Parameters (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set).
+Parameters
+   (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set).
 Parameter f : forall n:nat, C n -> D (S n) true.
 Coercion f : C >-> D.
 Parameter g : forall (n:nat) (b:bool), D n b -> E b.
diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index 12a9616e2..19be94560 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -538,19 +538,23 @@ let treesort leA_dec eqA_dec l =
 \end{verbatim}
 
 Let's test it: 
-
+% Format.set_margin 72;;
 \begin{verbatim}
 # #use "heapsort.ml";;
 type sumbool = Left | Right
 type nat = O | S of nat
 type 'a tree = Tree_Leaf | Tree_Node of 'a * 'a tree * 'a tree
 type 'a list = Nil | Cons of 'a * 'a list
-val merge : ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list -> 'a list =
-  <fun>
-val heap_to_list : ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a list = <fun>
-val insert : ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a -> 'a tree = <fun>
-val list_to_heap : ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a tree = <fun>
-val treesort : ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list = <fun>
+val merge : 
+  ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list -> 'a list = <fun>
+val heap_to_list : 
+  ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a list = <fun>
+val insert : 
+  ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a -> 'a tree = <fun>
+val list_to_heap : 
+  ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a tree = <fun>
+val treesort : 
+  ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list = <fun>
 \end{verbatim}
 
 One can remark that the argument of {\tt treesort} corresponding to 
@@ -566,9 +570,9 @@ val leAdec : 'a -> 'a -> sumbool = <fun>
 # let rec listn = function 0 -> Nil
                          | n -> Cons(Random.int 10000,listn (n-1));;
 val listn : int -> int list = <fun>
-# treesort leAdec () (listn 10);;
-- : int list = Cons (136, Cons (760, Cons (1512, Cons (2776, Cons (3064, 
-Cons (4536, Cons (5768, Cons (7560, Cons (8856, Cons (8952, Nil))))))))))
+# treesort leAdec () (listn 9);;
+- : int list = Cons (160, Cons (883, Cons (1874, Cons (3275, Cons 
+  (5392, Cons (7320, Cons (8512, Cons (9632, Cons (9876, Nil)))))))))
 \end{verbatim}
 
 Some tests on longer lists (10000 elements) show that the program is
diff --git a/doc/Omega.tex b/doc/Omega.tex
index 69764336d..bbf17f630 100755
--- a/doc/Omega.tex
+++ b/doc/Omega.tex
@@ -1,29 +1,29 @@
-\achapter{\texttt{Omega}: a solver of quantifier-free problems in
+\achapter{Omega: a solver of quantifier-free problems in
 Presburger Arithmetic}
 \aauthor{Pierre Crégut}
 \label{OmegaChapter}
 
-\asection{Description of {\tt Omega}}
-\tacindex{Omega}
+\asection{Description of {\tt omega}}
+\tacindex{omega}
 \label{description}
 
-{\tt Omega}~solves a goal in Presburger arithmetic, ie a universally
+{\tt omega} solves a goal in Presburger arithmetic, i.e. a universally
 quantified formula made of equations and inequations. Equations may
 be specified either on the type \verb=nat= of natural numbers or on
 the type \verb=Z= of binary-encoded integer numbers. Formulas on
 \verb=nat= are automatically injected into \verb=Z=.  The procedure
 may use any hypothesis of the current proof session to solve the goal.
 
-Multiplication is handled by {\tt Omega}~but only goals where at
+Multiplication is handled by {\tt omega} but only goals where at
 least one of the two multiplicands of products is a constant are
 solvable. This is the restriction meaned by ``Presburger arithmetic''.
 
 If the tactic cannot solve the goal, it fails with an error message.
 In any case, the computation eventually stops.
 
-\asubsection{Arithmetical goals recognized by {\tt Omega}}
+\asubsection{Arithmetical goals recognized by {\tt omega}}
 
-{\tt Omega}~applied only to quantifier-free formulas built from the
+{\tt omega} applied only to quantifier-free formulas built from the
 connectors
 
 \begin{quote}
@@ -42,13 +42,13 @@ on atomic formulas. Atomic formulas are built from the predicates
 \verb!=, <, <=, >, >=!
 \end{quote}
 
- on \verb=Z=. In expressions of type \verb=nat=, {\tt Omega}~recognizes 
+ on \verb=Z=. In expressions of type \verb=nat=, {\tt omega} recognizes 
 
 \begin{quote}
 \verb!plus, minus, mult, pred, S, O!
 \end{quote}
 
-and in expressions of type \verb=Z=, {\tt Omega}~recognizes 
+and in expressions of type \verb=Z=, {\tt omega} recognizes 
 
 \begin{quote}
 \verb!+, -, *, Zsucc!, and constants.
@@ -58,36 +58,39 @@ All expressions of type \verb=nat= or \verb=Z= not built on these
 operators are considered abstractly as if they
 were arbitrary variables of type \verb=nat= or \verb=Z=.
 
-\asubsection{Messages from {\tt Omega}}
+\asubsection{Messages from {\tt omega}}
 \label{errors}
 
-When {\tt Omega}~does not solve the goal, one of the following errors
+When {\tt omega} does not solve the goal, one of the following errors
 is generated:
 
 \begin{ErrMsgs}
-\item \errindex{Omega can't solve this system}\\
+
+\item \errindex{omega can't solve this system}
+
   This may happen if your goal is not quantifier-free (if it is
-  universally quantified, try {\tt Intros} first; if it contains
-  existentials quantifiers too, {\tt Omega}\ is not strong enough to solve your
+  universally quantified, try {\tt intros} first; if it contains
+  existentials quantifiers too, {\tt omega} is not strong enough to solve your
   goal). This may happen also if your goal contains arithmetical
-  operators unknown from {\tt Omega}. Finally, your goal may be really
-  wrong !
+  operators unknown from {\tt omega}. Finally, your goal may be really
+  wrong!
 
-\item \errindex{Omega: Not a quantifier-free goal}\\
+\item \errindex{omega: Not a quantifier-free goal}
+  
   If your goal is universally quantified, you should first apply {\tt
-    Intro} as many time as needed.
+    intro} as many time as needed.
 
-\item \errindex{Omega: Unrecognized predicate or connective:{\rm\sl ident}}
+\item \errindex{omega: Unrecognized predicate or connective: {\sl ident}}
 
-\item \errindex{Omega: Unrecognized atomic proposition:{\rm\sl prop}}
+\item \errindex{omega: Unrecognized atomic proposition: {\sl prop}}
   
-\item \errindex{Omega: Can't solve a goal with proposition variables}
+\item \errindex{omega: Can't solve a goal with proposition variables}
 
-\item \errindex{Omega: Unrecognized proposition}
+\item \errindex{omega: Unrecognized proposition}
 
-\item \errindex{Omega: Can't solve a goal with non-linear products}
+\item \errindex{omega: Can't solve a goal with non-linear products}
 
-\item \errindex{Omega: Can't solve a goal with equality on {\rm\sl type}}
+\item \errindex{omega: Can't solve a goal with equality on {\sl type}}
 
 \end{ErrMsgs}
 
@@ -103,25 +106,24 @@ is generated:
 %      procedure (see \ref{technical}).
 % \end{itemize}
 
-% \comindex{Set Omega Time}
-% \comindex{UnSet Omega Time}
-% \comindex{Switch Omega Time}
-% \comindex{Set Omega System}
-% \comindex{UnSet Omega System}
-% \comindex{Switch Omega System}
-% \comindex{Set Omega Action}
-% \comindex{UnSet Omega Action}
-% \comindex{Switch Omega Action}
+% \comindex{Set omega Time}
+% \comindex{UnSet omega Time}
+% \comindex{Switch omega Time}
+% \comindex{Set omega System}
+% \comindex{UnSet omega System}
+% \comindex{Switch omega System}
+% \comindex{Set omega Action}
+% \comindex{UnSet omega Action}
+% \comindex{Switch omega Action}
 
- Use {\tt Set Omega {\rm\sl flag}} to set the flag
- {\rm\sl flag}. Use {\tt Unset Omega {\rm\sl flag}} to unset it and
-{\tt Switch Omega {\rm\sl flag}} to toggle it.
+% Use {\tt Set omega {\rm\sl flag}} to set the flag
+% {\rm\sl flag}. Use {\tt Unset omega {\rm\sl flag}} to unset it and
+% {\tt Switch omega {\rm\sl flag}} to toggle it.
 
-\section{Using {\tt Omega}}
+\section{Using {\tt omega}}
 
-The tactic {\tt Omega}~does not belong to the core system. It should be
+The {\tt omega} tactic does not belong to the core system. It should be
 loaded by
-
 \begin{coq_example*}
 Require Import Omega.
 Open Scope Z_scope.
@@ -167,7 +169,7 @@ intro; omega.
 
 \asubsection{Overview of the {\it OMEGA} decision procedure}
 
-The {\it OMEGA} decision procedure involved in the {\tt Omega}~tactic uses
+The {\it OMEGA} decision procedure involved in the {\tt omega} tactic uses
 a small subset of the decision procedure presented in
 
 \begin{quote}
@@ -176,8 +178,7 @@ algorithm for dependence analysis", William Pugh, Communication of the
 ACM , 1992, p 102-114.
 \end{quote}
 
-Here is an overview.
-The reader is refered to the original paper for more information.
+Here is an overview, look at the original paper for more information.
 
 \begin{itemize}
 
@@ -187,13 +188,13 @@ The reader is refered to the original paper for more information.
      equal to one.
 \item Note that each inequation defines a half space in the space of real value
      of the variables.
-\item Inequations are solved by projecting on the hyperspace defined by 
-     cancelling one of the variable. 
-     They are partitioned according to the sign of
-     the coefficient of the eliminated variable. Pairs of inequations from
-     different classes define a new edge in the projection.
-\item Redundant inequations are eliminated or merged in new equations that can
-     be eliminated by the Banerjee test.
+   \item Inequations are solved by projecting on the hyperspace
+     defined by cancelling one of the variable.  They are partitioned
+     according to the sign of the coefficient of the eliminated
+     variable. Pairs of inequations from different classes define a
+     new edge in the projection.
+   \item Redundant inequations are eliminated or merged in new
+     equations that can be eliminated by the Banerjee test.
 \item The last two steps are iterated until a contradiction is reached
      (success) or there is no more variable to eliminate (failure).
 
@@ -211,10 +212,10 @@ decision procedure is only partial.
 
 \item Much too slow.
 
-\item Certainely other bugs! You can report them to
+\item Certainly other bugs! You can report them to
 
 \begin{quote}
-  \verb=Pierre.Cregut@cnet.francetelecom.fr= 
+  \url{Pierre.Cregut@cnet.francetelecom.fr}
 \end{quote}
 
 \end{itemize}
diff --git a/doc/Polynom.tex b/doc/Polynom.tex
index 02c49577b..37633d199 100644
--- a/doc/Polynom.tex
+++ b/doc/Polynom.tex
@@ -3,11 +3,11 @@
 \label{ring}
 \tacindex{ring}
 
-This chapter presents  the \texttt{Ring} tactic.
+This chapter presents  the \texttt{ring} tactic.
 
 \asection{What does this tactic?}
 
-\texttt{Ring} does associative-commutative rewriting in ring and semi-ring
+\texttt{ring} does associative-commutative rewriting in ring and semi-ring
 structures. Assume you have two binary functions $\oplus$ and $\otimes$
 that are associative and commutative, with $\oplus$ distributive on
 $\otimes$, and two constants 0 and 1 that are unities for $\oplus$ and
@@ -24,9 +24,9 @@ different, i.e. each monomial in the sum is strictly less than the
 following monomial according to the lexicographic order. It is an easy
 theorem to show that every polynomial is equivalent (modulo the ring
 properties) to exactly one canonical sum. This canonical sum is called
-the \textit{normal form} of the polynomial. So what does \texttt{Ring}? It
+the \textit{normal form} of the polynomial. So what does \texttt{ring}? It
 normalizes polynomials over any ring or semi-ring structure. The basic
-utility of \texttt{Ring} is to simplify ring expressions, so that the user
+use of \texttt{ring} is to simplify ring expressions, so that the user
 does not have to deal manually with the theorems of associativity and
 commutativity.
 
@@ -91,7 +91,7 @@ this paragraph and use the tactic according to your intuition.
 \asection{Concrete usage in \Coq}
 
 Under a session launched by \texttt{coqtop} or \texttt{coqtop -full},
-load the \texttt{Ring} files with the command:
+load the \texttt{ring} files with the command:
 
 \begin{quotation}
 \begin{verbatim}
@@ -103,23 +103,23 @@ It does not work under \texttt{coqtop -opt} because the compiled ML
 objects used by the tactic are not linked in this binary image, and
 dynamic loading of native code is not possible in \ocaml.
 
-In order to use \texttt{Ring} on naturals, load \texttt{ArithRing}
+In order to use \texttt{ring} on naturals, load \texttt{ArithRing}
 instead; for binary integers, load the module \texttt{ZArithRing}.
 
 Then, to normalize the terms $term_1$, \dots, $term_n$ in
 the current subgoal, use the tactic:
 
 \begin{quotation}
-\texttt{Ring} $term_1$ \dots{} $term_n$
+\texttt{ring} $term_1$ \dots{} $term_n$
 \end{quotation}
-\tacindex{Ring}
+\tacindex{ring}
 
 Then the tactic guesses the type of given terms, the ring theory to
 use, the variables map, and replace each term with its normal form.
 The variables map is common to all terms
 
-\Warning \texttt{Ring $term_1$; Ring $term_2$} is not equivalent to 
-\texttt{Ring $term_1$ $term_2$}. In the latter case the variables map
+\Warning \texttt{ring $term_1$; ring $term_2$} is not equivalent to 
+\texttt{ring $term_1$ $term_2$}. In the latter case the variables map
 is shared between the two terms, and common subterm $t$ of $term_1$
 and $term_2$ will have the same associated variable number.
 
@@ -135,7 +135,7 @@ and $term_2$ will have the same associated variable number.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item \texttt{Ring}
+\item \texttt{ring}
 
   That works if the current goal is an equality between two
   polynomials. It will normalize both sides of the
@@ -150,7 +150,7 @@ and $term_2$ will have the same associated variable number.
 \asection{Add a ring structure}
 
 It can be done in the \Coq toplevel (No ML file to edit and to link
-with \Coq). First, \texttt{Ring} can handle two kinds of structure:
+with \Coq). First, \texttt{ring} can handle two kinds of structure:
 rings and semi-rings. Semi-rings are like rings without an opposite to
 addition. Their precise specification (in \gallina) can be found in
 the file
@@ -303,8 +303,8 @@ This allows automatic detection of the theory used to achieve the
 normalization. On popular demand, we can change that and allow several
 ring structures on the same set.
 
-The table of theories of \texttt{Ring} is compatible with the \Coq\ 
-sectioning mechanism. If you declare a Ring inside a section, the
+The table of ring theories is compatible with the \Coq\ 
+sectioning mechanism. If you declare a ring inside a section, the
 declaration will be thrown away when closing the section.
 And when you load a compiled file, all the \texttt{Add Ring}
 commands of this file that are not inside a section will be loaded.
@@ -321,15 +321,14 @@ load the module \texttt{ZArithRing}.
 
 \asection{How does it work?}
 
-The code of \texttt{Ring} a good  example of tactic written using
-\textit{reflection} (or \textit{internalization}, it is 
-synonymous). What is reflection? Basically,  it is writing \Coq\ tactics
-in \Coq, rather than in \ocaml. From the philosophical point of view,
-it is using the ability of the Calculus of Constructions to speak and
-reason about itself.
-For the \texttt{Ring} tactic we used 
-\Coq\ as a programming language and also as a proof environment to build a
-tactic and to prove it correctness.
+The code of \texttt{ring} is a good example of tactic written using
+\textit{reflection} (or \textit{internalization}, it is synonymous).
+What is reflection? Basically, it is writing \Coq{} tactics in \Coq,
+rather than in \ocaml. From the philosophical point of view, it is
+using the ability of the Calculus of Constructions to speak and reason
+about itself.  For the \texttt{ring} tactic we used \Coq\ as a
+programming language and also as a proof environment to build a tactic
+and to prove it correctness.
 
 The interested reader is strongly advised to have a look at the file
 \texttt{Ring\_normalize.v}. Here a type for polynomials is defined: 
@@ -366,9 +365,9 @@ its correctness w.r.t interpretation, that is:
 \begin{small}
 \begin{flushleft}
 \begin{verbatim}
-Theorem polynomial_simplify_correct : (v:(varmap A))(p:polynomial)
+Theorem polynomial_simplify_correct : forall (v:(varmap A))(p:polynomial)
   (interp v (polynomial_simplify p))
-  ==(interp v p).
+  =(interp v p).
 \end{verbatim}
 \end{flushleft}
 \end{small}
@@ -405,7 +404,7 @@ $\beta\delta\iota$ simplification extended with AC rewriting rules.
 Basically, the proof is only the application of the main
 correctness theorem to well-chosen arguments.
 
-\asection{History of \texttt{Ring}}
+\asection{History of \texttt{ring}}
 
 First Samuel Boutin designed the tactic \texttt{ACDSimpl}. 
 This tactic did lot of rewriting. But the proofs
@@ -439,7 +438,7 @@ reasoning (see \ref{DiscussReflection}). He also wrote a
 few ML code for the \texttt{Add Ring} command, that allow to register
 new rings dynamically.
 
-Proofs terms generated by \texttt{Ring} are quite small, they are
+Proofs terms generated by \texttt{ring} are quite small, they are
 linear in the number of $\oplus$ and $\otimes$ operations in the
 normalized terms. Type-checking those terms requires some time because it
 makes a large use of the conversion rule, but
@@ -449,7 +448,7 @@ memory requirements are much smaller.
 \label{DiscussReflection}
 
 Efficiency is not the only motivation to use reflection
-here. \texttt{Ring} also deals with constants, it rewrites for example the
+here. \texttt{ring} also deals with constants, it rewrites for example the
 expression $34 + 2*x -x + 12$ to the expected result $x + 46$. For the
 tactic \texttt{ACDSimpl}, the only constants were 0 and 1. So the
 expression $34 + 2*(x - 1) + 12$ is interpreted as 
@@ -461,12 +460,12 @@ result. Here rewriting is not sufficient: you have to do some kind of
 reduction (some kind of \textit{computation}) to achieve the
 normalization.
 
-The tactic \texttt{Ring} is not only faster than a classical one:
+The tactic \texttt{ring} is not only faster than a classical one:
 using reflection, we get for free integration of computation and
 reasoning that would be very complex to implement in the classic fashion.
 
 Is it the ultimate way to write tactics? 
-The answer is: yes and no. The \texttt{Ring} tactic
+The answer is: yes and no. The \texttt{ring} tactic
 uses intensively the conversion
 rule of \CIC, that is replaces proof by computation the most as it is
 possible. It can be useful in all situations where a classical tactic
diff --git a/doc/RefMan-coi.tex b/doc/RefMan-coi.tex
index ef5907016..120c1201e 100755
--- a/doc/RefMan-coi.tex
+++ b/doc/RefMan-coi.tex
@@ -173,7 +173,7 @@ The elimination of a stream introduced by a \verb!CoFixpoint! definition
 is done lazily, i.e. its definition can be expanded only when it occurs 
 at the head of an application which is the argument of a case expression. 
 Isolately it is considered as a canonical expression which 
-is completely evaluated. We can test this using the command \verb!Compute! 
+is completely evaluated. We can test this using the command \verb!compute! 
 to calculate the normal forms of some terms~:
 \begin{coq_example}
 Eval compute in (from 0).
diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex
index 4f88f600d..da21ec467 100755
--- a/doc/RefMan-com.tex
+++ b/doc/RefMan-com.tex
@@ -94,121 +94,151 @@ The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}:
 
 \begin{description}
-\item[{\tt -byte}]\ \\
+\item[{\tt -byte}]\ 
+
   Run the byte-code version of \Coq{}.
 
-\item[{\tt -opt}]\ \\
+\item[{\tt -opt}]\ 
+
   Run the native-code version of \Coq{}.
 
-\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ \\
+\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ 
+
   Add {\em directory} to the searched directories when looking for a
   file.
 
-\item[{\tt -R} {\em directory} {\dirpath}]\ \\
+\item[{\tt -R} {\em directory} {\dirpath}]\ 
+
   This maps the subdirectory structure of physical {\em directory} to
   logical {\dirpath} and adds {\em directory} and its subdirectories
   to the searched directories when looking for a file.
 
-\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ \\
+\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ 
+
   Cause \Coq~to use the state put in the file {\em file} as its input
   state. The default state is {\em initial.coq}.
   Mainly useful to build the standard input state.
 
-\item[{\tt -nois}]\ \\
+\item[{\tt -nois}]\ 
+
   Cause \Coq~to begin with an empty state. Mainly useful to build the
   standard input state.
 
-\item[{\tt -notactics}]\ \\
+\item[{\tt -notactics}]\ 
+
   Forbid the dynamic loading of tactics.
 
-\item[{\tt -init-file} {\em file}]\ \\
+\item[{\tt -init-file} {\em file}]\ 
+
   Take {\em file} as the resource file.
 
-\item[{\tt -q}]\ \\
+\item[{\tt -q}]\ 
+
   Cause \Coq~not to load the resource file.
 
-\item[{\tt -user} {\em username}]\ \\
+\item[{\tt -user} {\em username}]\ 
+
   Take resource file of user {\em username} (that is 
   \verb+~+{\em username}{\tt /.coqrc.7.0}) instead of yours.
 
-\item[{\tt -load-ml-source} {\em file}]\ \\
+\item[{\tt -load-ml-source} {\em file}]\ 
+
   Load the Caml source file {\em file}.
 
-\item[{\tt -load-ml-object} {\em file}]\ \\
+\item[{\tt -load-ml-object} {\em file}]\ 
+
   Load the Caml object file {\em file}.
 
-\item[{\tt -load-vernac-source} {\em file}]\ \\
+\item[{\tt -load-vernac-source} {\em file}]\ 
+
   Load \Coq~file {\em file}{\tt .v}
 
-\item[{\tt -load-vernac-object} {\em file}]\ \\
+\item[{\tt -load-vernac-object} {\em file}]\ 
+
   Load \Coq~compiled file {\em file}{\tt .vo}
 
 %\item[{\tt -preload} {\em file}]\ \\
 %Add {\em file}{\tt .vo} to the files to be loaded and opened
 %before making the initial state.
 %
-\item[{\tt -require} {\em file}]\ \\
+\item[{\tt -require} {\em file}]\ 
+
   Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
     Require} {\em file}).
 
-\item[{\tt -compile} {\em file}]\ \\
+\item[{\tt -compile} {\em file}]\ 
+
   This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo}.
   This option implies options {\tt -batch} and {\tt -silent}. It is
   only available for {\tt coqtop}.
 
-%\item[{\tt -compile-verbose} {\em file}]\ \\
+%\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
 %  only available for {\tt coqtop}.
 
-\item[{\tt -batch}]\ \\
+\item[{\tt -batch}]\ 
+
   Batch mode : exit just after arguments parsing. This option is only
   used by {\tt coqc}.
 
-\item[{\tt -debug}]\ \\
+\item[{\tt -debug}]\ 
+
   Switch on the debug flag.
 
-\item[{\tt -emacs}]\ \\
+\item[{\tt -emacs}]\ 
+
   Tells \Coq\ it is executed under Emacs.
 
-\item[{\tt -db}]\ \\
+\item[{\tt -db}]\ 
+
   Launch \Coq\ under the Objective Caml debugger (provided that \Coq\
   has been compiled for debugging; see next chapter).
 
-\item[{\tt -impredicative-set}]\ \\
+\item[{\tt -impredicative-set}]\ 
+
   Change the logical theory of {\Coq} by declaring the sort {\tt Set}
   impredicative; warning: this is known to be inconsistent with
   some standard axioms of classical mathematics such as the functional
-  axiom of choice or the principle of description\\
+  axiom of choice or the principle of description
+
+\item[{\tt -dont-load-proofs}]\ 
 
-\item[{\tt -dont-load-proofs}]\ \\
   This avoids loading in memory the proofs of opaque theorems
   resulting in a smaller memory requirement and faster compilation;
   warning: this invalidates some features such as the extraction tool.
 
-\item[{\tt -image} {\em file}]\ \\
+\item[{\tt -image} {\em file}]\ 
+
   This option sets the binary image to be used to be {\em file}
   instead of the standard one. Not of general use.
 
-\item[{\tt -bindir} {\em directory}]\ \\
+\item[{\tt -bindir} {\em directory}]\ 
+
   Set the directory containing \Coq\ binaries.
   It is equivalent to do \texttt{export COQBIN=}{\em directory}
   before lauching \Coq.
 
-\item[{\tt -libdir} {\em file}]\ \\
+\item[{\tt -libdir} {\em file}]\ 
+
   Set the directory containing \Coq\ libraries.
   It is equivalent to do \texttt{export COQLIB=}{\em directory}
   before lauching \Coq.
 
-\item[{\tt -where}]\ \\
+\item[{\tt -where}]\ 
+
   Print the \Coq's standard library location and exit.
 
-\item[{\tt -v}]\ \\
+\item[{\tt -v}]\ 
+
   Print the \Coq's version and exit.
 
-\item[{\tt -h}, {\tt --help}]\ \\
+\item[{\tt -h}, {\tt --help}]\ 
+
   Print a short usage and exit.
+
 \end{description}
 
 % {\tt coqtop} owns an additional option:
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index a5cc9f7e4..568f8713b 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -14,20 +14,21 @@ macro is more general than the usual record types, since it allows
 also for ``manifest'' expressions. In this sense, the \verb+Record+
 construction allows to define ``signatures''.
 
-\begin{figure}
-\begin{tabular}{|lcl|}
-\hline
+\begin{figure}[h]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{tabular}{lcl}
 {\sentence} & ++= & {\record}\\
   & & \\
-{\record} & ::= &  {\tt Record} {\ident} \sequence{\binderlet}{} {\tt :} {\sort}
-    \verb.:=. \zeroone{\ident} \verb!{! 
-    \zeroone{\nelist{\field}{;}}
-    \verb!}! \verb:.:\\
+{\record} & ::= &  {\tt Record} {\ident} \sequence{\binderlet}{} :
+  {\sort} := \zeroone{\ident} \{ \zeroone{\nelist{\field}{;}} 
+    \} . \\
   & & \\
-{\field} & ::= & {\name} \verb.:. {\type} \\
- & $|$ & {\name} {\typecstr} \verb.:=. {\term} \\
-\hline
+{\field} & ::= & {\name} : {\type} \\
+ & $|$ & {\name} {\typecstr} := {\term}
 \end{tabular}
+\end{minipage}}
+\end{center}
 \caption{Syntax for the definition of {\tt Record}}
 \label{record-syntax}
 \end{figure}
@@ -79,18 +80,24 @@ 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:
+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}
 {\tt Inductive {\ident} {\params} :{\sort} :=} \\
 ~~~~{\tt
   {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).}
 \end{tabular}
-\medskip
-
 
 To build an object of type {\ident}, one should provide the
 constructor {\ident$_0$} with $n$ terms filling the fields of
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 264987c50..93045fae6 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -212,10 +212,10 @@ chapter \ref{Cic}. Extensions of this syntax are given in chapter
 \ref{Gallina-extension}. How to customize the syntax is described in
 chapter \ref{Addoc-syntax}.
 
+\begin{figure}[htbp]
 \begin{center}
-\begin{figure}[htb]
-\begin{tabular}{|lcl@{~~~~~}r|}
-\hline
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{tabular}{lcl@{~~~~~}r}
 {\term} & ::= &
          {\tt forall} {\binderlist} {\tt ,} {\term}  &(\ref{products})\\
  & $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\
@@ -270,19 +270,20 @@ chapter \ref{Addoc-syntax}.
 {\sort} & ::= & {\tt Prop} ~$|$~ {\tt Set} ~$|$~ {\tt Type} &\\
 \hline
 \end{tabular}
+\end{minipage}}
+\end{center}
 \caption{Syntax of terms}
 \label{term-syntax}
 \index{term@{\term}}
 \index{sort@{\sort}}
 \end{figure}
-\end{center}
 
 
 
-\begin{center}
 \begin{figure}[htb]
-\begin{tabular}{|lcl|}
-\hline
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{tabular}{lcl}
 {\idparams} & ::= &  {\ident} \sequence{\binderlet}{} {\typecstr} \\
 &&\\
 {\fixpointbodies} & ::= &
@@ -316,13 +317,14 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\qualid}                              \\
  & $|$ & {\tt \_}                                  \\
  & $|$ & {\num}                                 \\
- & $|$ & {\tt (} \nelist{\pattern}{,} {\tt )}     \\
-\hline
+ & $|$ & {\tt (} \nelist{\pattern}{,} {\tt )}     
 \end{tabular}
+\end{minipage}}
+\end{center}
 \caption{Syntax of terms (continued)}
 \label{term-syntax-aux}
 \end{figure}
-\end{center}
+
 
 %%%%%%%
 
@@ -408,6 +410,11 @@ of let-binders (the first one not being a variable with value), or
 {\ident$_1$}\ldots{\ident$_n$}\,{\tt :}\,{\type} if all variables
 share the same type.
 
+{\Coq} terms are typed. {\Coq} types are recognized by the same
+syntactic class as {\term}. We denote by {\type} the semantic subclass
+of types inside the syntactic class {\term}.
+\index{type@{\type}}
+
 \subsection{Abstractions}
 \label{abstractions}
 \index{abstractions}
@@ -560,14 +567,10 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
 \section{The Vernacular}
 \label{Vernacular}
 
-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.
-\begin{figure}
-\label{sentences-syntax}
-\begin{tabular}{|lcl|}
-\hline
+\begin{figure}[tbp]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{tabular}{lcl}
 {\sentence} & ::= & {\declaration} \\
             & $|$ & {\definition} \\
             & $|$ & {\inductive} \\
@@ -611,13 +614,13 @@ and ends with a dot.
 &&\\
 {\proof} & ::= & {\tt Proof} {\tt .} {\dots} {\tt Qed} {\tt .}\\
    & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Defined} {\tt .}\\
-   & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .}\\
-\hline
+   & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .}
 \end{tabular}
+\end{minipage}}
+\end{center}
 \caption{Syntax of sentences}
+\label{sentences-syntax}
 \end{figure}
-The different kinds of command are described hereafter. They all suppose
-that the terms occurring in the sentences are well-typed.
 
 %%
 %% Axioms and Parameters
diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex
index 686e60e7d..d0d9b1ee3 100644
--- a/doc/RefMan-ide.tex
+++ b/doc/RefMan-ide.tex
@@ -6,7 +6,7 @@ The \Coq{} Integrated Development Environment is a graphical tool, to
 be used as a user-friendly replacement to \texttt{coqtop}. Its main
 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, ...
+them respectively. % CREDITS ? Proof general, lablgtk, ...
 
 \coqide{} is run by typing the command \verb|coqide| on the command
 line. Without argument, the main screen is displayed with an ``unnamed
@@ -26,7 +26,7 @@ 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}
 
@@ -39,7 +39,7 @@ prove are displayed. The lower right window is the \emph{message window},
 where various messages resulting from commands are displayed. At the
 bottom is the status bar.
 
-\section{Managing files and buffers}
+\section{Managing files and buffers, basic edition}
 
 In the script window, you may open arbitrarily many buffers to
 edit. The \emph{File} menu allows you to open files or create some,
@@ -48,6 +48,13 @@ buffers, there is always one which is the current \emph{running
   buffer}, whose name is displayed on a green background, which is the
 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
+more complex editing commands, you may launch your favorite text
+editor on the current buffer, using the \emph{Edit/External Editor}
+menu. 
+
 \section{Interactive navigation into \Coq{} scripts}
 
 The running buffer is the one where navigation takes place. The
@@ -61,8 +68,8 @@ location of the error is emphasized by a red underline.
 On Figure~\ref{fig:coqide}, the running buffer is \verb|Fermat.v|, all
 commands until the \verb|Theorem| have been already executed, and the
 user tried to go forward executing \verb|Induction n|. That command
-failed because no such tactic exist (you remember that tactics in V8.0
-are lowercase, right ?), and the wrong word is underlined.
+failed because no such tactic exist (tactics are now in
+lowercase\ldots), and the wrong word is underlined. 
 
 Notice that the green part of the running buffer is not editable. If
 you ever want to modify something you have to go backward using the up
@@ -75,9 +82,9 @@ one to go back to the beginning. If you try to go to the end, or in
 general to run several commands using the \textsf{goto} button, the
   execution will stop whenever an error is found.
 
-If you ever try to execute a long-running command, such as an
-\verb|intuition eauto with *|, and would like to abort it before its
-end, you may use the interrupt button, the red cross-like.
+If you ever try to execute a command which happens to run during a
+long time, and would like to abort it before its
+termination, you may use the interrupt button (the white cross on a red circle).
  
 Finally, notice that these navigation buttons are also available in
 the menu, where their keyboard shortcuts are given.
@@ -87,11 +94,11 @@ the menu, where their keyboard shortcuts are given.
 
 The menu \texttt{Try Tactics} provides some features for automatically
 trying to solve the current goal using simple tactics. If such a
-tactics succeeds in solving the goal, then its text is automatically
+tactic succeeds in solving the goal, then its text is automatically
 inserted into the script. There is finally a combination of these
 tactics, called the \emph{proof wizard} which will try each of them in
-turn. This wizard is also available as a tool button, with a light
-bulb shape.  The set of tactics tried by the wizard is customizable in
+turn. This wizard is also available as a tool button (the light
+bulb).  The set of tactics tried by the wizard is customizable in
 the preferences.
 
 These tactics are general ones, in particular they do not refer to
@@ -104,8 +111,8 @@ preferences if undesirable.
 \section{Vernacular commands, templates}
 
 The \texttt{Templates} menu allows to use shortcuts to insert
-vernacular commands. This is a nice menu to use if you are not sure of
-the spelling of the command you want.
+vernacular commands. This is a nice way to proceed if you are not sure
+of the spelling of the command you want.
 
 Moreover, this menu offers some \emph{templates} which will automatic
 insert a complex command like Fixpoint with a convenient shape for its
@@ -124,7 +131,7 @@ arguments.
 \fi
 %END LATEX
 \end{center}
-\caption{Coqide main screen}
+\caption{\coqide{}: the query window}
 \label{fig:querywindow}
 \end{figure}
 
@@ -139,7 +146,7 @@ demand, either by using the \texttt{Window} menu, or directly using
 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 ans run the \texttt{SearchAbout} in
+both make appear the query window and run the \texttt{SearchAbout} in
 it, displaying the result. Shortcuts \verb|F3| and \verb|F4| are for
 \verb|Check| and \verb|Print| respectively.
 Figure~\ref{fig:querywindow} displays the query window after selection
@@ -148,11 +155,13 @@ print its definition.
 
 \section{Compilation}
 
-The \verb|Compile| menu offers direct commands to compile the current
-buffer, compile a set of files using \verb|make|, and creating a
-\verb|makefile| using \verb|coq_makefile|.
-
-TODO: \verb|Next error| !
+The \verb|Compile| menu offers direct commands to:
+\begin{itemize}
+\item compile the current buffer
+\item run a compilation using \verb|make|
+\item go to the last compilation error
+\item create a \verb|makefile| using \verb|coq_makefile|.
+\end{itemize}
 
 \section{Customizations}
 
@@ -160,7 +169,7 @@ You may customize your environment using menu
 \texttt{Edit/Preferences}. A new window will be displayed, with
 several customization sections presented as a notebook. 
 
-The first section is the select the text font used for scripts, goal
+The first section is for selecting the text font used for scripts, goal
 and message windows. 
 
 The second section is devoted to file management: you may
@@ -183,6 +192,24 @@ The last section is for miscellaneous boolean settings, such as the
 ``contextual menu on goals'' feature presented in
 Section~\ref{sec:trytactics}. 
 
+Notice that these settings are saved in the file \verb|.coqiderc| of
+your home directory. 
+
+A gtk2 accelerator keymap is saved under the name \verb|.coqide.keys|.
+This file should not be edited manually: to modify a given menu
+shortcut, go to the corresponding menu item without releasing the
+mouse button, press the key you want for the new shortcut, and release
+the mouse button afterwards.
+
+For experts: it is also possible to set up a specific gtk resource
+file, under the name \verb|.coqide-gtk2rc|, following the gtk2
+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.
+
+  
 % $Id$ 
 
 %%% Local Variables: 
diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex
index 1595dccf5..2331b6226 100755
--- a/doc/RefMan-int.tex
+++ b/doc/RefMan-int.tex
@@ -11,17 +11,16 @@ the advanced user.
 %The system \Coq\ is designed to develop mathematical proofs. It can be
 %used by mathematicians to develop mathematical theories and by
 %computer scientists to write formal specifications,
-The system \Coq\ is designed to develop mathematical proofs, and
-especially to write formal specifications,
-programs and to verify that programs are correct with respect to their
-specification. It provides a specification language named \gallina. Terms of
-\gallina\ can represent programs as well as properties of these
-programs and proofs of these properties. Using the so-called
-\textit{Curry-Howard isomorphism}, programs, properties and proofs are
-formalized in the same 
-language called \textit{Calculus of Inductive Constructions}, that is
-a $\lambda$-calculus with a rich type system.
-All logical judgments in \Coq\ are typing judgments. The very heart of the Coq
+The \Coq{} system is designed to develop mathematical proofs, and
+especially to write formal specifications, programs and to verify that
+programs are correct with respect to their specification. It provides
+a specification language named \gallina. Terms of \gallina\ can
+represent programs as well as properties of these programs and proofs
+of these properties. Using the so-called \textit{Curry-Howard
+  isomorphism}, programs, properties and proofs are formalized in the
+same language called \textit{Calculus of Inductive Constructions},
+that is a $\lambda$-calculus with a rich type system.  All logical
+judgments in \Coq\ are typing judgments. The very heart of the Coq
 system is the type-checking algorithm that checks the correctness of
 proofs, in other words that checks that a program complies to its
 specification. \Coq\ also provides an interactive proof assistant to
@@ -32,12 +31,7 @@ interpretation of a command language called \textit{the vernacular}.
 
 \Coq\ has an interactive mode in which commands are interpreted as the
 user types them in from the keyboard and a compiled mode where
-commands are processed from a file.  Other modes of interaction with
-\Coq\ are possible, through an emacs shell window, an emacs generic
-user-interface for proof assistant (ProofGeneral~\cite{ProofGeneral}) 
-or through a customized interface (PCoq~\cite{Pcoq}). 
-These facilities are not documented here.
-There is also a \Coq{} Integrated Development Environment described in chapter~\ref{Addoc-coqide}
+commands are processed from a file.  
 
 \begin{itemize}
 \item The interactive mode may be used as a debugging mode in which
@@ -54,6 +48,13 @@ There is also a \Coq{} Integrated Development Environment described in chapter~\
 \end{itemize}
 These two modes are documented in chapter \ref{Addoc-coqc}.
 
+Other modes of interaction with \Coq{} are possible: through an emacs
+shell window, an emacs generic user-interface for proof assistant
+(ProofGeneral~\cite{ProofGeneral}) or through a customized interface
+(PCoq~\cite{Pcoq}).  These facilities are not documented here.  There
+is also a \Coq{} Integrated Development Environment described in
+Chapter~\ref{Addoc-coqide}.
+
 \section*{How to read this book}
 
 This is a Reference Manual, not a User Manual, then it is not made for a
@@ -67,7 +68,7 @@ below.
   theorems and proofs in the Calculus of Inductive
   Constructions. Chapter~\ref{Theories} describes the standard library
   of \Coq. Chapter~\ref{Cic} is a mathematical description of the
-  formalism. Chapter~\ref{Mod} describes the module system.
+  formalism. Chapter~\ref{chapter:Modules} describes the module system.
 
 \item The second part describes the proof engine. It is divided in
   five chapters. Chapter~\ref{Vernacular-commands} presents all
@@ -101,7 +102,8 @@ 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.
+a tactic index and a vernacular command index, and an index of error
+messages. 
 
 \section*{List of additional documentation}
 
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 13f9bd64f..f9b4d2ae0 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -93,13 +93,12 @@ constructions). They are equipped with an appealing syntax enriching the
 extension is shown on figure \ref{formulas-syntax}.
 
 \begin{figure}
-\label{formulas-syntax}
 \begin{center}
-\begin{tabular}{|lclr|}
-\hline
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{tabular}{rclr}
 {\form} & ::= & {\tt True} & ({\tt True})\\
   & $|$ & {\tt False} & ({\tt False})\\
-  & $|$ & {\verb|~|} {\form} & ({\tt not})\\
+  & $|$ & {\tt\char'176} {\form} & ({\tt not})\\
   & $|$ & {\form} {\tt /$\backslash$} {\form} & ({\tt and})\\
   & $|$ & {\form} {\tt $\backslash$/} {\form} & ({\tt or})\\
   & $|$ & {\form} {\tt ->} {\form} & (\em{primitive implication})\\
@@ -111,21 +110,28 @@ extension is shown on figure \ref{formulas-syntax}.
   & $|$ & {\tt exists2} {\ident} \zeroone{{\tt :} {\specif}} {\tt
   ,} {\form}  {\tt \&} {\form} & ({\tt ex2})\\
   & $|$ & {\term} {\tt =} {\term} & ({\tt eq})\\
-  & $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq})\\
-\hline
+  & $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq})
 \end{tabular}
+\end{minipage}}
 \end{center}
+\caption{Syntax of formulas}
+\label{formulas-syntax}
+\end{figure}
 
-\medskip
+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 The implication is not defined but primitive
+\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. 
-\caption{Syntax of formulas}
-\end{figure}
 
 \subsubsection{Propositional Connectives} \label{Connectives}
 \index{Connectives}
@@ -297,11 +303,9 @@ Abort.
 \subsection{Datatypes} \label{Datatypes}
 
 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}.
+    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}
 \index{Programming}
@@ -371,7 +375,7 @@ End projections.
 The following notions\footnote{They are defined in module {\tt
 Specif.v}} allows to build new datatypes and specifications. 
 They are available with the syntax shown on
-figure \ref{specif-syntax}\footnote{This syntax can be found in the module
+Figure~\ref{specif-syntax}\footnote{This syntax can be found in the module
 {\tt SpecifSyntax.v}}.
 
 For instance, given \verb|A:Set| and \verb|P:A->Prop|, the construct
@@ -454,10 +458,9 @@ Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B).
 \end{coq_example*}
 
 \begin{figure}
-\label{specif-syntax}
 \begin{center}
-\begin{tabular}{|lclr|}
-\hline
+\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})\\
@@ -472,11 +475,12 @@ Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B).
   & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
     \&} {\specif} {\tt \}} & ({\tt sigS2})\\
   &  & & \\
-{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair})\\
-\hline
+{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair})
 \end{tabular}
-\caption{Syntax of datatypes and specifications}
+\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
@@ -965,12 +969,13 @@ Check 2 + 3.
 
 \subsubsection{Some tactics}
 
-In addition to the Ring, Field and Fourier tactics (see chapter \ref{Tactics})
-there are:
-
-{\tt DiscrR} prove that a real integer constante c1 is non equal to
-another real integer constante c2.
-\tacindex{DiscrR}
+In addition to the \verb|ring|, \verb|field| and \verb|fourier|
+tactics (see Chapter~\ref{Tactics}) there are:
+\begin{itemize}
+\item {\tt discrR} \tacindex{discrR}
+  
+  Proves that a real integer constant $c_1$ is different from another
+  real integer constant $c_2$.  
 
 \begin{coq_example*}
 Require Import DiscrR.
@@ -985,9 +990,9 @@ discrR.
 Abort.
 \end{coq_eval}
 
-{\tt SplitAbsolu} allows us to unfold {\tt Rabsolu} contants and split 
+\item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits 
 corresponding conjonctions.
-\tacindex{SplitAbsolu}
+\tacindex{split\_Rabs}
 
 \begin{coq_example*}
 Require Import SplitAbsolu.
@@ -1002,10 +1007,10 @@ intro; split_Rabs.
 Abort.
 \end{coq_eval}
 
-{\tt SplitRmult} allows us to split a condition that a product is non equal to 
-zero into subgoals corresponding to the condition on each subterm of the 
-product.
-\tacindex{SplitRmult}
+\item {\tt split\_Rmult} allows to split a condition that a product is
+  non null into subgoals corresponding to the condition on each
+  operand of the product. 
+\tacindex{split\_Rmult}
 
 \begin{coq_example*}
 Require Import SplitRmult.
@@ -1016,8 +1021,10 @@ Goal forall x y z:R, x * y * z <> 0.
 intros; split_Rmult.
 \end{coq_example}
 
+\end{itemize}
+
 All this tactics has been written with the tactic language Ltac
-described in chapter~\ref{TacticLanguage}.  More details are available
+described in Chapter~\ref{TacticLanguage}.  More details are available
 in document \url{http://coq.inria.fr/~desmettr/Reals.ps}.
 
 \begin{coq_eval}
diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index a252a1fd9..3e3a93e7f 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -45,6 +45,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}.
+
 \begin{Remarks}
 \item The infix tacticals ``\dots\ {\tt ||} \dots'' and ``\dots\ {\tt
     ;} \dots'' are associative. 
@@ -68,41 +69,40 @@ is understood as
 \end{Remarks}
 
 
-\begin{table}[htbp]
-\noindent{}\framebox[6in][l]
-{\parbox{6in}
-{\begin{center}
+\begin{figure}[htbp]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
 \begin{tabular}{lcl}
-{\tacexpr} & \cn{}::= &
+{\tacexpr} & ::= &
            {\tacexpr} {\tt ;} {\tacexpr}\\
-& \cn{}| & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\
-& \cn{}| & {\tacexprpref}\\
+& | & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\
+& | & {\tacexprpref}\\
 \\
-{\tacexprpref} & \cn{}::= &
+{\tacexprpref} & ::= &
            {\tt do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
-& \cn{}| & {\tt info} {\tacexprpref}\\
-& \cn{}| & {\tt progress} {\tacexprpref}\\
-& \cn{}| & {\tt repeat} {\tacexprpref}\\
-& \cn{}| & {\tt try} {\tacexprpref}\\
-& \cn{}| & {\tacexprinf} \\
+& | & {\tt info} {\tacexprpref}\\
+& | & {\tt progress} {\tacexprpref}\\
+& | & {\tt repeat} {\tacexprpref}\\
+& | & {\tt try} {\tacexprpref}\\
+& | & {\tacexprinf} \\
 \\
-{\tacexprinf} & \cn{}::= &
+{\tacexprinf} & ::= &
            {\tacexprlow} {\tt ||} {\tacexprpref}\\
-& \cn{}| & {\tacexprlow}\\
+& | & {\tacexprlow}\\
 \\
-{\tacexprlow} & \cn{}::= &
+{\tacexprlow} & ::= &
 {\tt fun} \nelist{\name}{} {\tt =>} {\atom}\\
-& \cn{}| &
+& | &
 {\tt let} \nelist{\letclause}{\tt with} {\tt in}
 {\atom}\\
-& \cn{}| &
+& | &
 {\tt let rec} \nelist{\recclause}{\tt with} {\tt in}
 {\tacexpr}\\
-& \cn{}| &
+& | &
 {\tt match goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
-& \cn{}| &
+& | &
 {\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
-& \cn{}| &
+& | &
 {\tt match} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\
 & \cn{}| & {\tt abstract} {\atom}\\
 & \cn{}| & {\tt abstract} {\atom} {\tt using} {\ident} \\
@@ -119,22 +119,22 @@ is understood as
 & \cn{}| & {\qualid} \nelist{\tacarg}{}\\
 & \cn{}| & {\atom}\\
 \\
-{\atom} & \cn{}::= &
+{\atom} & ::= &
            {\qualid} \\
-& \cn{}| & ()\\
-& \cn{}| & {\tt (} {\tacexpr} {\tt )}\\
+& | & ()\\
+& | & {\tt (} {\tacexpr} {\tt )}\\
 \end{tabular}
-\end{center}}}
+\end{minipage}}
+\end{center}
 \caption{Syntax of the tactic language}
 \label{ltac}
-\end{table}
+\end{figure}
 
 
 
-\begin{table}[htbp]
-\noindent{}\framebox[6in][l]
-{\parbox{6in}
-{\begin{center}
+\begin{figure}[htbp]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
 \begin{tabular}{lcl}
 \tacarg & ::= & 
         {\qualid}\\
@@ -158,24 +158,25 @@ is understood as
 & $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\
 & $|$ & {\tt \_ =>} {\tacexpr}\\
 \end{tabular}
-\end{center}}}
+\end{minipage}}
+\end{center}
 \caption{Syntax of the tactic language (continued)}
 \label{ltac_aux}
-\end{table}
+\end{figure}
 
-\begin{table}[ht]
-\noindent{}\framebox[6in][l]
-{\parbox{6in}
-{\begin{center}
+\begin{figure}[ht]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
 \begin{tabular}{lcl}
 \nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
 \\
 \nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr}
 \end{tabular}
-\end{center}}}
+\end{minipage}}
+\end{center}
 \caption{Tactic toplevel definitions}
 \label{ltactop}
-\end{table}
+\end{figure}
 
 
 %%
@@ -203,7 +204,7 @@ of Ltac.
 %% Values are given by table~\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{table}[ht]
+%% \begin{figure}[ht]
 %% \noindent{}\framebox[6in][l]
 %% {\parbox{6in}
 %% {\begin{center}
@@ -236,7 +237,7 @@ of Ltac.
 %% \end{center}}}
 %% \caption{Values of ${\cal L}_{tac}$}
 %% \label{ltacval}
-%% \end{table}
+%% \end{figure}
 
 %% \subsection{Evaluation}
 
@@ -245,25 +246,27 @@ of Ltac.
 \index{;@{\tt ;}}
 \index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}}
 
-A sequence is an expression of the following form:
-\begin{center}
+\begin{tabbing}
 {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
-\end{center}
+\end{tabbing}
 {\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]}}
 \index{Tacticals!; [ | ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
 
-We can generalize the previous sequence operator by:
-\begin{center}
+
+We can generalize the previous sequence operator as
+\begin{tabbing}
 {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
 {\tacexpr}$_n$ {\tt ]}
-\end{center}
+\end{tabbing}
 {\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
@@ -274,9 +277,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{center}
+\begin{tabbing}
 {\tt do} {\num} {\tacexpr}
-\end{center}
+\end{tabbing}
 {\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
@@ -288,9 +291,9 @@ the {\num} applications have been completed.
 \index{Tacticals!repeat@{\tt repeat}}
 
 We have a repeat loop with:
-\begin{center}
+\begin{tabbing}
 {\tt repeat} {\tacexpr}
-\end{center}
+\end{tabbing}
 {\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
@@ -302,9 +305,9 @@ fails.
 \index{Tacticals!try@{\tt try}}
 
 We can catch the tactic errors with:
-\begin{center}
+\begin{tabbing}
 {\tt try} {\tacexpr}
-\end{center}
+\end{tabbing}
 {\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,
@@ -314,9 +317,9 @@ then the exception is re-raised with its level decremented.
 \tacindex{progress}
 
 We can check if a tactic made progress with:
-\begin{center}
+\begin{tabbing}
 {\tt progress} {\tacexpr}
-\end{center}
+\end{tabbing}
 {\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
@@ -324,15 +327,14 @@ raised.
 
 \ErrMsg \errindex{Failed to progress}
 
-
 \subsubsection{Branching}
 \tacindex{||}
 \index{Tacticals!orelse@{\tt ||}}
 
 We can easily branch with the following structure:
-\begin{center}
+\begin{tabbing}
 {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$
-\end{center}
+\end{tabbing}
 {\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.
@@ -343,9 +345,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{center}
+\begin{tabbing}
 {\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
-\end{center}
+\end{tabbing}
 {\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.
@@ -358,9 +360,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{center}
+\begin{tabbing}
 {\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
-\end{center}
+\end{tabbing}
 {\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.
@@ -373,11 +375,12 @@ 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{center}
+\begin{tabbing}
 {\tt idtac} and {\tt idtac "message"}
-\end{center}
+\end{tabbing}
 The latter variant prints the string on the standard output.
 
+
 \subsubsection{Failing}
 \tacindex{fail}
 \index{Tacticals!fail@{\tt fail}}
@@ -385,9 +388,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{center}
+\begin{tabbing}
 {\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"}
-\end{center}
+\end{tabbing}
 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
@@ -397,24 +400,19 @@ If $0$, it makes {\tt match goal} considering the next clause
 \ErrMsg \errindex{Tactic Failure "message" (level $n$)}.
 
 \subsubsection{Local definitions}
-\tacindex{let}
-\tacindex{let rec}
+\index{Ltac!let}
+\index{Ltac!let rec}
+\index{let!in Ltac}
+\index{let rec!in Ltac}
 
 Local definitions can be done as follows:
-
-%\newpage{}
-
-%\phantom{}
-%\vfill{}
-
-\begin{tabular}{l}
+\begin{tabbing}
 {\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{tabular}
-
+\end{tabbing}
 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$
@@ -427,9 +425,9 @@ argument is required.
 \subsubsection{Application}
 
 An application is an expression of the following form:
-\begin{center}
+\begin{tabbing}
 {\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$
-\end{center}
+\end{tabbing}
 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$.
@@ -441,22 +439,23 @@ definition expecting at least $n$ arguments.  The expressions
 %\subsection{Application of tactic values}
 
 \subsubsection{Function construction}
-\tacindex{fun}
+\index{fun!in Ltac}
+\index{Ltac!fun}
 
 A parameterized tactic can be built anonymously (without resorting to
 local definitions) with:
-\begin{center}
+\begin{tabbing}
 {\tt fun} {\ident${}_1$} ... {\ident${}_n$} {\tt =>} {\tacexpr}
-\end{center}
+\end{tabbing}
 Indeed, local definitions of functions are a syntactic sugar for
 binding a {\tt fun} tactic to an identifier.
 
 \subsubsection{Pattern matching on terms}
-\tacindex{match}
+\index{Ltac!match}
+\index{match!in Ltac}
 
 We can carry out pattern matching on terms with:
-
-\begin{tabular}{l}
+\begin{tabbing}
 {\tt match} {\tacexpr} {\tt with}\\
 ~~~{\cpattern}$_1$ {\tt =>} {\tacexpr}$_1$\\
 ~{\tt |} {\cpattern}$_2$ {\tt =>} {\tacexpr}$_2$\\
@@ -464,8 +463,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{tabular}
-
+\end{tabbing}
 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
@@ -478,18 +476,23 @@ goal}). If all clauses fail (in particular, there is no pattern {\_})
 then a no-matching error is raised.
 
 \begin{ErrMsgs}
-\item \errindex{No matching clauses for match}\\
-No pattern can be used and, in particular, there is no {\tt \_} pattern.
-\item \errindex{Argument of match does not evaluate to a term}\\
-This happens when {\tacexpr} does not denote a term.
+
+\item \errindex{No matching clauses for match}
+
+  No pattern can be used and, in particular, there is no {\tt \_} pattern.
+
+\item \errindex{Argument of match does not evaluate to a term}
+
+  This happens when {\tacexpr} does not denote a term.
+
 \end{ErrMsgs}
 
-\tacindex{context (in pattern)}
+\index{context!in pattern}
 There is a special form of patterns to match a subterm against the
 pattern:
-\begin{center}
+\begin{tabbing}
 {\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}
-\end{center}
+\end{tabbing}
 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
@@ -503,23 +506,25 @@ the order of matching is left unspecified.
 
 
 \subsubsection{Pattern matching on goals}
-\tacindex{match goal}
-\tacindex{match reverse goal}
+\index{Ltac!match goal}
+\index{Ltac!match reverse goal}
+\index{match goal!in Ltac}
+\index{match reverse goal!in Ltac}
 
 We can make pattern matching on goals using the following expression:
-
-\begin{tabular}{l}
+\begin{tabbing}
 {\tt match goal with}\\
-~~~$hyp_{1,1}${\tt ,}...{\tt ,}$hyp_{1,m_1}$
+~~\={\tt |} $hyp_{1,1}${\tt ,}...{\tt ,}$hyp_{1,m_1}$
    ~~{\tt |-}{\cpattern}$_1${\tt =>} {\tacexpr}$_1$\\
-~~{\tt |}$hyps_{2,1}${\tt ,}...{\tt ,}$hyp_{2,m_2}$
+  \>{\tt |} $hyp_{2,1}${\tt ,}...{\tt ,}$hyp_{2,m_2}$
    ~~{\tt |-}{\cpattern}$_2${\tt =>} {\tacexpr}$_2$\\
 ~~...\\
-~~{\tt |}$hyp_{n,1}${\tt ,}...{\tt ,}$hyp_{n,m_n}$
+  \>{\tt |} $hyp_{n,1}${\tt ,}...{\tt ,}$hyp_{n,m_n}$
    ~~{\tt |-}{\cpattern}$_n${\tt =>} {\tacexpr}$_n$\\
-~~{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\
+  \>{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\
 {\tt end}
-\end{tabular}
+\end{tabbing}
+
 
 % TODO: specify order of hypothesis and explain reverse...
 
@@ -539,8 +544,9 @@ is applied.
 
 \ErrMsg \errindex{No matching clauses for match goal}
 
-No goal pattern can be used and, in particular, there is no {\tt
-\_} goal pattern.
+  No goal pattern can be used and, in particular, there is no {\tt
+    \_} goal pattern.
+
 \medskip
 
 It is important to know that each hypothesis of the goal can be
@@ -552,14 +558,14 @@ first), but it possible to reverse this order (older first) with
 the {\tt match reverse goal with} variant.
 
 \subsubsection{Filling a term context}
-\tacindex{context (in expressions)}
+\index{context!in expression}
 
 The following expression is not a tactic in the sense that it does not
 produce subgoals but generates a term to be used in tactic
 expressions:
-\begin{center}
+\begin{tabbing}
 {\tt context} {\ident} {\tt [} {\tacexpr} {\tt ]}
-\end{center}
+\end{tabbing}
 {\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
@@ -567,34 +573,38 @@ replaces the hole of the value of {\ident} by the value of
 
 \ErrMsg \errindex{not a context variable}
 
+
 \subsubsection{Generating fresh hypothesis names}
-\tacindex{fresh}
+\index{Ltac!fresh}
+\index{fresh!in Ltac}
 
 Tactics sometimes have to generate new names for hypothesis. Letting
 the system decide a name with the {\tt intro} tactic is not so good
 since it is very awkward to retrieve the name the system gave.
 
 As before, the following expression returns a term:
-\begin{center}
+\begin{tabbing}
 {\tt fresh} {\qstring}
-\end{center}
+\end{tabbing}
 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}.
 
 \subsubsection{{\tt type of} {\term}}
-\tacindex{type of}
+%\tacindex{type of}
+\index{Ltac!type of}
+\index{type of!in Ltac}
 
 This tactic computes the type of {\term}.
 
-
 \subsubsection{Computing in a constr}
-\tacindex{eval}
+\index{Ltac!eval}
+\index{eval!in Ltac}
 
 Evaluation of a term can be performed with:
-\begin{center}
+\begin{tabbing}
 {\tt eval} {\nterm{redexpr}} {\tt in} {\term}
-\end{center}
+\end{tabbing}
 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}.
@@ -609,10 +619,10 @@ elementary tactics, this is equivalent to \tacexpr. For complex tactic
 like \texttt{auto}, it displays the operations performed by the
 tactic.
 
-
 \subsubsection{Proving a subgoal as a separate lemma}
 \tacindex{abstract}
 \index{Tacticals!abstract@{\tt abstract}}
+
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called 
 {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
@@ -640,22 +650,21 @@ Basically, tactics toplevel definitions are made as follows:
 %script is evaluated by substituting $v$ to {\ident}.
 %
 %We can define functional definitions by:\\
-\begin{center}
+\begin{tabbing}
 {\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=}
 {\tacexpr}
-\end{center}
+\end{tabbing}
 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{center}
+\begin{tabbing}
 {\tt Ltac} {\ident} {\tt := fun} {\ident}$_1$ ... {\ident}$_n$
 {\tt =>} {\tacexpr}
-\end{center}
+\end{tabbing}
 Recursive and mutual recursive function definitions are also
 possible with the syntax:
-\begin{center}
-\begin{tabular}{l}
+\begin{tabbing}
 {\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 :=}
@@ -663,12 +672,429 @@ possible with the syntax:
 ...\\
 {\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=}
 {\tacexpr}$_n$
-\end{tabular}
-\end{center}
+\end{tabbing}
 
 %This definition bloc is a set of definitions (use of
 %the same previous syntactical sugar) and the other scripts are evaluated as
 %usual except that the substitutions are lazily carried out (when an identifier
 %to be evaluated is the name of a recursive definition).
 
+\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}
+
+\begin{figure}[b]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example*}
+Section Sort.
+Variable A : Set.
+Inductive permut : list A -> list A -> Prop :=
+  | permut_refl   : forall l, permut l l
+  | permut_cons   :
+      forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1)
+  | permut_append : forall a l, permut (a :: l) (l ++ a :: nil)
+  | permut_trans  :
+      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}
+\end{figure}
+
+
+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{figure}[p]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example}
+Ltac Permut n :=
+  match goal with
+  | |- (permut _ ?l ?l) => apply permut_refl
+  | |- (permut _ (?a :: ?l1) (?a :: ?l2)) =>
+      let newn := eval compute in (length l1) in
+      (apply permut_cons; Permut newn)
+  | |- (permut ?A (?a :: ?l1) ?l2) =>
+      match eval compute in n with
+      | 1 => fail
+      | _ =>
+          let l1' := constr:(l1 ++ a :: nil) in
+          (apply (permut_trans A (a :: l1) l1' l2);
+            [ apply permut_append | compute; Permut (pred n) ])
+      end
+  end.
+Ltac PermutProve :=
+  match goal with
+  | |- (permut _ ?l1 ?l2) =>
+      match eval compute in (length l1 = length l2) with
+      | (?n = ?n) => Permut n
+      end
+  end.
+\end{coq_example}
+\end{minipage}}
+\end{center}
+\caption{Permutation tactic}
+\label{permutltac}
+\end{figure}
+
+\begin{figure}[p]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example*}
+Lemma permut_ex1 :
+  permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
+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.
+\end{coq_example*}
+\end{minipage}}
+\end{center}
+\caption{Examples of {\tt PermutProve} use}
+\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
+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}.
+
+With {\tt PermutProve}, we can now prove lemmas such those shown in
+table~\ref{permutlem}.
+
+
+\subsection{Deciding intuitionistic propositional logic}
+
+\begin{figure}[b]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example}
+Ltac Axioms :=
+  match goal with
+  | |- True => trivial
+  | _:False |- _  => elimtype False; assumption
+  | _:?A |- ?A  => auto
+  end.
+Ltac DSimplif :=
+  repeat
+   (intros;
+    match goal with
+     | id:(~ _) |- _ => red in id
+     | id:(_ /\ _) |- _ =>
+         elim id; do 2 intro; clear id
+     | id:(_ \/ _) |- _ =>
+         elim id; intro; clear id
+     | id:(?A /\ ?B -> ?C) |- _ =>
+         cut (A -> B -> C);
+          [ intro | intros; apply id; split; assumption ]
+     | id:(?A \/ ?B -> ?C) |- _ =>
+         cut (B -> C);
+          [ cut (A -> C);
+             [ intros; clear id
+             | intro; apply id; left; assumption ]
+          | intro; apply id; right; assumption ]
+     | id0:(?A -> ?B),id1:?A |- _ =>
+         cut B; [ intro; clear id0 | apply id0; assumption ]
+     | |- (_ /\ _) => split
+     | |- (~ _) => red
+     end).
+\end{coq_example}
+\end{minipage}}
+\end{center}
+\caption{Deciding intuitionistic propositions (1)}
+\label{tautoltaca}
+\end{figure}
+
+\begin{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example}
+Ltac TautoProp :=
+  DSimplif;
+   Axioms ||
+     match goal with
+     | id:((?A -> ?B) -> ?C) |- _ =>
+          cut (B -> C);
+          [ intro; cut (A -> B);
+             [ intro; cut C;
+                [ intro; clear id | apply id; assumption ]
+             | clear id ]
+          | intro; apply id; intro; assumption ]; TautoProp
+     | id:(~ ?A -> ?B) |- _ =>
+         cut (False -> B);
+          [ intro; cut (A -> False);
+             [ intro; cut B;
+                [ intro; clear id | apply id; assumption ]
+             | clear id ]
+          | intro; apply id; red; intro; assumption ]; TautoProp
+     | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp)
+     end.
+\end{coq_example}
+\end{minipage}}
+\end{center}
+\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. In Table~\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
+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{figure}[tb]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example*}
+Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
+Proof.
+TautoProp.
+Qed.
+
+Lemma tauto_ex2 :
+   forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
+Proof.
+TautoProp.
+Qed.
+\end{coq_example*}
+\end{minipage}}
+\end{center}
+\caption{Proofs of tautologies with {\tt TautoProp}}
+\label{tautolem}
+\end{figure}
+
+For example, with {\tt TautoProp}, we can prove tautologies like those in
+table~\ref{tautolem}.
+
+
+\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{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example*}
+Open Scope type_scope.
+Section Iso_axioms.
+Variables A B C : Set.
+Axiom Com : A * B = B * A.
+Axiom Ass : A * (B * C) = A * B * C.
+Axiom Cur : (A * B -> C) = (A -> B -> C).
+Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
+Axiom P_unit : A * unit = A.
+Axiom AR_unit : (A -> unit) = unit.
+Axiom AL_unit : (unit -> A) = A.
+Lemma Cons : B = C -> A * B = A * C.
+Proof.
+intro Heq; rewrite Heq; apply refl_equal.
+Qed.
+End Iso_axioms.
+\end{coq_example*}
+\end{minipage}}
+\end{center}
+\caption{Type isomorphism axioms}
+\label{isosax}
+\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}.
+
+\begin{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example}
+Ltac DSimplif trm :=
+  match trm with
+  | (?A * ?B * ?C) =>
+      rewrite <- (Ass A B C); try MainSimplif
+  | (?A * ?B -> ?C) =>
+      rewrite (Cur A B C); try MainSimplif
+  | (?A -> ?B * ?C) =>
+      rewrite (Dis A B C); try MainSimplif
+  | (?A * unit) =>
+      rewrite (P_unit A); try MainSimplif
+  | (unit * ?B) =>
+      rewrite (Com unit B); try MainSimplif
+  | (?A -> unit) =>
+      rewrite (AR_unit A); try MainSimplif
+  | (unit -> ?B) =>
+      rewrite (AL_unit B); try MainSimplif
+  | (?A * ?B) =>
+      (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
+  | (?A -> ?B) =>
+      (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
+  end
+ with MainSimplif :=
+  match goal with
+  | |- (?A = ?B) => try DSimplif A; try DSimplif B
+  end.
+Ltac Length trm :=
+  match trm with
+  | (_ * ?B) => let succ := Length B in constr:(S succ)
+  | _ => constr:1
+  end.
+Ltac assoc := repeat rewrite <- Ass.
+\end{coq_example}
+\end{minipage}}
+\end{center}
+\caption{Type isomorphism tactic (1)}
+\label{isosltac1}
+\end{figure}
+
+\begin{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example}
+Ltac DoCompare n :=
+  match goal with
+  | [ |- (?A = ?A) ] => apply refl_equal
+  | [ |- (?A * ?B = ?A * ?C) ] =>
+    apply Cons; let newn := Length B in DoCompare newn
+  | [ |- (?A * ?B = ?C) ] =>
+    match eval compute in n with
+    | 1 => fail
+    | _ =>
+      pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n)
+    end
+  end.
+Ltac CompareStruct :=
+  match goal with
+  | [ |- (?A = ?B) ] =>
+      let l1 := Length A
+      with l2 := Length B in
+      match eval compute in (l1 = l2) with
+      | (?n = ?n) => DoCompare n
+      end
+  end.
+Ltac IsoProve := MainSimplif; CompareStruct.
+\end{coq_example}
+\end{minipage}}
+\end{center}
+\caption{Type isomorphism tactic (2)}
+\label{isosltac2}
+\end{figure}
+
+Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
+
+\begin{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example*}
+Lemma isos_ex1 : 
+  forall A B:Set, A * unit * B = B * (unit * A).
+Proof.
+intros; IsoProve.
+Qed.
+
+Lemma isos_ex2 :
+  forall A B C:Set,
+    (A * unit -> B * (C * unit)) =
+    (A * unit -> (C -> unit) * C) * (unit -> A -> B).
+Proof.
+intros; IsoProve.
+Qed.
+\end{coq_example*}
+\end{minipage}}
+\end{center}
+\caption{Type equalities solved by {\tt IsoProve}}
+\label{isoslem}
+\end{figure}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
diff --git a/doc/RefMan-mod.tex b/doc/RefMan-mod.tex
index de4f14fa5..1999d47dd 100644
--- a/doc/RefMan-mod.tex
+++ b/doc/RefMan-mod.tex
@@ -1,48 +1,67 @@
-\section{Module system}\index{Modules}\label{Modules}
+\section{Module system}
+\index{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{tabular}{|rcl|}
-\hline
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{tabular}{rcl}
 {\modtype}  & ::= & {\ident} \\
- & $|$ & {\modtype} \texttt{ with Definition }{\ident} \verb.:=. {\term} \\
- & $|$ & {\modtype} \texttt{ with Module }{\ident} \verb.:=. {\qualid} \\
+ & $|$ & {\modtype} \texttt{ with Definition }{\ident} := {\term} \\
+ & $|$ & {\modtype} \texttt{ with Module }{\ident} := {\qualid} \\
  &&\\
 
-{\onemodbinding}  & ::= & {\tt ( \nelist{\ident}{} \verb.:. {\modtype} )}\\
+{\onemodbinding}  & ::= & {\tt ( \nelist{\ident}{} : {\modtype} )}\\
  &&\\
 
 {\modbindings} & ::= & \nelist{\onemodbinding}{}\\
  &&\\
 
-{\modexpr} & ::= & \nelist{\qualid}{} \\
-\hline
+{\modexpr} & ::= & \nelist{\qualid}{} 
 \end{tabular}
+\end{minipage}}
+\end{center}
 \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}.
 
 \begin{Variants}
-\item{\tt Module {\ident} {\modbindings}}\\
+
+\item{\tt Module {\ident} {\modbindings}}
+
   Starts an interactive functor with parameters given by {\modbindings}.
-\item{\tt Module {\ident} \verb.:. {\modtype}}\\
+
+\item{\tt Module {\ident} \verb.:. {\modtype}}
+
   Starts an interactive module specifying its module type. 
-\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype}}\\
+
+\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype}}
+
   Starts an interactive functor with parameters given by
   {\modbindings}, and output module type {\modtype}.
-\item{\tt Module {\ident} \verb.<:. {\modtype}}\\
+
+\item{\tt Module {\ident} \verb.<:. {\modtype}}
+
   Starts an interactive module satisfying {\modtype}. 
-\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype}}\\
+
+\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype}}
+
   Starts an interactive functor with parameters given by
   {\modbindings}. The output module type is verified against the
   module type {\modtype}.
+
 \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
 is signaled if the matching fails. If the module is basic (is not a
@@ -56,34 +75,54 @@ now available through the dot notation.
 \end{ErrMsgs}
 
 
-\subsection{\tt Module {\ident} := {\modexpr}}\comindex{Module}
-This command defines the module identifier {\ident} to be equal to {\modexpr}.
+\subsection{\tt Module {\ident} := {\modexpr}}
+\comindex{Module}
+
+This command defines the module identifier {\ident} to be equal to
+{\modexpr}. 
 
 \begin{Variants}
-\item{\tt Module {\ident} {\modbindings} := {\modexpr}}\\
+\item{\tt Module {\ident} {\modbindings} := {\modexpr}}
+
  Defines a functor with parameters given by {\modbindings} and body {\modexpr}.
+
 % Particular cases of the next 2 items
-%\item{\tt Module {\ident} \verb.:. {\modtype} := {\modexpr}}\\
+%\item{\tt Module {\ident} \verb.:. {\modtype} := {\modexpr}}
+%
 %  Defines a module with body {\modexpr} and interface {\modtype}.
-%\item{\tt Module {\ident} \verb.<:. {\modtype} := {\modexpr}}\\
+%\item{\tt Module {\ident} \verb.<:. {\modtype} := {\modexpr}}
+%
 %  Defines a module with body {\modexpr}, satisfying {\modtype}.
-\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype} := {\modexpr}}\\
+
+\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype} :=
+    {\modexpr}}
+
   Defines a functor with parameters given by {\modbindings} (possibly none),
   and output module type {\modtype}, with body {\modexpr}. 
-\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype} := {\modexpr}}\\
+
+\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype} :=
+    {\modexpr}}
+
   Defines a functor with parameters given by {\modbindings} (possibly none) 
   with body {\modexpr}. The body is checked against {\modtype}.
+
 \end{Variants}
 
 \subsection{\tt Module Type {\ident}}\comindex{Module Type}
+
 This command is used to start an interactive module type {\ident}.
 
 \begin{Variants}
-\item{\tt Module Type {\ident} {\modbindings}}\\
+
+\item{\tt Module Type {\ident} {\modbindings}}
+
   Starts an interactive functor type with parameters given by {\modbindings}.
+
 \end{Variants}
 
-\subsection{\tt End {\ident}}\comindex{End}
+\subsection{\tt End {\ident}}
+\comindex{End}
+
 This command closes the interactive module type {\ident}.
 
 \begin{ErrMsgs}
@@ -91,11 +130,13 @@ This command closes the interactive module type {\ident}.
 \end{ErrMsgs}
 
 \subsection{\tt Module Type {\ident} := {\modtype}}
-Define a module type {\ident} equal to {\modtype}.
+
+Defines a module type {\ident} equal to {\modtype}.
 
 \begin{Variants}
-\item {\tt Module Type {\ident} {\modbindings} := {\modtype}} \\
-  Define a functor type {\ident} specifying functors taking arguments
+\item {\tt Module Type {\ident} {\modbindings} := {\modtype}}
+
+  Defines a functor type {\ident} specifying functors taking arguments
   {\modbindings} and returning {\modtype}.
 \end{Variants}
 
@@ -104,34 +145,50 @@ Starts an interactive module declaration. This command is available
 only in module types. 
 
 \begin{Variants}
-\item{\tt Declare Module {\ident} {\modbindings}}\\
+
+\item{\tt Declare Module {\ident} {\modbindings}}
+
   Starts an interactive declaration of a functor with parameters given
   by {\modbindings}.
+
 % Particular case of the next item
-%\item{\tt Declare Module {\ident} \verb.<:. {\modtype}}\\
+%\item{\tt Declare Module {\ident} \verb.<:. {\modtype}}
+%
 %  Starts an interactive declaration of a module satisfying {\modtype}.
-\item{\tt Declare Module {\ident} {\modbindings} \verb.<:. {\modtype}}\\
+
+\item{\tt Declare Module {\ident} {\modbindings} \verb.<:. {\modtype}}
+
   Starts an interactive declaration of a functor with parameters given
   by {\modbindings} (possibly none). The declared output module type is
   verified against the module type {\modtype}.
+
 \end{Variants}
 
 \subsection{\tt End {\ident}}
+
 This command closes the interactive declaration of module {\ident}.
 
 \subsection{\tt Declare Module {\ident} : {\modtype}}
+
 Declares a module of {\ident} of type {\modtype}. This command is available
 only in module types. 
 
 \begin{Variants}
-\item{\tt Declare Module {\ident} {\modbindings} \verb.:. {\modtype}}\\
+
+\item{\tt Declare Module {\ident} {\modbindings} \verb.:. {\modtype}}
+
   Declares a functor with parameters {\modbindings} and output module
   type {\modtype}.
-\item{\tt Declare Module {\ident} := {\qualid}}\\
+
+\item{\tt Declare Module {\ident} := {\qualid}}
+
   Declares a module equal to the module {\qualid}.
-\item{\tt Declare Module {\ident} \verb.<:. {\modtype} := {\qualid}}\\
+
+\item{\tt Declare Module {\ident} \verb.<:. {\modtype} := {\qualid}}
+
   Declares a module equal to the module {\qualid}, verifying that the
   module type of the latter is a subtype of {\modtype}.
+
 \end{Variants}
 
 
@@ -147,12 +204,9 @@ Module M.
   Defined.
 End M.
 \end{coq_example}
-
-\noindent
 Inside a module one can define constants, prove theorems and do any
 other things that can be done in the toplevel. Components of a closed
 module can be accessed using the dot notation:
-
 \begin{coq_example}
 Print M.x.
 \end{coq_example}
@@ -163,8 +217,6 @@ Module Type SIG.
   Parameter x : T.
 End SIG.
 \end{coq_example}
-
-\noindent
 Inside a module type the proof editing mode is not available.
 Consequently commands like \texttt{Definition}\ without body,
 \texttt{Lemma}, \texttt{Theorem} are not allowed.  In order to declare
@@ -203,7 +255,7 @@ transparent constraint
 Module P <: SIG := M.
 Print P.y.
 \end{coq_example}
-Now let us create a functor, i.e.\ a parametric module
+Now let us create a functor, i.e. a parametric module
 \begin{coq_example}
 Module Two (X Y: SIG).
 \end{coq_example}
@@ -303,24 +355,30 @@ Reset Mod.
 
 
 \begin{Variants}
-\item{\tt Export {\qualid}}\comindex{Export}\\
+\item{\tt Export {\qualid}}\comindex{Export}
+
   When the module containing the command {\tt Export {\qualid}} is
   imported, {\qualid} is imported as well.
 \end{Variants}
 
 \begin{ErrMsgs}
-  \item \errindex{{\qualid} is not a module}
+  \item \errindexbis{{\qualid} is not a module}{is not a module}
 % this error is impossible in the import command
 %  \item \errindex{Cannot mask the absolute name {\qualid} !}
 \end{ErrMsgs}
+
 \begin{Warnings}
   \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 f9a251fdc..055e2313f 100644
--- a/doc/RefMan-modr.tex
+++ b/doc/RefMan-modr.tex
@@ -1,5 +1,5 @@
 \chapter{The Module System}
-\label{Mod}
+\label{chapter:Modules}
 
 The module system extends the Calculus of Inductive Constructions
 providing a convenient way to structure large developments as well as
diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index e065d54ed..392d68658 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -23,7 +23,7 @@ global constant.
 \comindex{About}\\ 
 This displays various informations about the object denoted by {\qualid}:
 its kind (module, constant, assumption, inductive,
-constructor, abbreviation, ...), long name, type, implicit
+constructor, abbreviation\ldots), long name, type, implicit
 arguments and argument scopes.
 
 %\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\
@@ -79,9 +79,9 @@ displayed in Objective Caml syntax, where global identifiers are still
 displayed as in \Coq\ terms.
 
 \begin{Variants}
-\item \texttt{Recursive Extraction {\qualid$_1$} ... {\qualid$_n$}.}\\
+\item \texttt{Recursive Extraction {\qualid$_1$} \ldots{} {\qualid$_n$}.}\\
   Recursively extracts all the material needed for the extraction of 
-  globals {\qualid$_1$} ... {\qualid$_n$}.
+  globals {\qualid$_1$} \ldots{} {\qualid$_n$}.
 \end{Variants}
 
 \SeeAlso chapter~\ref{Extraction}.
@@ -154,14 +154,15 @@ environment}\\
 
 \begin{Variants}
 \item
-{\tt Search {\qualid} inside {\module$_1$}...{\module$_n$}.}
+{\tt Search {\qualid} inside {\module$_1$} \ldots{} {\module$_n$}.}
 
-This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.
+This restricts the search to constructions defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
 
-\item {\tt Search {\qualid} outside {\module$_1$}...{\module$_n$}.}
+\item {\tt Search {\qualid} outside {\module$_1$} \ldots{} {\module$_n$}.}
 
 This restricts the search to constructions not defined in modules
-{\module$_1$}...{\module$_n$}.
+{\module$_1$} \ldots{} {\module$_n$}.
 
 \begin{ErrMsgs}
 \item \errindex{Module/section \module{} not found}
@@ -202,13 +203,14 @@ SearchAbout [ Zmult Zplus "distr" ].
   inside {\module$_1$} \ldots{} {\module$_n$}.}
 
 This restricts the search to constructions defined in modules
-{\module$_1$}...{\module$_n$}.
+{\module$_1$} \ldots{} {\module$_n$}.
 
-\item {\tt SearchAbout {\term} outside {\module$_1$}...{\module$_n$}.}\\
-{\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ] outside {\module$_1$}...{\module$_n$}.}
+\item {\tt SearchAbout {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}\\
+{\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
+  outside {\module$_1$} \ldots{} {\module$_n$}.}
 
 This restricts the search to constructions not defined in modules
-{\module$_1$}...{\module$_n$}.
+{\module$_1$} \ldots{} {\module$_n$}.
 
 \end{Variants}
 
@@ -234,15 +236,16 @@ SearchPattern (?X1 + _ = _ + ?X1).
 
 \begin{Variants}
 \item {\tt SearchPattern {\term} inside
-{\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... inside
-...}
+{\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} inside
+\ldots{}}
 
-This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.
+This restricts the search to constructions defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
 
-\item {\tt SearchPattern {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... outside ...}
+\item {\tt SearchPattern {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} outside \ldots{}}
 
 This restricts the search to constructions not defined in modules
-{\module$_1$}...{\module$_n$}.
+{\module$_1$} \ldots{} {\module$_n$}.
 
 \end{Variants}
 
@@ -259,14 +262,15 @@ SearchRewrite (_ + _ + _).
 
 \begin{Variants}
 \item {\tt SearchRewrite {\term} inside
-{\module$_1$}...{\module$_n$}.}
+{\module$_1$} \ldots{} {\module$_n$}.}
 
-This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.
+This restricts the search to constructions defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
 
-\item {\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.}
+\item {\tt SearchRewrite {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}
 
 This restricts the search to constructions not defined in modules
-{\module$_1$}...{\module$_n$}.
+{\module$_1$} \ldots{} {\module$_n$}.
 
 \end{Variants}
 
diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index b84d1b38a..1411d9afb 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -81,17 +81,29 @@ memory overflow.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Defined.}\comindex{Defined} \label{Defined} \\
+
+\item {\tt Defined.}
+\comindex{Defined} 
+\label{Defined} 
+
   Defines the proved term as a transparent constant.
-\item {\tt Save.}\comindex{Save}\\
+
+\item {\tt Save.}
+\comindex{Save}
+
   Is equivalent to {\tt Qed}.
-\item {\tt Save {\ident}.}\\ Forces the name of the original goal to
-be {\ident}.  This command (and the following ones) can only be used
-if the original goal has been opened using the {\tt Goal} command.
+
+\item {\tt Save {\ident}.}
+  
+  Forces the name of the original goal to be {\ident}.  This command
+  (and the following ones) can only be used if the original goal has
+  been opened using the {\tt Goal} command.
+
 \item {\tt Save Theorem {\ident}.} \\
  {\tt Save Lemma {\ident}.} \\
  {\tt Save Remark {\ident}.}\\
- {\tt Save Fact {\ident}.}\\
+ {\tt Save Fact {\ident}.}
+
   Are equivalent to {\tt Save {\ident}.} 
 \end{Variants}
 
@@ -99,36 +111,53 @@ if the original goal has been opened using the {\tt Goal} command.
 This command is available in interactive editing proof mode to give up
 the current proof and declare the initial goal as an axiom.
 
-\subsection{\tt Theorem {\ident} : {\form}.}\comindex{Theorem}\label{Theorem}
+\subsection{\tt Theorem {\ident} : {\form}.}
+\comindex{Theorem}
+\label{Theorem}
+
 This command switches to interactive editing proof mode and declares
 {\ident} as being the name of the original goal {\form}. When declared
 as a {\tt Theorem}, the name {\ident} is known at all section levels:
 {\tt Theorem} is a {\sl global} lemma.
 
 %\ErrMsg (see section \ref{Goal})
+
 \begin{ErrMsgs}
+
 \item \errindex{the term \form\ has type \ldots{} which should be Set,
     Prop or Type}
-\item \ident\ \errindex{already exists}\\ 
+
+\item \errindexbis{\ident already exists}{already exists}
+ 
   The name you provided already defined. You have then to choose
   another name.
+
 \end{ErrMsgs}
 
 
 \begin{Variants}
-\item {\tt Lemma {\ident} : {\form}.}\comindex{Lemma}\\
+
+\item {\tt Lemma {\ident} : {\form}.}
+\comindex{Lemma}
+
   It is equivalent to {\tt Theorem {\ident} : {\form}.}
+
 \item {\tt Remark {\ident} : {\form}.}\comindex{Remark}\\
-  {\tt Fact {\ident} : {\form}.}\comindex{Fact}\\
+  {\tt Fact {\ident} : {\form}.}\comindex{Fact}
+
   Used to have a different meaning, but are now equivalent to {\tt
   Theorem {\ident} : {\form}.} They are kept for compatibility.
+
 \item {\tt Definition {\ident} : {\form}.}
-\comindex{Definition}\\
+\comindex{Definition}
+
   Analogous to {\tt Theorem}, intended to be used in conjunction with
   {\tt Defined} (see \ref{Defined}) in order to define a
   transparent constant.
+
 \item {\tt Local {\ident} : {\form}.}
-\comindex{Local}\\
+\comindex{Local}
+
   Analogous to {\tt Definition} except that the definition is turned
   into a local definition on objects depending on it after closing the
   current section.
@@ -140,38 +169,55 @@ This command applies in proof editing mode. It is equivalent to {\tt
 one gulp, as a proof term (see section \ref{exact}).
 
 \begin{Variants}
-\item{\tt Proof.}\\
-Is a noop which is useful to delimit the sequence of
-tactic commands which start a proof, after a {\tt Theorem} command.
-It is a good practice to use {\tt Proof.} as an opening parenthesis,
-closed in the script with a closing {\tt Qed.}
-\item{\tt Proof with {\tac}.}\\
-This command may be used to start a proof. It defines a default tactic to be used each time a tactic command is ended by ``\verb#...#''. In this case the tactic command typed by the user is equivalent to \emph{command};{\tac}.  
+
+\item{\tt Proof.}
+  
+  Is a noop which is useful to delimit the sequence of tactic commands
+  which start a proof, after a {\tt Theorem} command.  It is a good
+  practice to use {\tt Proof.} as an opening parenthesis, closed in
+  the script with a closing {\tt Qed.}
+
+\item{\tt Proof with {\tac}.}
+  
+  This command may be used to start a proof. It defines a default
+  tactic to be used each time a tactic command is ended by
+  ``\verb#...#''. In this case the tactic command typed by the user is
+  equivalent to \emph{command};{\tac}.
 
 \end{Variants}
 
-\subsection{\tt Abort.}\comindex{Abort}
+\subsection{\tt Abort.}
+\comindex{Abort}
+
 This command cancels the current proof development, switching back to
 the previous proof development, or to the \Coq\ toplevel if no other
 proof was edited.
 
 \begin{ErrMsgs}
-\item \errindex{No focused proof}\texttt{ (No proof-editing in progress)}
+\item \errindex{No focused proof (No proof-editing in progress)}
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Abort {\ident}.}\\
+
+\item {\tt Abort {\ident}.}
+
   Aborts the editing of the proof named {\ident}.
-\item {\tt Abort All.}\\
+
+\item {\tt Abort All.}
+
   Aborts all current goals, switching back to the \Coq\ toplevel.
+
 \end{Variants}
 
-\subsection{\tt Suspend.}\comindex{Suspend}
+\subsection{\tt Suspend.}
+\comindex{Suspend}
+
 This command applies in proof editing mode. It switches back to the
 \Coq\ toplevel, but without canceling the current proofs.
 
 \subsection{\tt Resume.}
 \comindex{Resume}\label{Resume}
+
 This commands switches back to the editing of the last edited proof.
 
 \begin{ErrMsgs}
@@ -179,9 +225,12 @@ This commands switches back to the editing of the last edited proof.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Resume {\ident}.}\\
+
+\item {\tt Resume {\ident}.}
+
   Restarts the editing of the proof named {\ident}. This can be used
   to navigate between currently edited proofs.
+
 \end{Variants}
 
 \begin{ErrMsgs}
@@ -190,7 +239,9 @@ This commands switches back to the editing of the last edited proof.
 
 \section{Navigation in the proof tree}
 
-\subsection{\tt Undo.}\comindex{Undo}
+\subsection{\tt Undo.}
+\comindex{Undo}
+
 This command cancels the effect of the last tactic command.  Thus, it
 backtracks one step.
 
@@ -200,17 +251,24 @@ backtracks one step.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Undo {\num}.}\\
+
+\item {\tt Undo {\num}.}
+
   Repeats {\tt Undo} {\num} times.
+
 \end{Variants}
 
-\subsection{\tt Set Undo {\num}.}\comindex{Set Undo}
+\subsection{\tt Set Undo {\num}.}
+\comindex{Set Undo}
+
 This command changes the maximum number of {\tt Undo}'s that will be
 possible when doing a proof. It only affects proofs started after
 this command, such that if you want to change the current undo limit
 inside a proof, you should first restart this proof.
 
-\subsection{\tt Unset Undo.}\comindex{Unset Undo}
+\subsection{\tt Unset Undo.}
+\comindex{Unset Undo}
+
 This command resets the default number of possible {\tt Undo} commands
 (which is currently 12).
 
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 886457466..21479ca4b 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -110,28 +110,40 @@ proved. Otherwise, it fails.
 \item  \errindex{No such assumption}
 \end{ErrMsgs}
 
-\subsection{\tt clear {\ident}}\tacindex{clear}\label{clear}
+\subsection{\tt clear {\ident}}
+\tacindex{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
 usable in the proof development.
 
 \begin{Variants}
-\item {\tt clear {\ident$_1$} {\ldots} {\ident$_n$}.}\\
-This is equivalent to {\tt clear {\ident$_1$}. {\ldots} clear {\ident$_n$}.}
 
-\item {\tt clearbody {\ident}.}\tacindex{clearbody}\\
-This tactic expects {\ident} to be a local definition then clears its
-body. Otherwise said, this tactic turns a definition into an assumption.
+\item {\tt clear {\ident$_1$} {\ldots} {\ident$_n$}.}
+  
+  This is equivalent to {\tt clear {\ident$_1$}. {\ldots} clear
+    {\ident$_n$}.}
+  
+\item {\tt clearbody {\ident}.}\tacindex{clearbody}
+  
+  This tactic expects {\ident} to be a local definition then clears
+  its body. Otherwise said, this tactic turns a definition into an
+  assumption.
+
 \end{Variants}
 
 \begin{ErrMsgs}
 \item \errindex{No such assumption}
-\item \errindex{{\ident} is used in the conclusion}
-\item \errindex{{\ident} is used in the hypothesis {\ident'}}
+\item \errindexbis{{\ident} is used in the conclusion}{is used in the
+    conclusion} 
+\item \errindexbis{{\ident} is used in the hypothesis {\ident'}}{is
+    used in the hypothesis} 
 \end{ErrMsgs}
 
 \subsection{\tt move {\ident$_1$} after {\ident$_2$}}
-\tacindex{Move}
+\tacindex{move}
+
 This moves the hypothesis named {\ident$_1$} in the local context
 after the hypothesis named {\ident$_2$}.
 
@@ -144,36 +156,44 @@ then all hypotheses between {\ident$_1$} and {\ident$_2$} which
 (possibly indirectly) occur in {\ident$_1$} are moved also.
 
 \begin{ErrMsgs}
+
 \item \errindex{No such assumption: {\ident$_i$}}
 
 \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}:
                    it occurs in {\ident$_2$}}
+
 \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}:
                    it depends on {\ident$_2$}}
+
 \end{ErrMsgs}
 
 \subsection{\tt rename {\ident$_1$} into {\ident$_2$}}
-\tacindex{Rename}
+\tacindex{rename}
+
 This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current
 context\footnote{but it does not rename the hypothesis in the
-proof-term...}
+  proof-term...}
 
 \begin{ErrMsgs}
+
 \item \errindex{No such assumption}
 
-\item \errindex{{\ident$_2$} is already used}
+\item \errindexbis{{\ident$_2$} is already used}{is already used}
+
 \end{ErrMsgs}
 
 \subsection{\tt intro}
 \tacindex{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
-``Lam''\index{Typing rules!Lam} rule given in section
-\ref{Typed-terms}\footnote{Actually, only the second subgoal will be
-generated since the other one can be automatically checked.}.  If the
-goal starts with a let binder then the tactic implements a mix of the
-``Let''\index{Typing rules!Let} and ``Conv''\index{Typing rules!Conv}.
+``Lam''\index{Typing rules!Lam} rule given in
+Section~\ref{Typed-terms}\footnote{Actually, only the second subgoal
+  will be generated since the other one can be automatically
+  checked.}.  If the goal starts with a let binder then the tactic
+implements a mix of the ``Let''\index{Typing rules!Let} and
+``Conv''\index{Typing rules!Conv}.
 
 If the current goal is a dependent product {\tt forall (x:T), U} (resp {\tt
 let x:=t in U}) then {\tt intro} puts {\tt x:T} (resp {\tt x:=t}) in the
@@ -199,7 +219,7 @@ the tactic {\tt intro} applies the tactic {\tt red} until the tactic
 
 \begin{ErrMsgs}
 \item \errindex{No product even after head-reduction}
-\item \errindex{\texttt{{\ident} is already used}}
+\item \errindexbis{{\ident} is already used}{is already used}
 \end{ErrMsgs}
 
 \begin{Variants}
@@ -241,7 +261,8 @@ the tactic {\tt intro} applies the tactic {\tt red} until the tactic
 \item {\tt intros until {\num}}  \tacindex{intros until}
   
   Repeats {\tt intro} until the {\num}-th non-dependent premise. For
-  instance, on the subgoal \verb+forall x y:nat, x=y -> forall z:nat,z=x->z=y+ the
+  instance, on the subgoal %
+  \verb+forall x y:nat, x=y -> forall z:nat,z=x->z=y+ the
   tactic \texttt{intros until 2} is equivalent to \texttt{intros x y H
     z H0} (assuming \texttt{x, y, H, z} and \texttt{H0} do not already
   occur in context).
@@ -400,17 +421,16 @@ should not be substituted.
   {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. One of the {\ident}'s
   may be the word {\tt Goal}.
 
-
 \item {\tt pose (  {\ident} {\tt :=} {\term} {\tt )}}
   
-This adds the local definition {\ident} := {\term} to the current
-context without performing any replacement in the goal or in the
-hypotheses.
+  This adds the local definition {\ident} := {\term} to the current
+  context without performing any replacement in the goal or in the
+  hypotheses.
 
 \item{\tt pose {\term}}
   
-This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but
-{\ident} is generated by {\Coq}.
+  This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but
+  {\ident} is generated by {\Coq}.
 
 \end{Variants}
 
@@ -432,6 +452,7 @@ in the list of subgoals remaining to prove.
 \end{ErrMsgs}
 
 \begin{Variants}
+
 \item{\tt assert {\form}}
   
   This behaves as {\tt assert (} {\ident} : {\form} {\tt )} but
@@ -570,7 +591,6 @@ This tactic applies to any goal. It implements the rule
 
 \subsection{Bindings list}
 \index{Binding list}\label{Binding-list}
-\index[tactic]{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$ :=
@@ -621,7 +641,6 @@ cases.  This tactic is a macro for the tactics sequence {\tt intros;
 
 \section{Conversion tactics}
 \index{Conversion tactics}
-\index[tactic]{Conversion tactics}
 \label{Conversion-tactics}
 
 This set of tactics implements different specialized usages of the
@@ -631,8 +650,8 @@ tactic \texttt{change}.
 %voir reduction__conv_x : histoires d'univers.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{{\tt cbv} \flag$_1$ \dots\ \flag$_n$, {\tt lazy} \flag$_1$
-\dots\ \flag$_n$ {\rm and} {\tt compute}}
+\subsection{{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$
+\dots\ \flag$_n$} and {\tt compute}}
 \tacindex{cbv}\tacindex{lazy}
 
 These parameterized reduction tactics apply to any goal and perform
@@ -673,7 +692,7 @@ strategy, the latter should be preferred for evaluating purely
 computational expressions (i.e. with few dead code).
 
 \begin{Variants}
-\item {\tt compute} \tacindex{Compute} 
+\item {\tt compute} \tacindex{compute} 
   
   This tactic is an alias for {\tt cbv beta delta evar iota zeta}.
 \end{Variants}
@@ -1590,15 +1609,18 @@ latter is first introduced in the local context using
 \end{ErrMsgs}
 
 \begin{Variants}
-\item \texttt{injection} \num\\
+\item \texttt{injection} \num{}
+
   This does the same thing as \texttt{intros until \num} then
 \texttt{injection \ident} where {\ident} is the identifier for the last
 introduced hypothesis.
-\item{\tt injection}\tacindex{injection} \\
-  If the current goal is of the form {\tt \verb=~={\term$_1$}={\term$_2$}}, 
-  the tactic computes the head normal form
-  of the goal and then behaves as the sequence: {\tt unfold not; intro
-    {\ident}; injection {\ident}}. \\
+
+\item{\tt injection}\tacindex{injection} 
+  
+  If the current goal is of the form {\tt
+    \verb=~={\term$_1$}={\term$_2$}}, the tactic computes the head
+  normal form of the goal and then behaves as the sequence: {\tt
+    unfold not; intro {\ident}; injection {\ident}}.
   
   \ErrMsg \errindex{goal does not satisfy the expected preconditions}
 \end{Variants}
@@ -1806,7 +1828,6 @@ Abort.
   ${\tt forall (}\vec{x}{\tt :}\vec{T}{\tt),} I~\vec{t}$ Sort \sort}
 \label{Derive-Inversion}
 \comindex{Derive Inversion}
-\index[tactic]{Derive Inversion@{\tt Derive Inversion}}
 
 This command generates an inversion principle for the
 \texttt{inversion \dots\ using} tactic.
@@ -1881,22 +1902,34 @@ By default, \texttt{auto} only uses the hypotheses of the current goal and the
 hints of the database named {\tt core}. 
 
 \begin{Variants}
-\item  {\tt auto \num}\\
-  Forces the search depth to be \num. The maximal search depth is 5 by default.
-\item {\tt auto with \ident$_1$ \dots\ \ident$_n$}\\
+
+\item  {\tt auto \num}
+
+  Forces the search depth to be \num. The maximal search depth is 5 by
+  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.
-\item {\tt auto with *}\\
+
+\item {\tt auto with *}
+
   Uses all existing hint databases, minus the special database
-  {\tt v62}. See section \ref{Hints-databases}
-\item {\tt trivial}\tacindex{trivial}\\
+  {\tt v62}. See Section~\ref{Hints-databases}
+
+\item {\tt trivial}\tacindex{trivial}
+
   This tactic is a restriction of {\tt auto} that is not recursive and 
   tries only hints which cost is 0. Typically it solves trivial
   equalities like $X=X$.
-\item \texttt{trivial with \ident$_1$ \dots\ \ident$_n$}\\
-\item \texttt{trivial with *}\\
+
+\item \texttt{trivial with \ident$_1$ \dots\ \ident$_n$}
+
+\item \texttt{trivial with *}
+
 \end{Variants}
 
 \Rem {\tt auto} either solves completely the goal or else leave it
@@ -2032,7 +2065,8 @@ incompatibilities.
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
-\subsection{{\tt firstorder}\tacindex{firstorder}}
+\subsection{{\tt firstorder}}
+\tacindex{firstorder}
 \label{firstorder}
 
 The tactic \texttt{firstorder} is an {\it experimental} extension of
@@ -2042,15 +2076,20 @@ It is not restricted to usual logical connectives but
 instead may reason about any first-order class inductive definition.
 
 \begin{Variants}
- \item {\tt firstorder {\tac}}\\
-   \tacindex{\tt firstorder {\tac}}
+ \item {\tt firstorder {\tac}}
+   \tacindex{firstorder {\tac}}
+
    Tries to solve the goal with {\tac} when no logical rule may apply.
- \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }\\
-   \tacindex{\tt firstorder with}
+
+ \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
+   \tacindex{firstorder with}
+
    Adds lemmata \ident$_1$ \dots\ \ident$_n$ to the proof-search
    environment.
- \item {\tt firstorder using \ident$_1$ \dots\ \ident$_n$ }\\
-   \tacindex{\tt firstorder using}
+
+ \item {\tt firstorder using \ident$_1$ \dots\ \ident$_n$ }
+   \tacindex{firstorder using}
+
    Adds lemmata in {\tt auto} hints bases \ident$_1$ \dots\ \ident$_n$
    to the proof-search environment.
 \end{Variants}
@@ -2059,13 +2098,14 @@ 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)}}\tacindex{jp {\em (Jprover)}}
+\subsection{{\tt jp} {\em (Jprover)}}
+\tacindex{jp}
 \label{jprover}
 
-The tactic \texttt{jp}, due to Huang Guan-Shieng, is an {\it
-  experimental} port of the {\em Jprover}\cite{SLKN01} semi-decision 
-procedure for first-order intuitionistic logic implemented in {\em
-  NuPRL}\cite{Kre02}. 
+The tactic \texttt{jp}, due to Huang Guan-Shieng, is an experimental
+port of the {\em Jprover}\cite{SLKN01} semi-decision procedure for
+first-order intuitionistic logic implemented in {\em
+  NuPRL}\cite{Kre02}.
 
 Search may optionnaly be bounded by a multiplicity parameter
 indicating how many (at most) copies of a formula may be used in 
@@ -2313,40 +2353,45 @@ Reset Initial.
 \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:\\
-
+tactic {\tt field}. You must provide this theory as follows:
+\begin{flushleft}
 {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
-Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-
-\noindent where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}}
-is a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt
-A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it Azero}} is a
-term of type {\tt A}, {\tt {\it Aopp}} is a term of type {\tt A->A}, {\tt {\it
-Aeq}} is a term of type {\tt A->bool}, {\tt {\it Ainv}} is a term of type {\tt
-A->A}, {\tt {\it Rth}} is a term of type {\tt (Ring\_Theory {\it A Aplus Amult
-Aone Azero Ainv Aeq})}, and {\tt {\it Tinvl}} is a term of type {\tt
-forall n:{\it A}, {\~{}}(n={\it Azero})->({\it Amult} ({\it Ainv} n) n)={\it Aone}}.
-To build a ring theory, refer to chapter~\ref{ring} for more details.
+Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}
+\end{flushleft}
+where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} is
+a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt
+  A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it
+    Azero}} is a term of type {\tt A}, {\tt {\it Aopp}} is a term of
+type {\tt A->A}, {\tt {\it Aeq}} is a term of type {\tt A->bool}, {\tt
+  {\it Ainv}} is a term of type {\tt A->A}, {\tt {\it Rth}} is a term
+of type {\tt (Ring\_Theory {\it A Aplus Amult Aone Azero Ainv Aeq})},
+and {\tt {\it Tinvl}} is a term of type {\tt forall n:{\it A},
+  {\~{}}(n={\it Azero})->({\it Amult} ({\it Ainv} n) n)={\it Aone}}.
+To build a ring theory, refer to Chapter~\ref{ring} for more details.
 
 This command adds also an entry in the ring theory table if this theory is not
 already declared. So, it is useless to keep, for a given type, the {\tt Add
 Ring} command if you declare a theory with {\tt Add Field}, except if you plan
-to use specific features of {\tt ring} (see chapter~\ref{ring}). However, the
+to use specific features of {\tt ring} (see Chapter~\ref{ring}). However, the
 module {\tt ring} is not loaded by {\tt Add Field} and you have to make a {\tt
 Require Import Ring} if you want to call the {\tt ring} tactic.
 
 \begin{Variants}
+
 \item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
 {\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-{\tt \phantom{Add Field }with minus:={\it Aminus}}\\
-Adds also the term {\it Aminus} which must be a constant expressed by means of
-{\it Aopp}.
+{\tt \phantom{Add Field }with minus:={\it Aminus}}
+
+Adds also the term {\it Aminus} which must be a constant expressed by
+means of {\it Aopp}.
 
 \item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
 {\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-{\tt \phantom{Add Field }with div:={\it Adiv}}\\
-Adds also the term {\it Adiv} which must be a constant expressed by means of
-{\it Ainv}.
+{\tt \phantom{Add Field }with div:={\it Adiv}}
+
+Adds also the term {\it Adiv} which must be a constant expressed by
+means of {\it Ainv}.
+
 \end{Variants}
 
 \SeeAlso file {\tt theories/Reals/Rbase.v} for an example of instantiation,\\
@@ -2359,9 +2404,9 @@ field}.
 \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 be loaded by 
-{\tt Require Import Fourier}.
+This tactic written by Lo{\"\i}c Pottier solves linear inequations on
+real numbers using Fourier's method~\cite{Fourier}. This tactic must
+be loaded by {\tt Require Import Fourier}.
 
 \Example
 \begin{coq_example*}
@@ -2442,6 +2487,7 @@ main subgoal excluded.
 
 \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}
@@ -2452,7 +2498,16 @@ 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:
 
-\comindex{Hint}
+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}
   \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$
 \end{quotation}
@@ -2460,8 +2515,9 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is:
 \noindent where {\sl hint\_definition} is one of the following expressions:
 
 \begin{itemize}
-\item \texttt{Resolve} {\term} \index[command]{Hint!Resolve}
-
+\item \texttt{Resolve} {\term} 
+  \comindex{Hint Resolve}
+  
   This command adds {\tt apply {\term}} to the hint list
   with the head symbol of the type of \term. The cost of that hint is
   the number of subgoals generated by {\tt apply {\term}}.
@@ -2483,27 +2539,31 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is:
 
     The head symbol of the type of {\term} is a bound variable such
     that this tactic cannot be associated to a constant.
+
   \item \term\ \errindex{cannot be used as a hint}
 
     The type of \term\ contains products over variables which do not
     appear in the conclusion. A typical example is a transitivity axiom.
     In that case the {\tt apply} tactic fails, and thus is useless.
+
   \end{ErrMsgs}
 
   \begin{Variants}
-    \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$}
 
-      Adds each \texttt{Resolve} {\term$_i$}.
+  \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$}
+
+    Adds each \texttt{Resolve} {\term$_i$}.
+
   \end{Variants}
 
-\item \texttt{Immediate {\term}} \index[command]{Hint!Immediate}\\
+\item \texttt{Immediate {\term}} 
+\comindex{Hint Immediate}
   
   This command adds {\tt apply {\term}; trivial} to the hint list
   associated with the head symbol of the type of \ident in the given
   database. This tactic will fail if all the subgoals generated by
-  {\tt apply {\term}} are 
-  not solved immediately by the {\tt trivial} tactic which only tries
-  tactics with cost $0$.
+  {\tt apply {\term}} are not solved immediately by the {\tt trivial}
+  tactic which only tries tactics with cost $0$.
   
   This command is useful for theorems such that the symmetry of equality
   or $n+1=m+1 \to n=m$ that we may like to introduce with a
@@ -2513,17 +2573,23 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is:
   so that it is not used by {\tt trivial} itself.
 
   \begin{ErrMsgs}
+
   \item \errindex{Bound head variable}
-  \item \term\ \errindex{cannot be used as a hint}
+
+  \item \term\ \errindex{cannot be used as a hint} 
+
   \end{ErrMsgs}
 
   \begin{Variants}
-    \item \texttt{Immediate} {\term$_1$} \dots {\term$_m$}
+
+    \item \texttt{Immediate} {\term$_1$} \dots {\term$_m$} 
 
       Adds each \texttt{Immediate} {\term$_i$}.
+
   \end{Variants}
 
-\item \texttt{Constructors} {\ident}\index[command]{Hint!Constructors}\\
+\item \texttt{Constructors} {\ident}
+\comindex{Hint Constructors}
   
   If {\ident} is an inductive type, this command adds all its
   constructors as hints of type \texttt{Resolve}. Then, when the
@@ -2531,26 +2597,39 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is:
   \texttt{auto} will try to apply each constructor.
 
   \begin{ErrMsgs}
+
     \item {\ident} \errindex{is not an inductive type}
+
     \item {\ident} \errindex{not declared}
+
   \end{ErrMsgs}
 
   \begin{Variants}
-    \item \texttt{Constructors} {\ident$_1$} \dots {\ident$_m$} \\
+
+    \item \texttt{Constructors} {\ident$_1$} \dots {\ident$_m$} 
+
       Adds each \texttt{Constructors} {\ident$_i$}.
+
   \end{Variants}
 
-\item \texttt{Unfold} {\qualid}\index[command]{Hint!unfold}\\
-  This adds the tactic {\tt unfold {\qualid}} to the hint list
-  that will only be used when the head constant of the goal is \ident.
-  Its cost is 4.
+\item \texttt{Unfold} {\qualid}
+\comindex{Hint Unfold}
+  
+  This adds the tactic {\tt unfold {\qualid}} to the hint list that
+  will only be used when the head constant of the goal is \ident.  Its
+  cost is 4.
 
   \begin{Variants}
-    \item \texttt{Unfold} {\ident$_1$} \dots {\ident$_m$} \\
+
+    \item \texttt{Unfold} {\ident$_1$} \dots {\ident$_m$} 
+
       Adds each \texttt{Unfold} {\ident$_i$}.
+
   \end{Variants}
 
-\item \texttt{Extern \num\ \pattern\ => }\textsl{tactic}\index[command]{Hint!Extern}\\
+\item \texttt{Extern \num\ \pattern\ => }\textsl{tactic}
+\comindex{Hint Extern}
+
   This hint type is to extend \texttt{auto} with tactics other than
   \texttt{apply} and \texttt{unfold}. For that, we must specify a
   cost, a pattern and a tactic to execute. Here is an example:
@@ -2590,18 +2669,21 @@ Abort.
 pattern-matching on hypotheses.
 
 \begin{Variants}
-\item \texttt{Hint} \textsl{hint\_definition} \\
+\item \texttt{Hint} \textsl{hint\_definition} 
+  
   No database name is given : the hint is registered in the {\tt core} 
     database. 
 
 \item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
-   \ident$_1$ \ldots\ \ident$_n$\\
+   \ident$_1$ \ldots\ \ident$_n$
+
   This is used to declare hints that must not be exported to the other
   modules that require and import the current module. Inside a
   section, the option {\tt Local} is useless since hints do not
   survive anyway to the closure of sections.
 
-\item\texttt{Hint Local} \textsl{hint\_definition} \\
+\item\texttt{Hint Local} \textsl{hint\_definition} 
+
   Idem for the {\tt core} database.
     
 \end{Variants}
@@ -2633,6 +2715,7 @@ library. There is no systematic relation between the directories of the
 library and the databases.
 
 \begin{description}
+
 \item[\tt core] This special database is automatically used by
   \texttt{auto}. It contains only basic lemmas about negation,
   conjunction, and so on from. Most of the hints in this database come 
@@ -2673,36 +2756,170 @@ development.
 \subsection{\tt Print Hint}
 \label{PrintHint}
 \comindex{Print Hint}
-\index[tactic]{Hint!\texttt{Print Hint}}
+%\index[tactic]{Hint!\texttt{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
 every moment.
 
 \begin{Variants}
-\item {\tt  Print Hint {\ident} }\\
+
+\item {\tt  Print Hint {\ident} }
+
  This command displays only tactics associated with \ident\ in the
  hints list. This is independent of the goal being edited, to this
  command will not fail if no goal is being edited.
 
-\item {\tt Print Hint *}\\
+\item {\tt Print Hint *}
+
   This command displays all declared hints. 
 
-\item {\tt  Print HintDb {\ident} }\\
+\item {\tt  Print HintDb {\ident} }
 \label{PrintHintDb}
 \comindex{Print HintDb}
+
  This command displays all hints from database \ident.
+
 \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}}
+
 Hints provided by the \texttt{Hint} commands are erased when closing a
 section. Conversely, all hints of a module \texttt{A} that are not
 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}}
 \label{Scheme}
 \comindex{Scheme}
@@ -2710,34 +2927,31 @@ e.g. \texttt{Require Import A.}).
 The {\tt Scheme} command is a high-level tool for generating
 automatically (possibly mutual) induction principles for given types
 and sorts.  Its syntax follows the schema:
-
-\noindent
+\begin{tabbing}
 {\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
   with\\
   \mbox{}\hspace{0.1cm} \dots\ \\
         with {\ident$_m$} := Induction for {\ident'$_m$} Sort
-        {\sort$_m$}}\\
-
+        {\sort$_m$}}
+\end{tabbing}
 \ident'$_1$ \dots\ \ident'$_m$ are different inductive type
-identifiers belonging to
-the same package of mutual inductive definitions. This command
-generates {\ident$_1$}\dots{} {\ident$_m$} to be mutually recursive
-definitions. Each term {\ident$_i$} proves a general principle 
-of mutual induction for objects in type {\term$_i$}. 
-
+identifiers belonging to the same package of mutual inductive
+definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$}
+to be mutually recursive definitions. Each term {\ident$_i$} proves a
+general principle of mutual induction for objects in type {\term$_i$}.
 
 \begin{Variants}
 \item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\
     with\\
     \mbox{}\hspace{0.1cm} \dots\ \\
     with {\ident$_m$} := Minimality for {\ident'$_m$} Sort
-    {\sort$_m$}}\\
+    {\sort$_m$}}
+
   Same as before but defines a non-dependent elimination principle more
   natural in case of inductively defined relations. 
 \end{Variants}
 
-\SeeAlso \ref{Scheme-examples}
-
+\SeeAlso Section~\ref{Scheme-examples}
 
 \section{Generation of induction principles with {\tt Functional Scheme}}
 \label{FunScheme}
@@ -2746,36 +2960,34 @@ of mutual induction for objects in type {\term$_i$}.
 The {\tt Functional Scheme} command is a high-level experimental
 tool for generating automatically induction principles
 corresponding to (possibly mutually recursive) functions.  Its
-syntax follows the schema:\bigskip
-
-\noindent
+syntax follows the schema:
+\begin{tabbing}
 {\tt Functional Scheme {\ident$_i$} := Induction for
-    \ident'$_i$ with \ident'$_1$ \dots\ \ident'$_m$.}\\
-  
-  \ident'$_1$ \dots\ \ident'$_m$ are the names of mutually
-  recursive functions (they must be in the same order as when
-  they were defined), \ident'$_i$ being one of them. This command
-  generates the induction principle \ident$_i$, following the
-  recursive structure and case analyses of the functions
-  \ident'$_1$ \dots\ \ident'$_m$, and having \ident'$_i$ as entry
-  point.
+    \ident'$_i$ with \ident'$_1$ \dots\ \ident'$_m$.}
+\end{tabbing}  
+\ident'$_1$ \dots\ \ident'$_m$ are the names of mutually recursive
+functions (they must be in the same order as when they were defined),
+\ident'$_i$ being one of them. This command generates the induction
+principle \ident$_i$, following the recursive structure and case
+analyses of the functions \ident'$_1$ \dots\ \ident'$_m$, and having
+\ident'$_i$ as entry point.
 
 \begin{Variants}
-\item {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$.}\\
+\item {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$.}
   
   This command is a shortcut for:
-  
+  \begin{tabbing} 
   {\tt Functional Scheme {\ident$_1$} := Induction for
     \ident'$_1$ with \ident'$_1$.}
+\end{tabbing}
 
-  This variant can be used for non mutually recursive functions only.
+This variant can be used for non mutually recursive functions only.
 \end{Variants}
 
-\SeeAlso \ref{FunScheme-examples}
+\SeeAlso Section~\ref{FunScheme-examples}
 
 
 \section{Simple tactic macros}
-\index[tactic]{tactic macros}
 \index{tactic macros}
 \comindex{Tactic Definition}
 \label{TacticDefinition}
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index 7a411e822..def17e717 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -807,7 +807,7 @@ is undecidable in general case, don't expect miracles from it!
 
 \SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml}
 
-\SeeAlso the tactic \texttt{ring} (chapter \ref{ring})
+\SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring})
 
 
 \section{Using the tactical language}
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 853189c6f..4d876f71e 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -79,13 +79,6 @@
 \nocite{*}
 \bibliographystyle{plain}
 \bibliography{biblio}
-%BEGIN LATEX
-\RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps}
-\RefManCutCommand{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps}
-\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-}
-\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM}
-\RefManCutClose
-%END LATEX
 
 \printindex
 
@@ -95,6 +88,17 @@
 
 \printindex[error]
 
+\listoffigures
+%\listoftables
+
+%BEGIN LATEX
+\RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps}
+\RefManCutCommand{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps}
+\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-}
+\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM}
+\RefManCutClose
+%END LATEX
+
 \end{document}
 
 
diff --git a/doc/Setoid.tex b/doc/Setoid.tex
index 68260e085..6d45411c3 100644
--- a/doc/Setoid.tex
+++ b/doc/Setoid.tex
@@ -1,18 +1,18 @@
-\achapter{The \texttt{Setoid\_replace} tactic}
+\achapter{The \texttt{setoid\_replace} tactic}
 \aauthor{Cl\'ement Renard}
-\label{Setoid_replace}
-\tacindex{Setoid\_replace}
+\label{setoid_replace}
+\tacindex{setoid\_replace}
 
-This chapter presents  the \texttt{Setoid\_replace} tactic.
+This chapter presents  the \texttt{setoid\_replace} tactic.
 
-\asection{Description of \texttt{Setoid\_replace}}
+\asection{Description of \texttt{setoid\_replace}}
 
 Working on user-defined structures in \Coq\ is not very easy if
 Leibniz equality does not denote the intended equality. For example
 using lists to denote finite sets drive to difficulties since two
 non convertible terms can denote the same set.
 
-We present here a \Coq\ module, {\tt Setoid\_replace}, which allow to
+We present here a \Coq\ module, {\tt setoid\_replace}, which allow to
 structure and automate some parts of the work. In particular, if
 everything has been registered a simple
 tactic can do replacement just as if the two terms were equal.
@@ -20,17 +20,11 @@ tactic can do replacement just as if the two terms were equal.
 \asection{Adding new setoid or morphisms}
 
 Under the toplevel
-load the \texttt{Setoid\_replace} files with the command:
+load the \texttt{setoid\_replace} files with the command:
 
-\begin{coq_eval}
+\begin{coq_example*}
   Require Setoid.
-\end{coq_eval}
-
-\begin{quotation}
-\begin{verbatim}
-Require Setoid.
-\end{verbatim}
-\end{quotation}
+\end{coq_example*}
 
 A setoid is just a type \verb+A+ and an equivalence relation on \verb+A+.
 
@@ -96,7 +90,7 @@ And when you load a compiled file, all the \texttt{Add Setoid}
 commands of this file that are not inside a section will be loaded.
 
 \Warning Only the setoid on \texttt{Prop} is loaded by default with the
-\texttt{Setoid\_replace} module. The equivalence relation used is
+\texttt{setoid\_replace} module. The equivalence relation used is
 \texttt{iff} {\it i.e.} the logical equivalence.
 
 \asection{Adding new morphisms}
@@ -129,28 +123,28 @@ The compatibility lemma genereted depends on the setoids already
 declared.
 
 \asection{The tactic itself}
-\tacindex{Setoid\_replace}
-\tacindex{Setoid\_rewrite}
+\tacindex{setoid\_replace}
+\tacindex{setoid\_rewrite}
 
 After having registered all the setoids and morphisms you need, you can
-use the tactic called \texttt{Setoid\_replace}. The syntax is
+use the tactic called \texttt{setoid\_replace}. The syntax is
 
 \begin{quotation}
-\texttt{Setoid\_replace} $ term_1$ with $term_2$
+\texttt{setoid\_replace} $ term_1$ with $term_2$
 \end{quotation}
 
 The effect is similar to the one of \texttt{Replace}.
 
-You also have a tactic called \texttt{Setoid\_rewrite} which is the
+You also have a tactic called \texttt{setoid\_rewrite} which is the
 equivalent of \texttt{Rewrite} for setoids. The syntax is 
 
 \begin{quotation}
-\texttt{Setoid\_rewrite} \term
+\texttt{setoid\_rewrite} \term
 \end{quotation}
 
 \begin{Variants}
- \item \texttt{Setoid\_rewrite ->} \term
- \item \texttt{Setoid\_rewrite <-} \term
+ \item \texttt{setoid\_rewrite ->} \term
+ \item \texttt{setoid\_rewrite <-} \term
 \end{Variants}
 
 The arrow tells the systems in which direction the rewriting has to be
diff --git a/doc/Translator.tex b/doc/Translator.tex
index 5ebee7fdf..423e22755 100644
--- a/doc/Translator.tex
+++ b/doc/Translator.tex
@@ -23,7 +23,8 @@
 
 \def\NT#1{\langle\textit{#1}\rangle}
 \def\NTL#1#2{\langle\textit{#1}\rangle_{#2}}
-\def\TERM#1{\textsf{\bf #1}}
+%\def\TERM#1{\textsf{\bf #1}}
+\def\TERM#1{\texttt{#1}}
 \newenvironment{transbox}
   {\begin{center}\tt\begin{tabular}{l|ll} \hfil\textrm{V7} & \hfil\textrm{V8} \\ \hline}
   {\end{tabular}\end{center}}
@@ -79,8 +80,8 @@ the eager user who wants to start with the new syntax quickly.
 
 The toplevel has an option {\tt -translate} which allows to
 interactively translate commands. This toplevel translator accepts a
-command, prints the translation on standard output (after a \verb+New
-syntax:+ balise), executes the command, and waits for another
+command, prints the translation on standard output (after a %
+\verb+New syntax:+ balise), executes the command, and waits for another
 command. The only requirements is that they should be syntactically
 correct, but they do not have to be well-typed.
 
@@ -103,6 +104,7 @@ syntax that changed and how they were translated. All the examples
 below can be tested by entering the V7 commands in the toplevel
 translator.
 
+
 %%
 
 \subsection{Changes in lexical conventions w.r.t. V7}
@@ -113,7 +115,7 @@ The lexical conventions changed: \TERM{_} is not a regular identifier
 anymore. It is used in terms as a placeholder for subterms to be inferred
 at type-checking, and in patterns as a non-binding variable.
 
-Furthermore, only letters (unicode letters), digits, single quotes and
+Furthermore, only letters (Unicode letters), digits, single quotes and
 _ are allowed after the first character.
 
 \subsubsection{Quoted string}
@@ -121,7 +123,7 @@ _ are allowed after the first character.
 Quoted strings are used typically to give a filename (which may not
 be a regular identifier). As before they are written between double
 quotes ("). Unlike for V7, there is no escape character: characters
-are written normaly but the double quote which is doubled.
+are written normally except the double quote which is doubled.
 
 \begin{transbox}
 \TRANS{"abcd$\backslash\backslash$efg"}{"abcd$\backslash$efg"}
@@ -171,7 +173,7 @@ to be used when notations of several scopes appear in the same
 expression.
 
 In examples below, scope changes are not needed if the appropriate scope
-has been opened. Scope nat_scope is opened in the initial state of Coq.
+has been opened. Scope \verb|nat_scope| is opened in the initial state of Coq.
 \begin{transbox}
 \TRANSCOM{`0+x=x+0`}{0+x=x+0}{\textrm{Z_scope}}
 \TRANSCOM{``0 + [if b then ``1`` else ``2``]``}{0 + if b then 1 else 2}{\textrm{R_scope}}
@@ -182,23 +184,21 @@ Below is a table that tells which notation is available in which
 scope. The relative precedences and associativity of operators is the
 same as in usual mathematics. See the reference manual for more
 details. However, it is important to remember that unlike V7, the type
-operators for product and sum are left associative, in order not to
+operators for product and sum are left-associative, in order not to
 clash with arithmetic operators.
 
 \begin{center}
 \begin{tabular}{l|l}
 scope & notations \\
 \hline
-nat_scope & $+ ~- ~* ~< ~\leq ~> ~\geq$ \\
-Z_scope & $+ ~- ~* ~/ ~\TERM{mod} ~< ~\leq ~> ~\geq ~?=$ \\
-R_scope & $+ ~- ~* ~/ ~< ~\leq ~> ~\geq$ \\
-type_scope & $* ~+$ \\
-bool_scope & $\TERM{\&\&} ~\TERM{$||$} ~\TERM{-}$ \\
-list_scope & $\TERM{::} ~\TERM{++}$
+nat_scope & \texttt{+ - * < <= > >=} \\
+Z_scope & \texttt{+ - * / mod < <= > >= ?=} \\
+R_scope & \texttt{+ - * / < <= > >=} \\
+type_scope & \texttt{* +} \\
+bool_scope & \texttt{\&\& || -} \\
+list_scope & \texttt{:: ++}
 \end{tabular}
 \end{center}
-(Note: $\leq$ stands for \TERM{$<=$})
-
 
 
 \subsubsection{Notation for implicit arguments}
@@ -206,7 +206,7 @@ list_scope & $\TERM{::} ~\TERM{++}$
 The explicitation of arguments is closer to the \emph{bindings}
 notation in tactics. Argument positions follow the argument names of
 the head constant. The example below assumes \verb+f+ is a function
-with 2 dependent arguments named \verb+x+ and \verb+y+, and a third
+with two dependent arguments named \verb+x+ and \verb+y+, and a third
 non-dependent argument.
 \begin{transbox}
 \TRANS{f 1!t1 2!t2 3!t3}{f (x:=t1) (y:=t2) (1:=t3)}
@@ -226,14 +226,14 @@ written {\tt _}
 \subsubsection{Universal quantification}
 
 The universal quantification and dependent product types are now
-materialized with the \TERM{forall} keyword before the binders and a
+introduced by the \texttt{forall} keyword before the binders and a
 comma after the binders.
 
 The syntax of binders also changed significantly. A binder can simply be
 a name when its type can be inferred. In other cases, the name and the type
 of the variable are put between parentheses. When several consecutive
 variables have the same type, they can be grouped. Finally, if all variables
-have the same type parentheses can be omitted.
+have the same type, parentheses can be omitted.
 
 \begin{transbox}
 \TRANS{(x:A)B}{forall (x:~A), B ~~\textrm{or}~~ forall x:~A, B}
@@ -246,8 +246,8 @@ have the same type parentheses can be omitted.
 \subsubsection{Abstraction}
 
 The notation for $\lambda$-abstraction follows that of universal
-quantification. The binders are surrounded by keyword \TERM{fun}
-and $\Rightarrow$ (\verb+=>+ in ascii).
+quantification. The binders are surrounded by keyword \texttt{fun}
+and \verb+=>+.
 
 \begin{transbox}
 \TRANS{[x,y:nat; z](f a b c)}{fun (x y:nat) z => f a b c}
@@ -301,7 +301,7 @@ dependent case analysis.
 
 \subsubsection{Fixpoints and cofixpoints}
 
-An easier syntax for non-mutual fixpoints is provided, making it very close
+An simpler syntax for non-mutual fixpoints is provided, making it very close
 to the usual notation for non-recursive functions. The decreasing argument
 is now indicated by an annotation between curly braces, regardless of the
 binders grouping. The annotation can be omitted if the binders introduce only
@@ -389,8 +389,8 @@ Ltac by default.
 
 \subsubsection{Occurrences}
 
-To avoid ambiguity between a numeric literal and the optionnal
-occurence numbers of this term, the occurence numbers are put after
+To avoid ambiguity between a numeric literal and the optional
+occurrence numbers of this term, the occurrence numbers are put after
 the term itself and after keyword \TERM{as}.
 \begin{transbox}
 \TRANS{Pattern 1 2 (f x) 3 4 d y z}{pattern f x at 1 2, d at 3 4, y, z}
@@ -605,7 +605,7 @@ try and make the translation.
 \subsubsection{The general case}
 
 The preferred way is to use script {\tt translate-v8} if your development
-is compiled by a Makfile with the following constraints:
+is compiled by a Makefile with the following constraints:
 \begin{itemize}
 \item compilation is achievd by invoke make without specifying a target
 \item options are passed to Coq with make variable COQFLAGS that
@@ -683,6 +683,8 @@ If the choices made by translation or in the following cases:
 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
@@ -693,20 +695,19 @@ to determine the context in which terms appearing in tactics
 live.}. If this happens, it is preferable to transform it manually
 before translation.
 
-
 \subsubsection{Syntax extensions with {\tt Grammar} and {\tt Syntax}}
 
 
 {\tt Grammar} and {\tt Syntax} are no longer supported. They
 should be replaced by an equivalent {\tt Notation} command and be
-processed as decribed above. Before attempting translation, users
+processed as described above. Before attempting translation, users
 should verify that compilation with option {\tt -v7} succeeds.
 
 In the cases where {\tt Grammar} and {\tt Syntax} cannot be emulated
 by {\tt Notation}, users have to change manually they development as
 they wish to avoid the use of {\tt Grammar}. If this is not done, the
 translator will simply expand the notations and the output of the
-translator will use the reuglar Coq syntax.
+translator will use the regular Coq syntax.
 
 \subsubsection{Syntax extensions with {\tt Notation} and {\tt Infix}}
 
@@ -891,5 +892,6 @@ 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 c10dca58e..277b62021 100644
--- a/doc/headers.tex
+++ b/doc/headers.tex
@@ -82,6 +82,7 @@ Vernacular Commands Index}
 \newcommand{\comindex}[1]{%
 \index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}}
 \newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}}
+\newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}}
 \newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}}
 \makeatother
 
diff --git a/doc/macros.tex b/doc/macros.tex
index 8084d8f94..71f223ad6 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -405,11 +405,10 @@
 
 % placement of figures
 
-\renewcommand{\topfraction}{.95}
-\renewcommand{\bottomfraction}{.95}
-\renewcommand{\textfraction}{.05}
-\renewcommand{\floatpagefraction}{.8}
-
+\renewcommand{\topfraction}{.99}
+\renewcommand{\bottomfraction}{.99}
+\renewcommand{\textfraction}{.01}
+\renewcommand{\floatpagefraction}{.9}
 
 % Macros Bruno pour description de la syntaxe