Merge commit 'upstream/8.1.gamma' into 8.1

13 files changed, 858 insertions, 458 deletions

diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 70889c9d..30dfa93d 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -1,10 +1,13 @@
 \achapter{The \texttt{ring} tactic}
-\aauthor{Patrick Loiseleur and Samuel Boutin}
+\aauthor{Bruno Barras, Benjamin Gr\'egoire and Assia
+  Mahboubi\footnote{based on previous work from
+  Patrick Loiseleur and Samuel Boutin}}
 \label{ring}
 \tacindex{ring}
 
 This chapter presents  the \texttt{ring} tactic.
 
+
 \asection{What does this tactic?}
 
 \texttt{ring} does associative-commutative rewriting in ring and semi-ring
@@ -14,20 +17,21 @@ $\otimes$, and two constants 0 and 1 that are unities for $\oplus$ and
 $\otimes$. A \textit{polynomial} is an expression built on variables $V_0, V_1,
 \dots$ and constants by application of $\oplus$ and $\otimes$.
 
-Let an {\it ordered product} be a product of variables $V_{i_1} \otimes
-\ldots \otimes V_{i_n}$ verifying $i_1 \le i_2 \le \dots \le i_n$. Let a
-\textit{monomial} be the product of a constant (possibly equal to 1, in
-which case we omit it) and an ordered product.  We can order the
-monomials by the lexicographic order on products of variables. Let a
-\textit{canonical sum} be an ordered sum of monomials that are all
-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
-normalizes polynomials over any ring or semi-ring structure. The basic
-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
+Let an {\it ordered product} be a product of variables $V_{i_1}
+\otimes \ldots \otimes V_{i_n}$ verifying $i_1 \le i_2 \le \dots \le
+i_n$. Let a \textit{monomial} be the product of a constant and an
+ordered product.  We can order the monomials by the lexicographic
+order on products of variables. Let a \textit{canonical sum} be an
+ordered sum of monomials that are all 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. In fact, the actual representation shares monomials
+with same prefixes. So what does \texttt{ring}? It normalizes
+polynomials over any ring or semi-ring structure. The basic 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.
 
 \begin{Examples}
@@ -55,7 +59,7 @@ expression in the \gallina\ language. For example in the ring
 \end{verbatim}
 \end{quotation}
 
-\noindent As a ring expression, is has 3 subterms. Give each subterm a
+\noindent As a ring expression, it has 3 subterms. Give each subterm a
 number in an arbitrary order:
 
 \begin{tabular}{ccl}
@@ -90,64 +94,339 @@ 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:
+The {\tt ring} tactic solves equations upon polynomial expressions of
+a ring (or semi-ring) structure. It proceeds by normalizing both hand
+sides of the equation (w.r.t. associativity, commutativity and
+distributivity, constant propagation) and comparing syntactically the
+results.
+
+{\tt ring\_simplify} applies the normalization procedure described
+above to the terms given. The tactic then replaces all occurrences of
+the terms given in the conclusion of the goal by their normal
+forms. If no term is given, then the conclusion should be an equation
+and both hand sides are normalized.
+
+The tactic must be loaded by \texttt{Require Import Ring}. The ring
+structures must be declared with the \texttt{Add Ring} command (see
+below). The ring of booleans is predefined; if one wants to use the
+tactic on \texttt{nat} one must first require the module
+\texttt{ArithRing}; for \texttt{Z}, do \texttt{Require Import
+ZArithRing}; for \texttt{N}, do \texttt{Require Import
+NArithRing}.
+
+\Example
+\begin{coq_eval}
+Reset Initial.
+Require Import ZArith.
+Open Scope Z_scope.
+\end{coq_eval}
+\begin{coq_example}
+Require Import ZArithRing.
+Goal forall a b c:Z,
+  (a + b + c) * (a + b + c) =
+  a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
+\end{coq_example}
+\begin{coq_example}
+intros; ring.
+\end{coq_example}
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
 
-\begin{quotation}
+\Warning \texttt{ring\_simplify $term_1$; ring\_simplify $term_2$} is
+not equivalent to \texttt{ring\_simplify $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. So the first alternative should be
+avoided for terms belonging to the same ring theory.
+
+\begin{ErrMsgs}
+\item \errindex{not a valid ring equation}
+  The conclusion of the goal is not provable in the corresponding ring
+  theory.
+\item \errindex{arguments of ring\_simplify do not have all the same type}
+  {\tt ring\_simplify} cannot simplify terms of several rings at the
+  same time. Invoke the tactic once per ring structure.
+\item \errindex{cannot find a declared ring structure over {\tt term}}
+  No ring has been declared for the type of the terms to be
+  simplified. Use {\tt Add Ring} first.
+\item \errindex{cannot find a declared ring structure for equality
+  {\tt term}}
+  Same as above is the case of the {\tt ring} tactic.
+\end{ErrMsgs}
+
+\asection{Adding a ring structure}
+
+Declaring a new ring consists in proving that a ring signature (a
+carrier set, an equality, and ring operations: {\tt
+Ring\_theory.ring\_theory} and {\tt Ring\_theory.semi\_ring\_theory})
+satisfies the ring axioms. Semi-rings (rings without $+$ inverse) are
+also supported. The equality can be either Leibniz equality, or any
+relation declared as a setoid (see~\ref{setoidtactics}). The definition
+of ring and semi-rings (see module {\tt Ring\_theory}) is:
 \begin{verbatim}
-Require Ring.
+ Record ring_theory : Prop := mk_rt {
+    Radd_0_l    : forall x, 0 + x == x;
+    Radd_sym    : forall x y, x + y == y + x;
+    Radd_assoc  : forall x y z, x + (y + z) == (x + y) + z;
+    Rmul_1_l    : forall x, 1 * x == x;
+    Rmul_sym    : forall x y, x * y == y * x;
+    Rmul_assoc  : forall x y z, x * (y * z) == (x * y) * z;
+    Rdistr_l    : forall x y z, (x + y) * z == (x * z) + (y * z);
+    Rsub_def    : forall x y, x - y == x + -y;
+    Ropp_def    : forall x, x + (- x) == 0
+ }.
+
+Record semi_ring_theory : Prop := mk_srt {
+    SRadd_0_l   : forall n, 0 + n == n;
+    SRadd_sym   : forall n m, n + m == m + n ;
+    SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p;
+    SRmul_1_l   : forall n, 1*n == n;
+    SRmul_0_l   : forall n, 0*n == 0; 
+    SRmul_sym   : forall n m, n*m == m*n;
+    SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p;
+    SRdistr_l   : forall n m p, (n + m)*p == n*p + m*p
+  }.
 \end{verbatim}
-\end{quotation}
 
-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.
+This implementation of {\tt ring} also features a notion of constant
+that can be parameterized. This can be used to improve the handling of
+closed expressions when operations are effective. It consists in
+introducing a type of \emph{coefficients} and an implementation of the
+ring operations, and a morphism from the coefficient type to the ring
+carrier type. The morphism needs not be injective, nor surjective.  As
+an example, one can consider the real numbers. The set of coefficients
+could be the rational numbers, upon which the ring operations can be
+implemented. The fact that there exists a morphism is defined by the
+following properties:
+\begin{verbatim}
+ Record ring_morph : Prop := mkmorph {
+    morph0    : [cO] == 0;
+    morph1    : [cI] == 1;
+    morph_add : forall x y, [x +! y] == [x]+[y];
+    morph_sub : forall x y, [x -! y] == [x]-[y];
+    morph_mul : forall x y, [x *! y] == [x]*[y];
+    morph_opp : forall x, [-!x] == -[x];
+    morph_eq  : forall x y, x?=!y = true -> [x] == [y] 
+  }.
+
+ Record semi_morph : Prop := mkRmorph {
+    Smorph0 : [cO] == 0;
+    Smorph1 : [cI] == 1;
+    Smorph_add : forall x y, [x +! y] == [x]+[y];
+    Smorph_mul : forall x y, [x *! y] == [x]*[y];
+    Smorph_eq  : forall x y, x?=!y = true -> [x] == [y] 
+  }.
+\end{verbatim}
+where {\tt c0} and {\tt cI} denote the 0 and 1 of the coefficient set,
+{\tt +!}, {\tt *!}, {\tt -!} are the implementations of the ring
+operations, {\tt ==} is the equality of the coefficients, {\tt ?+!} is
+an implementation of this equality, and {\tt [x]} is a notation for
+the image of {\tt x} by the ring morphism.
+
+Since {\tt Z} is an initial ring (and {\tt N} is an initial
+semi-ring), it can always be considered as a set of
+coefficients. There are basically three kinds of (semi-)rings:
+\begin{description}
+\item[abstract rings] to be used when operations are not
+  effective. The set of coefficients is {\tt Z} (or {\tt N} for
+  semi-rings).
+\item[computational rings] to be used when operations are
+  effective. The set of coefficients is the ring itself. The user only
+  has to provide an implementation for the equality.
+\item[customized ring] for other cases. The user has to provide the
+  coefficient set and the morphism.
+\end{description}
+
+The syntax for adding a new ring is {\tt Add Ring $name$ : $ring$
+($mod_1$,\dots,$mod_2$)}.  The name is not relevent. It is just used
+for error messages. $ring$ is a proof that the ring signature
+satisfies the (semi-)ring axioms. The optional list of modifiers is
+used to tailor the behaviour of the tactic. The following list
+describes their syntax and effects:
+\begin{description}
+\item[abstract] declares the ring as abstract. This is the default.
+\item[decidable \term] declares the ring as computational. \term{} is
+  the correctness proof of an equality test {\tt ?=!}. Its type should be of
+  the form {\tt forall x y, x?=!y = true $\rightarrow$ x == y}.
+\item[morphism \term] declares the ring as a customized one. \term{} is
+  a proof that there exists a morphism between a set of coefficient
+  and the ring carrier (see {\tt Ring\_theory.ring\_morph} and {\tt
+  Ring\_theory.semi\_morph}).
+\item[setoid \term$_1$ \term$_2$] forces the use of given
+  setoid. \term$_1$ is a proof that the equality is indeed a setoid
+  (see {\tt Setoid.Setoid\_Theory}), and \term$_2$ a proof that the
+  ring operations are morphisms (see {\tt Ring\_theory.ring\_eq\_ext} and
+  {\tt Ring\_theory.sring\_eq\_ext}). This modifier needs not be used if the
+  setoid and morphisms have been declared.
+\item[constants [\ltac]] specifies a tactic expression that, given a term,
+  returns either an object of the coefficient set that is mapped to
+  the expression via the morphism, or returns {\tt
+  Ring\_tac.NotConstant}. Abstract (semi-)rings need not define this.
+\item[preprocess [\ltac]]
+  specifies a tactic that is applied as a preliminary step for {\tt
+  ring} and {\tt ring\_simplify}. It can be used to transform a goal
+  so that it is better recognized. For instance, {\tt S n} can be
+  changed to {\tt plus 1 n}.
+\item[postprocess [\ltac]] specifies a tactic that is applied as a final step
+  for {\tt ring\_simplify}. For instance, it can be used to undo
+  modifications of the preprocessor.
+\end{description}
 
-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{ErrMsgs}
+\item \errindex{bad ring structure}
+  The proof of the ring structure provided is not of the expected type.
+\item \errindex{bad lemma for decidability of equality}
+  The equality function provided in the case of a computational ring
+  has not the expected type.
+\item \errindex{ring {\it operation} should be declared as a morphism}
+  A setoid associated to the carrier of the ring structure as been
+  found, but the ring operation should be declared as
+  morphism. See~\ref{setoidtactics}.
+\end{ErrMsgs}
 
-\begin{quotation}
-\texttt{ring} $term_1$ \dots{} $term_n$
-\end{quotation}
-\tacindex{ring}
+\asection{How does it work?}
 
-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
+The code of \texttt{ring} is a good example of tactic written using
+\textit{reflection}.  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.
 
-\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.
+The interested reader is strongly advised to have a look at the file
+\texttt{Ring\_polynom.v}. Here a type for polynomials is defined: 
 
-\begin{ErrMsgs}
-\item \errindex{All terms must have the same type}
-\item \errindex{Don't know what to do with this goal}
-\item \errindex{No Declared Ring Theory for \term.}
+\begin{small}
+\begin{flushleft}
+\begin{verbatim}
+Inductive PExpr : Type :=
+  | PEc : C -> PExpr
+  | PEX : positive -> PExpr
+  | PEadd : PExpr -> PExpr -> PExpr
+  | PEsub : PExpr -> PExpr -> PExpr
+  | PEmul : PExpr -> PExpr -> PExpr
+  | PEopp : PExpr -> PExpr.
+\end{verbatim}
+\end{flushleft}
+\end{small}
 
-  \texttt{Use Add [Semi] Ring to declare it}
+Polynomials in normal form are defined as:
+\begin{small}
+\begin{flushleft}
+\begin{verbatim}
+ Inductive Pol : Type :=
+  | Pc : C -> Pol 
+  | Pinj : positive -> Pol -> Pol                   
+  | PX : Pol -> positive -> Pol -> Pol.
+\end{verbatim}
+\end{flushleft}
+\end{small}
+where {\tt Pinj n P} denotes $P$ in which $V_i$ is replaced by
+$V_{i+n}$, and {\tt PX P n Q} denotes $P \otimes V_1^{n} \oplus Q'$,
+$Q'$ being $Q$ where $V_i$ is replaced by $V_{i+1}$. 
 
-  That happens when all terms have the same type \term, but there is
-  no declared ring theory for this set. See below.
-\end{ErrMsgs}
 
-\begin{Variants}
-\item \texttt{ring}
+Variables maps are represented by list of ring elements, and two
+interpretation functions, one that maps a variables map and a
+polynomial to an element of the concrete ring, and the second one that
+does the same for normal forms:
+\begin{small}
+\begin{flushleft}
+\begin{verbatim}
+Definition PEeval : list R -> PExpr -> R := [...].
+Definition Pphi_dev : list R -> Pol -> R := [...].
+\end{verbatim}
+\end{flushleft}
+\end{small}
+
+A function to normalize polynomials is defined, and the big theorem is
+its correctness w.r.t interpretation, that is:
+
+\begin{small}
+\begin{flushleft}
+\begin{verbatim}
+Definition norm : PExpr -> Pol := [...].
+Lemma Pphi_dev_ok :
+   forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.
+\end{verbatim}
+\end{flushleft}
+\end{small}
+
+So now, what is the scheme for a normalization proof? Let \texttt{p}
+be the polynomial expression that the user wants to normalize. First a
+little piece of ML code guesses the type of \texttt{p}, the ring
+theory \texttt{T} to use, an abstract polynomial \texttt{ap} and a
+variables map \texttt{v} such that \texttt{p} is
+$\beta\delta\iota$-equivalent to \verb|(PEeval v ap)|. Then we
+replace it by \verb|(Pphi_dev v (norm ap))|, using the
+main correctness theorem and we reduce it to a concrete expression
+\texttt{p'}, which is the concrete normal form of
+\texttt{p}. This is summarized in this diagram:
+\begin{center}
+\begin{tabular}{rcl}
+\texttt{p} & $\rightarrow_{\beta\delta\iota}$  
+   & \texttt{(PEeval v ap)} \\
+ & & $=_{\mathrm{(by\ the\ main\ correctness\ theorem)}}$ \\
+\texttt{p'} 
+   & $\leftarrow_{\beta\delta\iota}$ 
+   & \texttt{(Pphi\_dev v (norm ap))}
+\end{tabular}
+\end{center}
+The user do not see the right part of the diagram. 
+From outside, the tactic behaves like a
+$\beta\delta\iota$ simplification extended with AC rewriting rules.
+Basically, the proof is only the application of the main
+correctness theorem to well-chosen arguments.
+
+
+\asection{Legacy implementation}
 
-  That works if the current goal is an equality between two
-  polynomials. It will normalize both sides of the
-  equality, solve it if the normal forms are equal and in other cases
-  try to simplify the equality using \texttt{congr\_eqT} and \texttt{refl\_equal}
-  to reduce $x + y = x + z$ to $y = z$ and $x * z = x * y$ to $y = z$.
+\Warning This tactic is the {\tt ring} tactic of previous versions of
+\Coq{} and it should be considered as deprecated. It will probably be
+removed in future releases. It has been kept only for compatibility
+reasons and in order to help moving existing code to the newer
+implementation described above. For more details, please refer to the
+Coq Reference Manual, version 8.0.
 
-  \ErrMsg\errindex{This goal is not an equality}
+
+\subsection{\tt legacy ring \term$_1$ \dots\ \term$_n$
+\tacindex{legacy ring}
+\comindex{Add Legacy Ring}
+\comindex{Add Legacy Semi Ring}}
+
+This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
+associative commutative rewriting on every ring.  The tactic must be
+loaded by \texttt{Require Import LegacyRing}. The ring must be declared in
+the \texttt{Add Ring} command. The ring of booleans
+is predefined; if one wants to use the tactic on \texttt{nat} one must
+first require the module \texttt{LegacyArithRing}; for \texttt{Z}, do
+\texttt{Require Import LegacyZArithRing}; for \texttt{N}, do \texttt{Require
+Import LegacyNArithRing}.
+
+The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal
+conclusion. The tactic \texttt{ring} normalizes these terms
+w.r.t. associativity and commutativity and replace them by their
+normal form.
+
+\begin{Variants}
+\item \texttt{legacy ring} When the goal is an equality $t_1=t_2$, it
+  acts like \texttt{ring\_simplify} $t_1$ $t_2$ and then
+  solves the equality by reflexivity.
+
+\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite
+    S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a
+  proof that \texttt{forall (n:nat), S n = plus (S O) n}.
 
 \end{Variants}
 
-\asection{Add a ring structure}
+You can have a look at the files \texttt{LegacyRing.v},
+\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the
+\texttt{Add Ring} command.
+
+\subsection{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:
@@ -242,9 +521,9 @@ constructor.
 
 Finally to register a ring the syntax is:
 
-\comindex{Add Ring}
+\comindex{Add Legacy Ring}
 \begin{quotation}
-  \texttt{Add Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T}
+  \texttt{Add Legacy Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T}
   \texttt{[} \textit{c1 \dots cn} \texttt{].}
 \end{quotation}
 
@@ -267,8 +546,8 @@ and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)},
 \texttt{(S (S O))}, \ldots
 
 \begin{Variants}
-\item \texttt{Add Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T} 
-  \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Semi
+\item \texttt{Add Legacy Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T} 
+  \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Legacy Semi
     Ring}
   
   There are two differences with the \texttt{Add Ring} command: there
@@ -276,8 +555,8 @@ and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)},
   \texttt{(Semi\_Ring\_Theory }\textit{A Aplus Amult Aone Azero
     Aeq}\texttt{)}.
 
-\item \texttt{Add Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv 
-    Aeq T}\texttt{.}\comindex{Add Abstract Ring}
+\item \texttt{Add Legacy Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv 
+    Aeq T}\texttt{.}\comindex{Add Legacy Abstract Ring}
   
   This command should be used for when the operations of rings are not
   computable; for example the real numbers of
@@ -286,8 +565,8 @@ and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)},
   axioms. The argument \texttt{Aeq} is not used; a good choice for
   that function is \verb+[x:A]false+.
 
-\item \texttt{Add Abstract Semi Ring} \textit{A Aplus Amult Aone Azero
-    Aeq T}\texttt{.}\comindex{Add Abstract Semi Ring}
+\item \texttt{Add Legacy Abstract Semi Ring} \textit{A Aplus Amult Aone Azero
+    Aeq T}\texttt{.}\comindex{Add Legacy Abstract Semi Ring}
 
 \end{Variants}
 
@@ -318,90 +597,6 @@ booleans.
 load the module \texttt{ArithRing}, and for \texttt{Z},
 load the module \texttt{ZArithRing}.
 
-
-\asection{How does it work?}
-
-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: 
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Inductive Type polynomial := 
-  Pvar : idx -> polynomial
-| Pconst : A -> polynomial
-| Pplus : polynomial -> polynomial -> polynomial
-| Pmult : polynomial -> polynomial -> polynomial
-| Popp : polynomial -> polynomial.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-There is also a type to represent variables maps, and an
-interpretation function, that maps a variables map and a polynomial to an
-element of the concrete ring:
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Definition polynomial_simplify := [...]
-Definition interp : (varmap A) -> (polynomial A) -> A := [...]
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-A function to normalize polynomials is defined, and the big theorem is
-its correctness w.r.t interpretation, that is:
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Theorem polynomial_simplify_correct : forall (v:(varmap A))(p:polynomial)
-  (interp v (polynomial_simplify p))
-  =(interp v p).
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-(The actual code is slightly more complex: for efficiency,
-there is a special datatype to represent normalized polynomials,
-i.e. ``canonical sums''. But the idea is still the same).
-
-So now, what is the scheme for a normalization proof? Let \texttt{p}
-be the polynomial expression that the user wants to normalize. First a
-little piece of ML code guesses the type of \texttt{p}, the ring
-theory \texttt{T} to use, an abstract polynomial \texttt{ap} and a
-variables map \texttt{v} such that \texttt{p} is
-$\beta\delta\iota$-equivalent to \verb|(interp v ap)|. Then we
-replace it by \verb|(interp v (polynomial_simplify ap))|, using the
-main correctness theorem and we reduce it to a concrete expression
-\texttt{p'}, which is the concrete normal form of
-\texttt{p}. This is summarized in this diagram:
-\begin{center}
-\begin{tabular}{rcl}
-\texttt{p} & $\rightarrow_{\beta\delta\iota}$  
-   & \texttt{(interp v ap)} \\
- & & $=_{\mathrm{(by\ the\ main\ correctness\ theorem)}}$ \\
-\texttt{p'} 
-   & $\leftarrow_{\beta\delta\iota}$ 
-   & \texttt{(interp v (polynomial\_simplify ap))}
-\end{tabular}
-\end{center}
-The user do not see the right part of the diagram. 
-From outside, the tactic behaves like a
-$\beta\delta\iota$ simplification extended with AC rewriting rules.
-Basically, the proof is only the application of the main
-correctness theorem to well-chosen arguments.
-
 \asection{History of \texttt{ring}}
 
 First Samuel Boutin designed the tactic \texttt{ACDSimpl}. 
@@ -463,40 +658,26 @@ 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
-uses intensively the conversion
-rule of \CIC, that is replaces proof by computation the most as it is
+Is it the ultimate way to write tactics?  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
-generates huge proof terms. Symbolic Processing and Tautologies are
-in that case. But there are also tactics like \texttt{Auto} or
-\texttt{Linear}: that do many complex computations, using side-effects
-and backtracking, and generate
- a small proof term. Clearly, it would be a non-sense to
-replace them by tactics using reflection.
-
-Another argument against the reflection is that \Coq, as a
-programming language, has many nice features, like dependent types, 
-but is very far from the
-speed and the expressive power of \ocaml. Wait a minute! With \Coq\
-it is possible to extract ML code from \CIC\ terms, right? So, why not
-to link the extracted code with \Coq\ to inherit the benefits of the
-reflection and the speed of ML tactics? That is called \textit{total
-  reflection}, and is still an active research subject. With these
-technologies it will become possible to bootstrap the type-checker of
-\CIC, but there is still some work to achieve that goal.
-
-Another brilliant idea from Benjamin Werner: reflection could be used
-to couple a external tool (a rewriting program or a model checker)
-with \Coq. We define (in \Coq) a type of terms, a type of
-\emph{traces}, and prove a correction theorem that states that
-\emph{replaying traces} is safe w.r.t some interpretation. Then we let 
-the external tool do every computation (using side-effects,
-backtracking, exception, or others features that are not available in
-pure lambda calculus) to produce the trace: now we replay the trace in
-Coq{}, and apply the correction lemma. So internalization seems to be
-the best way to import \dots{} external proofs!
-
+generates huge proof terms. Symbolic Processing and Tautologies are in
+that case. But there are also tactics like \texttt{auto} or
+\texttt{linear} that do many complex computations, using side-effects
+and backtracking, and generate a small proof term. Clearly, it would
+be significantly less efficient to replace them by tactics using
+reflection.
+
+Another idea suggested by Benjamin Werner: reflection could be used to
+couple an external tool (a rewriting program or a model checker) with
+\Coq. We define (in \Coq) a type of terms, a type of \emph{traces},
+and prove a correction theorem that states that \emph{replaying
+traces} is safe w.r.t some interpretation. Then we let the external
+tool do every computation (using side-effects, backtracking,
+exception, or others features that are not available in pure lambda
+calculus) to produce the trace: now we can check in Coq{} that the
+trace has the expected semantic by applying the correction lemma.
  
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 48ce6bd9..4f8f1281 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -134,7 +134,7 @@ Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
 Here we have one obligation for each branch (branches for \verb:0: and \verb:(S 0): are
 automatically generated by the pattern-matching compilation algorithm):
 \begin{coq_example}
-  Show.
+  Obligations.
 \end{coq_example}
 
 \subsection{\tt Program Lemma {\ident} : type.
@@ -145,6 +145,18 @@ The \Russell\ language can also be used to type statements of logical
 properties. It will currently fail if the traduction to \Coq\
 generates obligations though it can be useful to insert automatic coercions.
 
+\subsection{Solving obligations}
+The following commands are available to manipulate obligations:
+
+\begin{itemize}
+\item {\tt Obligations [of \ident]} Displays all remaining
+  obligations.
+\item {\tt Solve Obligation num [of \ident]} Start the proof of
+  obligation {\tt num}.
+\item {\tt Solve Obligations [of \ident] using} {\tacexpr} Tries to solve
+  each obligation using the given tactic.
+\end{itemize}
+  
 
 % \subsection{\tt Program Fixpoint {\ident} {(\ident_$_0$ : \type_$_0$)
 %     \cdots (\ident_$_n$ : \type_$_n$)} {\tt \{wf}
@@ -507,7 +519,7 @@ generates obligations though it can be useful to insert automatic coercions.
 %  After compilation those two examples run nonetheless,
 %  thanks to the correction of the extraction~\cite{Let02}. 
 
-% $Id: Program.tex 8890 2006-06-01 21:33:26Z msozeau $ 
+% $Id: Program.tex 9332 2006-11-02 12:23:24Z msozeau $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 0a2f5904..8246e338 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -39,7 +39,8 @@ The remaining sections are concerned with the type-checking of terms.
 The beginner can skip them.
 
 The reader seeking a background on the Calculus of Inductive
-Constructions may read several papers.  Giménez~\cite{Gim98} provides
+Constructions may read several papers. Giménez and Castéran~\cite{GimCas05} 
+provide
 an introduction to inductive and coinductive definitions in Coq. In
 their book~\cite{CoqArt}, Bertot and Castéran give a precise
 description of the \CIC{} based on numerous practical examples.
@@ -117,7 +118,21 @@ indexes can be solved. From the user point of view we consequently
 have {\sf Type :Type}.
 
 We shall make precise in the typing rules the constraints between the
-indexes.
+indexes. 
+
+\paragraph{Implementation issues}
+In practice, the {\Type} hierarchy is implemented using algebraic
+universes. An algebraic universe $u$ is either a variable (a qualified
+identifier with a number) or a successor of an algebraic universe (an
+expression $u+1$), or an upper bound of algebraic universes (an
+expression $max(u_1,...,u_n)$), or the base universe (the expression
+$0$) which corresponds, in the arity of sort-polymorphic inductive
+types, to the predicative sort {\Set}. A graph of constraints between
+the universe variables is maintained globally. To ensure the existence
+of a mapping of the universes to the positive integers, the graph of
+constraints must remain acyclic.  Typing expressions that violate the
+acyclicity of the graph of constraints results in a \errindex{Universe
+inconsistency} error (see also section~\ref{PrintingUniverses}).
 
 \subsection{Constants}
 Besides the sorts, the language also contains constants denoting
@@ -1633,7 +1648,7 @@ using the {\tt Scheme} command described in section~\ref{Scheme}.
 The implementation contains also coinductive definitions, which are
 types inhabited by infinite objects. 
 More information on coinductive definitions can be found
-in~\cite{Gimenez95b,Gim98}.
+in~\cite{Gimenez95b,Gim98,GimCas05}.
 %They are described in chapter~\ref{Coinductives}.
 
 \section{\iCIC : the Calculus of Inductive Construction with
@@ -1684,7 +1699,7 @@ impredicative system for sort \Set{} become~:
      
 
 
-% $Id: RefMan-cic.tex 9001 2006-07-04 13:50:15Z herbelin $ 
+% $Id: RefMan-cic.tex 9306 2006-10-28 18:28:19Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 37660aa3..e0acef55 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -980,7 +980,7 @@ argument, use command
 Conversely, use command {\tt Unset Contextual Implicit} to
 unset the contextual implicit mode.
 
-\subsection{Explicit Applications
+\subsection{Explicit applications
 \index{Explicitation of implicit arguments}
 \label{Implicits-explicitation}
 \index{qualid@{\qualid}}}
@@ -1208,6 +1208,35 @@ printing features, use the command
 {\tt Unset Printing All.}
 \end{quote}
 
+\section{Printing universes}
+\label{PrintingUniverses}
+\comindex{Set Printing Universes}
+\comindex{Unset Printing Universes}
+
+The following command:
+\begin{quote}
+{\tt Set Printing Universes}
+\end{quote}
+activates the display of the actual level of each occurrence of
+{\Type}. See section~\ref{Sorts} for details.  This wizard option, in
+combination with \texttt{Set Printing All} (see
+section~\ref{SetPrintingAll}) can help to diagnose failures to unify
+terms apparently identical but internally different in the Calculus of
+Inductive Constructions. To reactivate the display of the actual level
+of the occurrences of {\Type}, use
+\begin{quote}
+{\tt Unset Printing Universes.}
+\end{quote}
+
+\comindex{Print Universes}
+
+The constraints on the internal level of the occurrences of {\Type}
+(see section~\ref{Sorts}) can be printed using the command
+\begin{quote}
+{\tt Print Universes.}
+\end{quote}
+
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index e7b825d7..1c258b20 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1362,7 +1362,7 @@ can be seen as a generalization of {\tt Fixpoint}.  It is actually a
 wrapper for several ways of defining a function \emph{and other useful
   related objects}, namely: an induction principle that reflects the
 recursive structure of the function (see \ref{FunInduction}), and its
-fixpoint equality (not always, see below).  The meaning of this
+fixpoint equality.  The meaning of this
 declaration is to define a function {\it ident}, similarly to {\tt
   Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be
 given (unless the function is not recursive), but it must not
@@ -1406,40 +1406,43 @@ Function plus (n m : nat) {struct n} : nat :=
 \paragraph{Limitations}
 \label{sec:Function-limitations}
 \term$_0$ must be build as a \emph{pure pattern-matching tree}
-(\texttt{match...with}) with $\lambda$-abstractions and applications only
-\emph{at the end} of each branch.  For now dependent cases are not
-treated.
+(\texttt{match...with}) with applications only \emph{at the end} of
+each branch.  For now dependent cases are not treated.
 
-\paragraph{Difference with \texttt{Functional Scheme}} 
-There is a difference between obtaining an induction scheme for a
-function by using \texttt{Function} (section~\ref{Function}) and
-by using \texttt{Functional Scheme} after a usual definition using
-\texttt{Fixpoint} or \texttt{Definition}. Indeed \texttt{Function}
-generally produces smaller principles, closer to the definition
-written by the user. This is because \texttt{Functional Scheme} works
-by analyzing the term \texttt{div2} after the compilation of pattern
-matching into exhaustive expanded ones, whereas \texttt{Function}
-analyzes the pseudo-term \emph{before} pattern matching expansion.
 
 
-\ErrMsg 
+\begin{ErrMsgs}
+\item \errindex{The recursive argument must be specified}
+\item \errindex{No argument name \ident}
+\item \errindex{Cannot use mutual definition with well-founded
+    recursion or measure}
 
-\errindex{while trying to define Inductive R\_\ident ...}
+\item \errindex{Cannot define graph for \ident\dots} (warning)
 
-The generation of the graph relation \texttt{(R\_\ident)} used to
-compute the induction scheme of \ident\ raised a typing error, the
-definition of \ident\ was aborted. You can use \texttt{Fixpoint}
-instead of \texttt{Function}, but the scheme will not be generated.
+  The generation of the graph relation \texttt{(R\_\ident)} used to
+  compute the induction scheme of \ident\ raised a typing error. Only
+  the ident is defined, the induction scheme will not be generated.
 
-This error happens generally when: 
+  This error happens generally when:
 
-\begin{itemize}
-\item the definition uses pattern matching on dependent types, which
-  \texttt{Function} cannot deal with yet.
-\item the definition is not a \emph{pattern-matching tree} as
-  explained above.
-\end{itemize}
+  \begin{itemize}
+  \item the definition uses pattern matching on dependent types, which
+    \texttt{Function} cannot deal with yet.
+  \item the definition is not a \emph{pattern-matching tree} as
+    explained above.
+  \end{itemize}
+
+\item \errindex{Cannot define principle(s) for \ident\dots} (warning)
+
+  The generation of the graph relation \texttt{(R\_\ident)} succeeded
+  but the induction principle could not be built. Only the ident is
+  defined. Please report.
+
+\item \errindex{Cannot built inversion information} (warning)
 
+  \texttt{functional inversion} will not be available for the
+  function.
+\end{ErrMsgs}
 
 
 \SeeAlso{\ref{FunScheme},\ref{FunScheme-examples},\ref{FunInduction}}
@@ -1453,20 +1456,27 @@ given below.
     : type$_0$ := \term$_0$}
 
   Defines the not recursive function \ident\ as if declared with
-  \texttt{Definition}.  Three elimination schemes {\tt\ident\_rect},
-  {\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the
-  documentation of {\tt Inductive} \ref{Inductive}), which reflect the
-  pattern matching structure of \term$_0$.
-
+  \texttt{Definition}.  Moreover the following are defined:
+
+  \begin{itemize}
+  \item {\tt\ident\_rect}, {\tt\ident\_rec} and {\tt\ident\_ind},
+    which reflect the pattern matching structure of \term$_0$ (see the
+    documentation of {\tt Inductive} \ref{Inductive});
+  \item The inductive \texttt{R\_\ident} corresponding to the graph of
+    \ident\ (silently);
+  \item \texttt{\ident\_complete} and \texttt{\ident\_correct} which are
+    inversion information linking the function and its graph.
+  \end{itemize}
 \item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
     {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$}
   
   Defines the structural recursive function \ident\ as if declared
-  with \texttt{Fixpoint}.  Three induction schemes {\tt\ident\_rect},
-  {\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the
-  documentation of {\tt Inductive} \ref{Inductive}), which reflect the
-  recursive structure of \term$_0$. When there is only one parameter,
-  {\tt \{struct} \ident$_0${\tt\}} can be omitted.
+  with \texttt{Fixpoint}.  Moreover the following are defined:
+
+  \begin{itemize}
+  \item The same objects as above;
+  \item The fixpoint equation of \ident: \texttt{\ident\_equation}.
+  \end{itemize}
   
 \item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt
       \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ :=
@@ -1502,18 +1512,22 @@ proof that the ordering relation is well founded.
 
 %Completer sur measure et wf
 
-The fixpoint equality  \texttt{\ident\_equation}, which is not trivial
-to prove in this case, is automatically generated and proved, together
-with three  induction schemes {\tt\ident\_rect},  {\tt\ident\_rec} and
-{\tt\ident\_ind} as explained above  (see  the   documentation  of  {\tt
-  Inductive} \ref{Inductive}), which  reflect the recursive structure
-of \term$_0$.
+Once proof obligations are discharged, the following objects are
+defined:
+
+\begin{itemize}
+\item The same objects as with the \texttt{struct};
+\item The lemma \texttt{\ident\_tcc} which collects all proof
+  obligations in one property;
+\item The lemmas \texttt{\ident\_terminate} and \texttt{\ident\_F}
+  which is needed to be inlined during extraction of \ident.
+\end{itemize}
 
 
 
 %Complete!!
 The way this recursive function is defined is the subject of several
-papers by Yves Bertot, Julien Forest, David Pichardie.
+papers by Yves Bertot and Antonia Balaa on one hand and  Gilles Barthe, Julien Forest, David Pichardie and Vlad Rusu on the other hand.
 
 %Exemples ok ici
 
@@ -1706,4 +1720,4 @@ To be able to unfold a proof, you should end the proof by {\tt Defined}
 % TeX-master: "Reference-Manual"
 % End: 
 
-% $Id: RefMan-gal.tex 9040 2006-07-11 18:06:49Z notin $ 
+% $Id: RefMan-gal.tex 9127 2006-09-07 15:47:14Z courtieu $ 
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index f9a5f975..f4cd9a6f 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -16,9 +16,9 @@ The \Coq\ library is structured into three parts:
   (see section~\ref{Require});
 
 \item[User contributions:] Other specification and proof developments
-  coming from the \Coq\ users' community. These libraries are no
-  longer distributed with the system.  They are available by anonymous
-  FTP (see section~\ref{Contributions}).
+  coming from the \Coq\ users' community. These libraries are
+  available for download at \texttt{http://coq.inria.fr} (see
+  section~\ref{Contributions}).
 \end{description}
 
 This chapter briefly reviews these libraries.
@@ -27,8 +27,8 @@ This chapter briefly reviews these libraries.
 \label{Prelude}
 
 This section lists the basic notions and results which are directly
-available in the standard \Coq\ system
-\footnote{Most of these constructions are defined in the
+available in the standard \Coq\ system\footnote{Most 
+of these constructions are defined in the
 {\tt Prelude} module in directory {\tt theories/Init} at the {\Coq}
 root directory; this includes the modules
 {\tt Notations},
@@ -155,6 +155,7 @@ Section Projections.
 Variables A B : Prop.
 Theorem proj1 : A /\ B -> A.
 Theorem proj2 : A /\ B -> B.
+End Projections.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
@@ -165,7 +166,6 @@ Abort All.
 \ttindex{iff}
 \ttindex{IF\_then\_else}
 \begin{coq_example*}
-End Projections.
 Inductive or (A B:Prop) : Prop :=
   | or_introl (_:A)
   | or_intror (_:B).
@@ -800,21 +800,24 @@ subdirectories:
 \begin{tabular}{lp{12cm}}
   {\bf Logic}   & Classical logic and dependent equality \\
   {\bf Arith}   & Basic Peano arithmetic \\
-  {\bf ZArith}  & Basic integer arithmetic \\
-  {\bf Bool}    &  Booleans (basic functions and results) \\
+  {\bf NArith}  & Basic positive integer arithmetic \\
+  {\bf ZArith}  & Basic relative integer arithmetic \\
+  {\bf Bool}    & Booleans (basic functions and results) \\
   {\bf Lists}   & Monomorphic and polymorphic lists (basic functions and
             results), Streams (infinite sequences defined with co-inductive
             types) \\
   {\bf Sets}    & Sets (classical, constructive, finite, infinite, power set,
             etc.) \\
-  {\bf IntMap}    & Representation of finite sets by an efficient
-  structure of map (trees indexed by binary integers).\\
- {\bf Reals}   & Axiomatization of Real Numbers (classical, basic functions, 
-                 integer part, fractional part, limit, derivative, Cauchy 
-                 series, power series and results,... Requires the 
-                 \textbf{ZArith} library).\\
+  {\bf FSets}   & Specification and implementations of finite sets and finite
+                  maps (by lists and by AVL trees)\\
+  {\bf IntMap}  & Representation of finite sets by an efficient
+                  structure of map (trees indexed by binary integers).\\
+ {\bf Reals}    & Axiomatization of real numbers (classical, basic functions, 
+                  integer part, fractional part, limit, derivative, Cauchy 
+                  series, power series and results,...)\\
  {\bf Relations} & Relations (definitions and basic results). \\
- {\bf Sorting} & Sorted list (basic definitions and heapsort correctness). \\
+ {\bf Sorting}  & Sorted list (basic definitions and heapsort correctness). \\
+ {\bf Strings}  & 8-bits characters and strings\\
  {\bf Wellfounded} & Well-founded relations (basic results). \\
 
 \end{tabular}
@@ -1094,7 +1097,7 @@ The users' contributions may also be obtained by anonymous FTP from site
 \verb:ftp.inria.fr:, in directory \verb:INRIA/coq/: and
 searchable on-line at \url{http://coq.inria.fr/contribs-eng.html}
 
-% $Id: RefMan-lib.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ 
+% $Id: RefMan-lib.tex 9312 2006-10-28 21:08:35Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index e7400232..ad2ffdc6 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -660,14 +660,17 @@ replaces the hole of the value of {\ident} by the value of
 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:
+The following expression returns an identifier:
 \begin{quote}
-{\tt fresh} {\qstring}
+{\tt fresh} \nelist{\textrm{\textsl{component}}}{}
 \end{quote}
-It evaluates to an identifier unbound in the goal, which is obtained
-by padding {\qstring} with a number if necessary. If no name is given,
-the prefix is {\tt H}.
+It evaluates to an identifier unbound in the goal. This fresh
+identifier is obtained by concatenating the value of the
+\textrm{\textsl{component}}'s (each of them is, either an {\ident} which
+has to refer to a name, or directly a name denoted by a
+{\qstring}). If the resulting name is already used, it is padded
+with a number so that it becomes fresh. If no component is
+given, the name is a fresh derivative of the name {\tt H}.
 
 \subsubsection{Computing in a constr}
 \index{Ltac!eval}
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 43216ed0..8b6e29b5 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -379,6 +379,9 @@ Mathematics (HELM cf \url{http://www.cs.unibo.it/helm}).
 A library for efficient representation of finite maps using binary trees
 contributed by Jean Goubault was integrated in the basic theories.
 
+Pierre Courtieu developed a command and a tactic to reason on the
+inductive structure of recursively defined functions.
+
 Jacek Chrz\k{a}szcz designed and implemented the module system of
 {\Coq} whose foundations are in Judicaël Courant's PhD thesis.
 
@@ -388,12 +391,12 @@ The development was coordinated by C. Paulin.
 
 Many discussions within the Démons team and the LogiCal project
 influenced significantly the design of {\Coq} especially with 
-%J. Chrz\k{a}szcz, 
-J. Courant, P. Courtieu, J. Duprat, J. Goubault, A. Miquel,
+%J. Chrz\k{a}szcz, P. Courtieu, 
+J. Courant, J. Duprat, J. Goubault, A. Miquel,
 C. Marché, B. Monate and B. Werner.
 
 Intensive users suggested improvements of the system : 
-Y. Bertot, L. Pottier, L. Théry , P. Zimmerman from INRIA, 
+Y. Bertot, L. Pottier, L. Théry, P. Zimmerman from INRIA, 
 C. Alvarado, P. Crégut, J.-F. Monin from France Telecom R \& D.
 \begin{flushright}
 Orsay, May. 2002\\
@@ -536,6 +539,9 @@ Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new
 more efficient and more general simplification algorithm on rings and
 semi-rings.
 
+Laurent Théry and Bruno Barras developed a new significantly more efficient
+simplification algorithm on fields.
+
 Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and
 Claudio Sacerdoti Coen added new tactic features.
 
@@ -564,9 +570,23 @@ Pierre Corbineau extended his tactic for solving first-order
 statements. He wrote a reflection-based intuitionistic tautology
 solver.
 
+Pierre Courtieu, Julien Forest and Yves Bertot added extra support to
+reason on the inductive structure of recursively defined functions.
+
 Jean-Marc Notin significantly contributed to the general maintenance
 of the system. He also took care of {\textsf{coqdoc}}.
 
+Pierre Castéran contributed to the documentation of (co-)inductive
+types and suggested improvements to the libraries.
+
+Pierre Corbineau implemented a declarative mathematical proof
+language, usable in combination with the tactic-based style of proof.
+
+Finally, many users suggested improvements of the system through the
+Coq-Club mailing list and bug-tracker systems, especially user groups
+from INRIA Rocquencourt, Radbout University, University of
+Pennsylvania and Yale University.
+
 \begin{flushright}
 Palaiseau, July 2006\\
 Hugo Herbelin
@@ -577,7 +597,7 @@ Hugo Herbelin
 % Integration of ZArith lemmas from Sophia and Nijmegen.
 
 
-% $Id: RefMan-pre.tex 9030 2006-07-07 15:37:23Z herbelin $ 
+% $Id: RefMan-pre.tex 9283 2006-10-26 08:13:51Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 8c1a7824..208a014a 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -374,7 +374,18 @@ All the hypotheses remains usable in the proof development.
 This command goes back to the default mode which is to print all
 available hypotheses.
 
-% $Id: RefMan-pro.tex 9030 2006-07-07 15:37:23Z herbelin $
+\section{$DPL$ : A Declarative proof language for Coq \emph{(experimental)} }
+
+An implementation of the $DPL$ declarative proof language by Pierre Corbineau at the Radboud University Nijmegen (The Netherlands) is included in Coq.
+
+ Due to the experimental nature and hence the potentially unstable semantics of the language, its documentation is not included here. However, it can be found at :
+
+\url{http://www.cs.ru.nl/~corbineau/mmode.html}
+
+
+
+
+% $Id: RefMan-pro.tex 9286 2006-10-26 17:43:00Z corbinea $
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 24699873..24ea78c0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -120,6 +120,7 @@ subgoal is proved. Otherwise, it fails.
 \end{ErrMsgs}
 
 \begin{Variants}
+\tacindex{eassumption}
   \item \texttt{eassumption}
 
     This tactic behaves like \texttt{assumption} but is able to handle
@@ -576,6 +577,45 @@ in the list of subgoals remaining to prove.
 %  \term\ will be kept.
 %\end{Variants}
 
+\subsection{{\tt apply {\term} in {\ident}}
+\tacindex{apply {\ldots} in}}
+
+This tactic applies to any goal.  The argument {\term} is a term
+well-formed in the local context and the argument {\ident} is an
+hypothesis of the context.  The tactic {\tt apply {\term} in {\ident}}
+tries to match the conclusion of the type of {\ident} against a non
+dependent premisses of the type of {\term}, trying them from right to
+left.  If it succeeds, the statement of hypothesis {\ident} is
+replaced by the conclusion of the type of {\ident}. The tactic also
+returns as many subgoals as the number of other non dependent premises
+in the type of {\term} and of the non dependent premises of the type
+of {\ident}.  The tactic {\tt apply} relies on first-order
+pattern-matching with dependent types.
+
+\begin{ErrMsgs}
+\item \errindex{Statement without assumptions}
+
+This happens if the type of {\term} has no non dependent premise.
+
+\item \errindex{Unable to apply}
+
+This happens if the conclusion of {\ident} does not match any of the
+non dependent premises of the type of {\term}.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt apply \nelist{\term}{,} in {\ident}}
+
+This applies each of {\term} in sequence in {\ident}.
+
+\item {\tt apply \nelist{{\term} {\bindinglist}}{,} in {\ident}}
+
+This does the same but uses the bindings in each {\bindinglist} to 
+instanciate the parameters of the corresponding type of {\term}
+(see syntax of bindings in Section~\ref{Binding-list}).
+
+\end{Variants}
+
 \subsection{\tt generalize \term
 \tacindex{generalize}
 \label{generalize}}
@@ -725,11 +765,12 @@ can be either the conclusion, or an hypothesis. In the case of a
 defined hypothesis it is possible to specify if the conversion should
 occur on the type part, the body part or both (default).
 
-\index{Clauses}
-Clauses are written after a conversion tactic (tactic
-\texttt{set}~\ref{tactic:set} also uses clauses) and are introduced by
-the keyword \texttt{in}. If no clause is provided, the default is to
-perform the conversion only in the conclusion.
+\index{Clauses} Clauses are written after a conversion tactic (tactics
+\texttt{set}~\ref{tactic:set},          \texttt{rewrite}~\ref{rewrite},
+\texttt{replace}~\ref{tactic:replace}                               and
+\texttt{autorewrite}~\ref{tactic:autorewrite}  also  use clauses)  and
+are introduced by  the keyword \texttt{in}. If no  clause is provided,
+the default is to perform the conversion only in the conclusion.
 
 The syntax and description of the various clauses follows:
 \begin{description}
@@ -754,7 +795,8 @@ performs the conversion in hypotheses $H_1\ldots H_n$.
 \dots\ \flag$_n$} and {\tt compute}
 \tacindex{cbv}
 \tacindex{lazy}
-\tacindex{compute}}
+\tacindex{compute}
+\tacindex{vm\_compute}}
 \label{vmcompute}
 
 These parameterized reduction tactics apply to any goal and perform
@@ -773,9 +815,7 @@ followed by {\tt [\qualid$_1$\ldots\qualid$_k$]} or {\tt
   -[\qualid$_1$\ldots\qualid$_k$]}), the {\tt delta} flag means that all constants must be unfolded.
 However, the {\tt delta} flag does not apply to variables bound by a
 let-in construction whose unfolding is controlled by the {\tt
-  zeta} flag only.  In addition, there is a flag {\tt Evar} to perform
-instantiation of existential variables (``?'') when an instantiation
-actually exists. 
+  zeta} flag only.
 
 The goal may be normalized with two strategies: {\em lazy} ({\tt lazy}
 tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy
@@ -798,7 +838,7 @@ computational expressions (i.e. with few dead code).
 \begin{Variants}
 \item {\tt compute} \tacindex{compute} 
   
-  This tactic is an alias for {\tt cbv beta delta evar iota zeta}.
+  This tactic is an alias for {\tt cbv beta delta iota zeta}.
 
 \item {\tt vm\_compute} \tacindex{vm\_compute}
 
@@ -1453,7 +1493,7 @@ Qed.
 \end{Variants}
 
 
-\subsection{\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$).
+\subsection{\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$).
 \tacindex{functional induction}
 \label{FunInduction}}
 
@@ -1461,8 +1501,7 @@ The \emph{experimental} tactic \texttt{functional induction} performs
 case analysis and induction following the definition of a function. It
 makes use of a principle generated by \texttt{Function}
 (section~\ref{Function}) or \texttt{Functional Scheme}
-(section~\ref{FunScheme}). This principle is named \ident\_ind by
-default but you can give it explicitly, see variants below.
+(section~\ref{FunScheme}).
 
 \begin{coq_eval}
 Reset Initial.
@@ -1478,22 +1517,22 @@ functional induction (minus n m); simpl; auto.
 Qed.
 \end{coq_example*}
 
-\Rem \texttt{(\ident\ \term$_1$ \dots\ \term$_n$)} must be a correct
-full application of \ident. In particular, the rules for implicit
-arguments are the same as usual. For example use \texttt{@\ident} if
+\Rem \texttt{(\qualid\ \term$_1$ \dots\ \term$_n$)} must be a correct
+full application of \qualid. In particular, the rules for implicit
+arguments are the same as usual. For example use \texttt{@\qualid} if
 you want to write implicit arguments explicitly.
 
-\Rem Parenthesis over \ident \dots \term$_n$ are not mandatory, but if
-there are not written then implicit arguments must be given.
+\Rem Parenthesis over \qualid \dots \term$_n$ are mandatory.
 
-\Rem \texttt{functional induction (f x1 x2 x3)} is actually a
-shorthand for \texttt{induction x1 x2 x3 (f x1 x2 x3) using f\_ind}.
-\texttt{f\_ind} being an induction scheme computed by the
-\texttt{Function} (section~\ref{Function}) or \texttt{Functional
-  Scheme} (section~\ref{FunScheme}) command . Therefore
-\texttt{functional induction} may fail if the induction scheme
-(\texttt{f\_ind}) is not defined. See also section~\ref{Function} for
-the function terms accepted by \texttt{Function}.
+\Rem \texttt{functional induction (f x1 x2 x3)} is actually a wrapper
+for \texttt{induction x1 x2 x3 (f x1 x2 x3) using \qualid} followed by
+a cleaning phase, where $\qualid$ is the induction principle
+registered for $f$ (by the \texttt{Function} (section~\ref{Function})
+or \texttt{Functional Scheme} (section~\ref{FunScheme}) command)
+corresponding to the sort of the goal.  Therefore \texttt{functional
+  induction} may fail if the induction scheme (\texttt{\qualid}) is
+not defined. See also section~\ref{Function} for the function terms
+accepted by \texttt{Function}.
 
 \Rem There is a difference between obtaining an induction scheme for a
 function by using \texttt{Function} (section~\ref{Function}) and by
@@ -1501,36 +1540,42 @@ using \texttt{Functional Scheme} after a normal definition using
 \texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
 details.
 
-\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples}}
+\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples},
+  \ref{sec:functional-inversion}}
 
-\ErrMsg 
-
-\errindex{The reference \ident\_ind was not found in the current
-environment}
+\begin{ErrMsgs}
+\item \errindex{Cannot find induction information on \qualid}
 
-~
+  ~
 
-\errindex{Not the right number of induction arguments}
- 
+\item \errindex{Not the right number of induction arguments}
+\end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
+\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$)
    using \term$_{m+1}$ with {\term$_{n+1}$} \dots {\term$_m$}}
 
  Similar to \texttt{Induction} and \texttt{elim}
  (section~\ref{Tac-induction}), allows to give explicitly the
  induction principle and the values of dependent premises of the
  elimination scheme, including \emph{predicates} for mutual induction
- when \ident is mutually recursive.
+ when \qualid is mutually recursive.
 
-\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
+\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$)
     using \term$_{m+1}$ with {\vref$_1$} := {\term$_{n+1}$} \dots\
     {\vref$_m$} := {\term$_n$}}
 
   Similar to \texttt{induction} and \texttt{elim}
   (section~\ref{Tac-induction}).
+
+\item All previous variants can be extended by the usual \texttt{as
+    \intropattern} construction, similarly for example to
+  \texttt{induction} and \texttt{elim} (section~\ref{Tac-induction}).
+    
 \end{Variants}
 
+
+
 \section{Equality}
 
 These tactics use the equality {\tt eq:forall A:Type, A->A->Prop}
@@ -1578,20 +1623,30 @@ This happens if \term$_1$ does not occur in the goal.
 \item {\tt rewrite {\term} in \textit{clause}}
   \tacindex{rewrite \dots\ in}\\
   Analogous to {\tt rewrite {\term}} but rewriting is done following
-  \textit{clause} (similarly to \ref{Conversion-tactics}). For instance:
-  \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H in H1;
-    rewrite H in H2; rewrite H} and \texttt{rewrite H in * |-} will do
-  \texttt{try rewrite H in H$_i$} for all hypothesis \texttt{H$_i$ <>
-    H}.
-
-\item {\tt rewrite -> {\term} in {\ident}}
+  \textit{clause} (similarly to \ref{Conversion-tactics}). For
+  instance:
+  \begin{itemize}
+  \item \texttt{rewrite H in H1} will rewrites \texttt{H} in the hypothesis
+    \texttt{H1} instead of the current goal.
+  \item \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H; rewrite H in H1;
+      rewrite H in H2}. In particular a failure will happen if any of
+    these three simplier tactics fails. 
+  \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
+      H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
+    as soon as at least one of these simplier tactics succeeds.
+  \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H} 
+    and \texttt{rewrite H in * |-} that succeeds if at
+    least one of these two tactics succeeds. 
+  \end{itemize}
+
+\item {\tt rewrite -> {\term} in \textit{clause}}
   \tacindex{rewrite -> \dots\ in}\\
-  Behaves as {\tt rewrite {\term} in {\ident}}.
+  Behaves as {\tt rewrite {\term} in \textit{clause}}.
  
-\item {\tt rewrite <- {\term} in {\ident}}\\
+\item {\tt rewrite <- {\term} in \textit{clause}}\\
   \tacindex{rewrite <- \dots\ in}
   Uses the equality \term$_1${\tt=}\term$_2$ from right to left to
-  rewrite in the hypothesis named {\ident}.
+  rewrite in \textit{clause} as explained above.
 \end{Variants}
 
 
@@ -1603,6 +1658,7 @@ This tactic acts like {\tt replace {\term$_1$} with {\term$_2$}}
 (see below).
 
 \subsection{\tt replace {\term$_1$} with {\term$_2$}
+\label{tactic:replace}
 \tacindex{replace \dots\ with}}
 
 This tactic applies to any goal. It replaces all free occurrences of
@@ -1618,21 +1674,23 @@ n}| assumption || symmetry; try assumption]}.
 \end{ErrMsgs}
 
 \begin{Variants}
-  
-\item {\tt replace {\term$_1$} with {\term$_2$} in \ident}\\
-  This replaces {\term$_1$} with {\term$_2$} in the hypothesis named
-  {\ident}, and generates the subgoal {\term$_2$}{\tt =}{\term$_1$}. 
-
-%   \begin{ErrMsgs}
-%   \item \errindex{No such hypothesis} : {\ident}
-%   \item \errindex{Nothing to rewrite in {\ident}}
-%   \end{ErrMsgs}
-
-\item {\tt replace {\term$_1$} with  {\term$_2$} by \tac}\\ This acts as
-  {\tt  replace {\term$_1$}  with {\term$_2$}}  but try  to  solve the
+\item {\tt replace {\term$_1$} with {\term$_2$} by \tac}\\ This acts
+  as {\tt replace {\term$_1$} with {\term$_2$}} but try to solve the
   generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
-\item {\tt replace {\term$_1$} with {\term$_2$} in \ident by \tac}\\
-  This acts as {\tt replace {\term$_1$} with {\term$_2$} in \ident} but try to solve the generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
+\item {\tt replace {\term}}\\ Replace {\term} with {\term'} using the
+  first assumption which type has the form {\tt \term=\term'} or {\tt
+    \term'=\term}
+\item {\tt replace -> {\term}}\\ Replace {\term} with {\term'} using the
+  first assumption which type has the form {\tt \term=\term'}
+\item {\tt replace <- {\term}}\\ Replace {\term} with {\term'} using the
+  first assumption which type has the form {\tt \term'=\term}
+\item {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} }\\
+    {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} by \tac }\\ 
+    {\tt replace {\term} \textit{clause}}\\ 
+    {\tt replace -> {\term} \textit{clause}}\\ 
+    {\tt replace -> {\term} \textit{clause}}\\ 
+    Act as before but the replacements take place in \textit{clause}~\ref{Conversion-tactics} an not only in the conclusion of the goal.\\
+    The  \textit{clause} arg must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
 \end{Variants}
 
 \subsection{\tt reflexivity
@@ -1709,7 +1767,7 @@ accepted as regular setoids for {\tt rewrite} and {\tt
 \tacindex{stepr}
 \comindex{Declare Right Step}
 \begin{Variants}
-\item{\tt stepl {\term} by {\tac}}\\
+\item{\tt stepl {\term}{\sl n} by {\tac}}\\
 This applies {\tt stepl {\term}} then applies {\tac} to the second goal.
 
 \item{\tt stepr {\term}}\\
@@ -1884,6 +1942,14 @@ introduced hypothesis.
   {\ident}}.
   
   \ErrMsg \errindex{goal does not satisfy the expected preconditions}
+
+\item \texttt{injection} \ident{} \texttt{as} \nelist{\intropattern}{}\\
+\texttt{injection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\texttt{injection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\tacindex{injection \ldots{} as}
+ 
+These variants apply \texttt{intros} \nelist{\intropattern}{} after the call to \texttt{injection}.
+
 \end{Variants}
 
 \subsection{\tt simplify\_eq {\ident}
@@ -2165,6 +2231,42 @@ the instance with the tactic {\tt inversion}.
 
 \SeeAlso \ref{inversion-examples} for examples
 
+
+
+\subsection{\tt functional inversion \ident}
+\label{sec:functional-inversion}
+
+\texttt{functional inversion} is a \emph{highly} experimental tactic
+which performs inversion on hypothesis \ident\ of the form
+\texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ =
+  \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been
+defined using \texttt{Function} (section~\ref{Function}).
+
+\begin{ErrMsgs}
+\item \errindex{Hypothesis \ident must contain at least one Function}
+\item \errindex{Cannot find inversion information for hypothesis \ident}
+  This error may be raised when  some inversion lemma failed to be
+  generated by Function.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt functional inversion \num}
+
+  This does the same thing as \texttt{intros until \num} then
+  \texttt{functional inversion \ident} where {\ident} is the
+  identifier for the last introduced hypothesis.
+\item {\tt functional inversion \ident\ \qualid}\\
+  {\tt functional inversion \num\ \qualid}
+
+  In case the hypothesis \ident (or \num) has a type of the form
+  \texttt{\qualid$_1$\ \term$_1$\dots\term$_n$\ =\qualid$_2$\
+    \term$_{n+1}$\dots\term$_{n+m}$} where \qualid$_1$ and \qualid$_2$
+  are valid candidates to functional inversion, this variant allows to
+  chose which must be inverted.
+\end{Variants}
+
+
+
 \subsection{\tt quote \ident
 \tacindex{quote}
 \index{2-level approach}}
@@ -2557,6 +2659,8 @@ If the goal is a non-quantified equality, {\tt congruence} tries to
 prove it with non-quantified equalities in the context. Otherwise it
 tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that an hypothesis is equal to the goal or to the negation of another hypothesis.
 
+{\tt congruence} is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the memebers of the equality must contain all the quantified variables in order for {\tt congruence} to match against it. 
+
 \begin{coq_eval}
 Reset Initial.
 Variable A:Set.
@@ -2586,6 +2690,12 @@ congruence.
 \end{coq_example}
 
 \begin{Variants}
+ \item {\tt congruence {\sl n}}\\
+  Tries to add at most {\tt \sl n} instances of hypotheses satting quantifiesd equalities to the problem in order to solve it. A bigger value of {\tt \sl n} does not make success slower, only failure. You might consider adding some lemmata as hypotheses using {\tt assert} in order for congruence to use them.
+
+\end{Variants}
+
+\begin{Variants}
 \item {\tt congruence with \term$_1$ \dots\ \term$_n$}\\
   Adds {\tt \term$_1$ \dots\ \term$_n$} to the pool of terms used by
   {\tt congruence}. This helps in case you have partially applied
@@ -2623,70 +2733,29 @@ integers. This tactic must be loaded by the command \texttt{Require Import
   Omega}. See the additional documentation about \texttt{omega}
 (chapter~\ref{OmegaChapter}).
 
-\subsection{\tt ring \term$_1$ \dots\ \term$_n$
+\subsection{{\tt ring} and {\tt ring\_simplify \term$_1$ \dots\ \term$_n$}
 \tacindex{ring}
-\comindex{Add Ring}
-\comindex{Add Semi Ring}}
-
-This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
-associative commutative rewriting on every ring.  The tactic must be
-loaded by \texttt{Require Import Ring}. The ring must be declared in
-the \texttt{Add Ring} command (see \ref{ring}). The ring of booleans
-is predefined; if one wants to use the tactic on \texttt{nat} one must
-first require the module \texttt{ArithRing}; for \texttt{Z}, do
-\texttt{Require Import ZArithRing}; for \texttt{N}, do \texttt{Require
-Import NArithRing}.
-
-The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal
-conclusion. The tactic \texttt{ring} normalizes these terms
-w.r.t. associativity and commutativity and replace them by their
-normal form.
+\tacindex{ring\_simplify}
+\comindex{Add Ring}}
 
-\begin{Variants}
-\item \texttt{ring} When the goal is an equality $t_1=t_2$, it
-  acts like \texttt{ring} $t_1$ $t_2$ and then simplifies or solves
-  the equality.
+The {\tt ring} tactic solves equations upon polynomial expressions of
+a ring (or semi-ring) structure. It proceeds by normalizing both hand
+sides of the equation (w.r.t. associativity, commutativity and
+distributivity, constant propagation) and comparing syntactically the
+results.
 
-\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite
-    S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a
-  proof that \texttt{forall (n:nat), S n = plus (S O) n}.
+{\tt ring\_simplify} applies the normalization procedure described
+above to the terms given. The tactic then replaces all occurrences of
+the terms given in the conclusion of the goal by their normal
+forms. If no term is given, then the conclusion should be an equation
+and both hand sides are normalized.
 
-\end{Variants}
-
-\Example
-\begin{coq_eval}
-Reset Initial.
-Require Import ZArith.
-Open Scope Z_scope.
-\end{coq_eval}
-\begin{coq_example}
-Require Import ZArithRing.
-Goal forall a b c:Z,
-  (a + b + c) * (a + b + c) =
-  a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
-\end{coq_example}
-\begin{coq_example}
-intros; ring.
-\end{coq_example}
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-You can have a look at the files \texttt{Ring.v},
-\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the
-\texttt{Add Ring} command.
-
-\SeeAlso Chapter~\ref{ring} for more detailed explanations about this tactic.
+See chapter~\ref{ring} for more information on the tactic and how to
+declare new ring structures.
 
 \subsection{\tt field
-\tacindex{field}}
-
-This tactic written by David~Delahaye and Micaela~Mayero solves equalities
-using commutative field theory. Denominators have to be non equal to zero and,
-as this is not decidable in general, this tactic may generate side conditions
-requiring some expressions to be non equal to zero. This tactic must be loaded
-by {\tt Require Import Field}. Field theories are declared (as for {\tt ring}) with
-the {\tt Add Field} command.
+\tacindex{field}
+\comindex{Add Field}}
 
 \Example
 \begin{coq_example*}
@@ -2705,13 +2774,28 @@ intros; field.
 Reset Initial.
 \end{coq_eval}
 
-\subsection{\tt Add Field
-\comindex{Add Field}}
+\SeeAlso file {\tt theories/Reals/Rbase.v} for an example of instantiation,\\
+\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt
+field}.
+
+\subsection{\tt legacy field
+\tacindex{legacy field}}
+
+This tactic written by David~Delahaye and Micaela~Mayero solves equalities
+using commutative field theory. Denominators have to be non equal to zero and,
+as this is not decidable in general, this tactic may generate side conditions
+requiring some expressions to be non equal to zero. This tactic must be loaded
+by {\tt Require Import LegacyField}. Field theories are declared (as for
+{\tt legacy ring}) with
+the {\tt Add Legacy Field} command.
+
+\subsection{\tt Add Legacy Field
+\comindex{Add Legacy Field}}
 
 This vernacular command adds a commutative field theory to the database for the
 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
+{\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
 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
@@ -2734,28 +2818,24 @@ 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}
+\item {\tt Add Legacy 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}.
 
-\item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
+\item {\tt Add Legacy 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}}
+{\tt \phantom{Add Legacy 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,\\
-\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt
-field}.
-
 \SeeAlso \cite{DelMay01} for more details regarding the implementation of {\tt
-field}.
+legacy field}.
 
 \subsection{\tt fourier
 \tacindex{fourier}}
@@ -2780,6 +2860,7 @@ Reset Initial.
 \end{coq_eval}
 
 \subsection{\tt autorewrite with \ident$_1$ \dots \ident$_n$.
+\label{tactic:autorewrite}
 \tacindex{autorewrite}}
 
 This tactic \footnote{The behavior of this tactic has much changed compared to
@@ -2806,9 +2887,17 @@ command.
 Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$
 $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
 
-\item \texttt{autorewrite with {\ident} in {\qualid}}
+\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}}
 
   Performs all the rewritings in hypothesis {\qualid}.
+\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}}
+
+  Performs all  the rewritings  in hypothesis {\qualid}  applying {\tt
+    \tac} to the main subgoal after each rewriting step.
+
+\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in \textit{clause}}
+  Performs all  the rewritings  in the clause \textit{clause}. \\
+  The  \textit{clause} arg must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
 
 \end{Variant}
 
@@ -3243,27 +3332,25 @@ tool for generating automatically induction principles
 corresponding to (possibly mutually recursive) functions.  Its
 syntax follows the schema:
 \begin{tabbing}
-{\tt Functional Scheme {\ident$_i$} := Induction for
-    \ident'$_i$ with \ident'$_1$ \dots\ \ident'$_m$.}
+{\tt Functional 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$}}
 \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.
+\ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
+names (they must be in the same order as when they were defined).
+This command generates the induction principles
+\ident$_1$\dots\ident$_m$, following the recursive structure and case
+analyses of the functions \ident'$_1$ \dots\ \ident'$_m$.
 
-\begin{Variants}
-\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.
-\end{Variants}
+\paragraph{\texttt{Functional Scheme}} 
+There is a difference between obtaining an induction scheme by using
+\texttt{Functional Scheme} on a function defined by \texttt{Function}
+or not. Indeed \texttt{Function} generally produces smaller
+principles, closer to the definition written by the user.
+
 
 \SeeAlso Section~\ref{FunScheme-examples}
 
@@ -3292,7 +3379,7 @@ The chapter~\ref{TacticLanguage} gives examples of more complex
 user-defined tactics.
 
 
-% $Id: RefMan-tac.tex 9044 2006-07-12 13:22:17Z herbelin $ 
+% $Id: RefMan-tac.tex 9283 2006-10-26 08:13:51Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 57155d21..0aee4317 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -373,10 +373,11 @@ with forest : Set :=
 \end{coq_example*}
 
 We define the function \texttt{tree\_size} that computes the size
-of a tree or a forest.
+of a tree or a forest. Note that we use \texttt{Function} which
+generally produces better principles.
 
 \begin{coq_example*}                
-Fixpoint tree_size (t:tree) : nat :=
+Function tree_size (t:tree) : nat :=
   match t with
   | node A f => S (forest_size f)
   end
@@ -387,23 +388,31 @@ Fixpoint tree_size (t:tree) : nat :=
   end.
 \end{coq_example*}
 
-The definition of principle of mutual induction following the
-recursive structure of \texttt{tree\_size} is defined by the
-command:
+Remark: \texttt{Function} generates itself non mutual induction
+principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}:
+
+\begin{coq_example}
+Check tree_size_ind.
+\end{coq_example}
+
+The definition of mutual induction principles following the recursive
+structure of \texttt{tree\_size} and \texttt{forest\_size} is defined
+by the command:
 
 \begin{coq_example*}
-Functional Scheme tree_size_ind := Induction for tree_size Sort Prop
-with forest_size_ind := Induction for forest_size Sort Prop.
+Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
+with forest_size_ind2 := Induction for forest_size Sort Prop.
 \end{coq_example*}
 
-You may now look at the type of {\tt tree\_size\_ind}:
+You may now look at the type of {\tt tree\_size\_ind2}:
 
 \begin{coq_example}
-Check tree_size_ind.
+Check tree_size_ind2.
 \end{coq_example}
 
 
 
+
 \section{{\tt inversion}}
 \tacindex{inversion}
 \label{inversion-examples}
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 10cd5b3e..030400e5 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -493,12 +493,14 @@ unprefixed form.
   ~\zeroone{\texttt{using relation} \textit{term}}\\
   ~\zeroone{\texttt{generate side conditions}
   \textit{term}$_1$ \ldots \textit{term}$_n$}\\
+  ~\zeroone{\texttt{by} \textit{tactic}}
 \end{verse}
 
-The \texttt{generate side conditions} and \texttt{using relation} arguments cannot be
-passed to the unprefixed form. The latter argument tells the tactic what
-parametric relation should be used to replace the first tactic argument
-with the second one. If omitted, it defaults to Leibniz equality.
+The  \texttt{generate  side  conditions} and  \texttt{using  relation}
+arguments cannot be passed to the unprefixed form. The latter argument
+tells the  tactic what parametric  relation should be used  to replace
+the first tactic argument with the second one. If omitted, it defaults
+to Leibniz equality.
 
 Every derived tactic that is based on the unprefixed forms of the tactics
 considered above will also work up to user defined relations. For instance,
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index b9a3a2c5..d16c82c5 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -100,26 +100,25 @@ Computer Architecture},
         YEAR               = {1992}
 }
 
-@inproceedings{Bou97,
-   title = {Using reflection to build efficient and certified decision procedure
+@INPROCEEDINGS{Bou97,
+   TITLE       = {Using reflection to build efficient and certified decision procedure
 s},
-   author = {S. Boutin},
-   booktitle = {TACS'97},
-   editor = {Martin Abadi and Takahashi Ito},
-   publisher = SV,
-   series = lncs,
-   volume=1281, 
-   PS={http://pauillac.inria.fr/~boutin/public_w/submitTACS97.ps.gz}, 
-   year = {1997}
+   AUTHOR      = {S. Boutin},
+   BOOKTITLE   = {TACS'97},
+   EDITOR      = {Martin Abadi and Takahashi Ito},
+   PUBLISHER   = SV,
+   SERIES      = lncs,
+   VOLUME      = 1281, 
+   YEAR        = {1997}
 }
 
-@PhdThesis{Bou97These,
-  author =       {S. Boutin},
-  title =        {R\'eflexions sur les quotients},
-  school =       {Paris 7},
-  year =         1997,
-  type =         {th\`ese d'Universit\'e},
-  month =        apr
+@PHDTHESIS{Bou97These,
+  AUTHOR       = {S. Boutin},
+  TITLE        = {R\'eflexions sur les quotients},
+  SCHOOL       = {Paris 7},
+  YEAR         = 1997,
+  TYPE         = {th\`ese d'Universit\'e},
+  MONTH        = apr
 }
 
 @ARTICLE{Bru72,
@@ -297,6 +296,15 @@ s},
         crossref = {Nijmegen93}
 }
 
+@PHDTHESIS{Cor97,
+        AUTHOR             = {C. Cornes},
+        MONTH              = nov,
+        SCHOOL             = {{Universit\'e Paris 7}},
+        TITLE              = {Conception d'un langage de haut niveau de représentation de preuves},
+        TYPE               = {Th\`ese de Doctorat},
+        YEAR               = {1997}
+}
+
 @MASTERSTHESIS{Cou94a,
         AUTHOR             = {J. Courant},
         MONTH              = sep,
@@ -525,14 +533,23 @@ s},
         YEAR               = {1994}
 }
 
-@TechReport{Gim98,
-  author = 	 {E. Gim\'enez},
-  title = 	 {A Tutorial on Recursive Types in Coq},
-  institution =  {INRIA},
-  year = 	 1998,
-  month =	 mar
+@TECHREPORT{Gim98,
+  AUTHOR       = {E. Gim\'enez},
+  TITLE        = {A Tutorial on Recursive Types in Coq},
+  INSTITUTION  = {INRIA},
+  YEAR         = 1998,
+  MONTH        = mar
 }
 
+@UNPUBLISHED{GimCas05,
+  AUTHOR       = {E. Gim\'enez and P. Cast\'eran},
+  TITLE        = {A Tutorial on [Co-]Inductive Types in Coq},
+  INSTITUTION  = {INRIA},
+  YEAR         = 2005,
+  MONTH        = jan,
+  NOTE         = {available at \url{http://coq.inria.fr/doc}}
+} 
+
 @INPROCEEDINGS{Gimenez95b,
         AUTHOR             = {E. Gim\'enez},
         BOOKTITLE          = {Workshop on Types for Proofs and Programs},
@@ -607,8 +624,6 @@ s},
         YEAR               = {1980}
 }
 
-
-
 @InProceedings{Hue87tapsoft,
   author = 	 {G. Huet},
   title = 	 {Programming of Future Generation Computers},
@@ -630,8 +645,6 @@ s},
         YEAR               = {1988}
 }
 
-
-
 @INPROCEEDINGS{Hue88,
         AUTHOR             = {G. Huet},
         BOOKTITLE          = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
@@ -1115,15 +1128,16 @@ Decomposition}},
   note =	 {\url{http://proofgeneral.inf.ed.ac.uk/}}
 }
 
+@Book{CoqArt,
+   title = "Interactive Theorem Proving and Program Development.
+    Coq'Art: The Calculus of Inductive Constructions",
+   author = "Yves Bertot and Pierre Castéran",
+   publisher = "Springer Verlag",
+   series = "Texts in Theoretical Computer Science. An EATCS series", 
+ year = 2004
+  }
 
 
-@Book{CoqArt,
-  author =	 {Yves bertot and Pierre Castéran},
-  title = 	 {Coq'Art},
-  publisher = 	 {Springer-Verlag},
-  year = 	 2004,
-  note =	 {To appear}
-}
 
 @INCOLLECTION{wadler87,
         AUTHOR             = {P. Wadler},