Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

14 files changed, 1264 insertions, 459 deletions

diff --git a/doc/Makefile b/doc/Makefile
index 07b13039..fd508e07 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -207,7 +207,7 @@ faq/html/index.html: faq/FAQ.v.html
 
 GLOBDUMP=$(COQTOP)/glob.dump
 
-LIBDIRS= Logic Bool Arith ZArith Reals Lists Sets Relations Sorting Wellfounded IntMap FSets
+LIBDIRS= Logic Bool Arith ZArith QArith Reals Lists Sets Relations Sorting Wellfounded IntMap FSets
 
 ### Standard library (browsable html format)
 
@@ -232,6 +232,7 @@ stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/ind
 stdlib/Library.coqdoc.tex: 
 	(for dir in $(LIBDIRS) ; do \
 	  $(COQDOC) -q --gallina --body-only --latex --stdout \
+	    --coqlib_path $(COQTOP) \
             -R $(COQTOP)/theories Coq "$(COQTOP)/theories/$$dir/"*.v >> $@ ; done)
 
 stdlib/Library.dvi: $(COMMON) stdlib/Library.coqdoc.tex stdlib/Library.tex
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 95411afa..a05231cd 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -444,7 +444,7 @@ Inductive LE : nat -> nat -> Prop :=
 \end{coq_example}
 
 We can use multiple patterns to write  the proof of the lemma
- \texttt{(n,m:nat) (LE n m)}\verb=\/=\texttt{(LE m n)}:
+ \texttt{forall (n m:nat), (LE n m)}\verb=\/=\texttt{(LE m n)}:
 
 \begin{coq_example}
 Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n :=
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index ed1e6e63..48ce6bd9 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -1,36 +1,87 @@
 \def\Program{\textsc{Program}}
-\def\Russel{\textsc{Russel}}
+\def\Russell{\textsc{Russell}}
+\def\PVS{\textsc{PVS}}
 
-\achapter{The \Program{} tactic}
+\achapter{\Program{}}
 \label{Program}
 \aauthor{Matthieu Sozeau}
 \index{Program}
 
 \begin{flushleft}
-  \em The status of \Program is experimental.
+  \em The status of \Program\ is experimental.
 \end{flushleft}
 
-We present here the \Coq\ \Program tactic commands, used to build certified
-\Coq programs, elaborating them from their algorithmic skeleton and a
-rich specification. It can be sought of as a dual of extraction \ref{Extraction}.
+We present here the new \Program\ tactic commands, used to build certified
+\Coq\ programs, elaborating them from their algorithmic skeleton and a
+rich specification. It can be sought of as a dual of extraction
+(chapter \ref{Extraction}). The goal of \Program~is to program as in a regular
+functional programming language whilst using as rich a specification as 
+desired and proving that the code meets the specification using the whole \Coq{} proof
+apparatus. This is done using a technique originating from the
+``Predicate subtyping'' mechanism of \PVS \cite{Rushby98}, which generates type-checking
+conditions while typing a term constrained to a particular type. 
+Here we insert existential variables in the term, which must be filled
+with proofs to get a complete \Coq\ term. \Program\ replaces the
+\Program\ tactic by Catherine Parent \cite{Parent95b} which had a similar goal but is no longer
+maintained.
+
 The languages available as input are currently restricted to \Coq's term
 language, but may be extended to \ocaml{}, \textsc{Haskell} and others
-in the future. Input terms and types are typed in an extended system (\Russel) and
+in the future. We use the same syntax as \Coq\ and permit to use implicit
+arguments and the existing coercion mechanism.
+Input terms and types are typed in an extended system (\Russell) and
 interpreted into \Coq\ terms. The interpretation process may produce
 some proof obligations which need to be resolved to create the final term.
 
 \asection{Elaborating programs}
-\comindex{Program Fixpoint}
+The main difference from \Coq\ is that an object in a type $T : \Set$
+can be considered as an object of type $\{ x : T~|~P\}$ for any
+wellformed $P : \Prop$. 
+If we go from $T$ to the subset of $T$ verifying property $P$, we must
+prove that the object under consideration verifies it. \Russell\ will
+generate an obligation for every such coercion. In the other direction,
+\Russell\ will automatically insert a projection.
+
+Another distinction is the treatment of pattern-matching. Apart from the
+following differences, it is equivalent to the standard {\tt match}
+operation (section \ref{Caseexpr}).
+\begin{itemize}
+\item Generation of equalities. A {\tt match} expression is always
+  generalized by the corresponding equality. As an example,
+  the expression: 
+
+\begin{coq_example*}
+  match x with
+  | 0 => t
+  | S n => u
+  end.
+\end{coq_example*}
+will be first rewrote to:
+\begin{coq_example*}
+  (match x as y return (x = y -> _) with
+  | 0 => fun H : x = 0 -> t
+  | S n => fun H : x = S n -> u
+  end) (refl_equal n).
+\end{coq_example*}
+  
+  This permits to get the proper equalities in the context of proof
+  obligations inside clauses, without which reasoning is very limited.
+  
+\item Coercion. If the object being matched is coercible to an inductive
+  type, the corresponding coercion will be automatically inserted. This also
+  works with the previous mechanism.
+\end{itemize}
 
-The next two commands are similar to they standard counterparts
-\ref{Simpl-definitions} and \ref{Fixpoint} in that
+The next two commands are similar to their standard counterparts
+Definition (section \ref{Simpl-definitions}) and Fixpoint (section \ref{Fixpoint}) in that
 they define constants. However, they may require the user to prove some
-goals to construct the final definitions.
+goals to construct the final definitions. {\em Note:} every subtac
+definition must end with the {\tt Defined} vernacular.
 
-\section{\tt Program Definition {\ident} := {\term}.
+\subsection{\tt Program Definition {\ident} := {\term}.
   \comindex{Program Definition}\label{ProgramDefinition}}
 
-This command types the value {\term} in \Russel and generate subgoals
+This command types the value {\term} in \Russell\ and generate subgoals
 corresponding to proof obligations. Once solved, it binds the final
 \Coq\ term to the name {\ident} in the environment.
 
@@ -65,63 +116,36 @@ corresponding to proof obligations. Once solved, it binds the final
 
 \SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
 
-\section{\tt Program Fixpoint {\ident} {\params} {\tt \{order\}} : type$_0$ := \term$_0$ 
+\subsection{\tt Program Fixpoint {\ident} {\params} {\tt \{order\}} : type := \term
   \comindex{Program Fixpoint}
   \label{ProgramFixpoint}}
 
-This command allows to define objects using a fixed point
-construction. The meaning of this declaration is to define {\it ident}
-a recursive function with arguments specified by
-{\binder$_1$}\ldots{\binder$_n$} such that {\it ident} applied to
-arguments corresponding to these binders has type \type$_0$, and is
-equivalent to the expression \term$_0$. The type of the {\ident} is
-consequently {\tt forall {\params} {\tt,} \type$_0$}
-and the value is equivalent to {\tt fun {\params} {\tt =>} \term$_0$}.
-
-There are two ways to define fixpoints with \Program{}, structural and
-well-founded recursion.
-
-\subsection{\tt Program Fixpoint {\ident} {\params} {\tt \{struct}
-  \ident$_0$ {\tt \}} : type$_0$ := \term$_0$  
-  \comindex{Program Fixpoint Struct}
-  \label{ProgramFixpointStruct}}
-
-To be accepted, a structural {\tt Fixpoint} definition has to satisfy some
-syntactical constraints on a special argument called the decreasing
-argument. They are needed to ensure that the {\tt Fixpoint} definition
-always terminates. The point of the {\tt \{struct \ident {\tt \}}}
-annotation is to let the user tell the system which argument decreases
-along the recursive calls. This annotation may be left implicit for
-fixpoints with one argument. For instance, one can define the identity
-function on naturals as :
+The structural fixpoint operator behaves just like the one of Coq
+(section \ref{Fixpoint}), except it may also generate obligations.
 
 \begin{coq_example}
-Program Fixpoint id (n : nat) : { x : nat | x = n } :=
+Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
   match n with
-  | O => O
-  | S p => S (id p)
+  | S (S p) => S (div2 p)
+  | _ => O
   end.
 \end{coq_example}
 
-The {\tt match} operator matches a value (here \verb:n:) with the
-various constructors of its (inductive) type. The remaining arguments
-give the respective values to be returned, as functions of the
-parameters of the corresponding constructor. Thus here when \verb:n:
-equals \verb:O: we return \verb:0:, and when \verb:n: equals 
-\verb:(S p): we return \verb:(S (id p)):.
-
-The {\tt match} operator is formally described
-in detail in Section~\ref{Caseexpr}.  The system recognizes that in
-the inductive call {\tt (id p)} the argument actually
-decreases because it is a {\em pattern variable} coming from {\tt match
-  n with}.
-
-Here again, proof obligations may be generated. In our example, we would
-have one for each branch:
+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.
+  Show.
 \end{coq_example}
 
+\subsection{\tt Program Lemma {\ident} : type.
+  \comindex{Program Lemma}
+  \label{ProgramLemma}}
+
+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{\tt Program Fixpoint {\ident} {(\ident_$_0$ : \type_$_0$)
 %     \cdots (\ident_$_n$ : \type_$_n$)} {\tt \{wf}
 %   \ident$_i$ \term_{wf} {\tt \}} : type$_t$ := \term$_0$
@@ -483,7 +507,7 @@ Show.
 %  After compilation those two examples run nonetheless,
 %  thanks to the correction of the extraction~\cite{Let02}. 
 
-% $Id: Program.tex 8688 2006-04-07 15:08:12Z msozeau $ 
+% $Id: Program.tex 8890 2006-06-01 21:33:26Z msozeau $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 18b6ed9c..e288cdfb 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -223,8 +223,8 @@ either $x:T$ is an assumption in $\Gamma$ or that there exists some $t$ such
 that $x:=t:T$ is a definition in $\Gamma$. If $\Gamma$ defines some
 $x:=t:T$, we also write $(x:=t:T)\in\Gamma$.  Contexts must be
 themselves {\em well formed}.  For the rest of the chapter, the
-notation $\Gamma::(y:T)$ (resp $\Gamma::(y:=t:T)$) denotes the context
-$\Gamma$ enriched with the declaration $y:T$ (resp $y:=t:T$). The
+notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the context
+$\Gamma$ enriched with the declaration $y:T$ (resp. $y:=t:T$). The
 notation $[]$ denotes the empty context.  \index{Context}
 
 % Does not seem to be used further...
@@ -579,46 +579,95 @@ inductively as being an inductive family of type $\Set\ra\Set$:
 \[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
   \ra (\List~A) \ra (\List~A)}\]
 There are drawbacks to this point of view. The
-information which says that $(\List~\nat)$ is an inductively defined
+information which says that for any $A$, $(\List~A)$ is an inductively defined
 \Set\ has been lost.
+So we introduce two important definitions.
+
+\paragraph{Inductive parameters, real arguments.}
+An inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits 
+$r$ inductive parameters if each type of constructors $(c:C)$ in
+$\Gamma_C$ is such that 
+\[C\equiv \forall
+p_1:P_1,\ldots,\forall p_r:P_r,\forall a_1:A_1, \ldots \forall a_n:A_n,
+(I~p_1~\ldots p_r~t_1\ldots t_q)\]
+with $I$ one of the inductive definitions in $\Gamma_I$. 
+We say that $n$ is the number of real arguments of the constructor
+$c$. 
+\paragraph{Context of parameters}
+If an inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits 
+$r$ inductive parameters, then there exists a context $\Gamma_P$ of
+size $r$, such that $\Gamma_P=p_1:P_1;\ldots;\forall p_r:P_r$ and 
+if $(t:A)\in\Gamma_I,\Gamma_C$ then $A$ can be written as 
+$\forall p_1:P_1,\ldots \forall p_r:P_r,A'$. 
+We call $\Gamma_P$ the context of parameters of the inductive
+definition and use the notation $\forall \Gamma_P,A'$ for the term $A$.
+\paragraph{Remark.}
+If we have a term $t$ in an instance of an
+inductive definition $I$ which starts with a constructor $c$, then the
+$r$ first arguments of $c$ (the parameters) can be deduced from the
+type $T$ of $t$: these are exactly the $r$ first arguments of $I$ in
+the head normal form of $T$.
+\paragraph{Examples.}
+The \List{} definition has $1$ parameter:
+\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
+  \ra (\List~A) \ra (\List~A)}\]
+This is also the case for this more complex definition where there is
+a recursive argument on a different instance of \List: 
+\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
+           \ra (\List~A\ra A) \ra (\List~A)}\]
+But the following definition has $0$ parameters:
+\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
+           \ra (\List~A) \ra (\List~A*A)}\]
+
 %\footnote{
-%The interested reader may look at the compare the above definition with the two 
+%The interested reader may compare the above definition with the two 
 %following ones which have very different logical meaning:\\
 %$\NInd{}{\List:\Set}{\Nil:\List,\cons : (A:\Set)A
 %  \ra \List \ra \List}$ \\
 %$\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
 %  \ra (\List~A\ra A) \ra (\List~A)}$.}
-
-In the system, we keep track in the syntax of the context of
-parameters. The idea of these parameters is that they can be
-instantiated and still we have an inductive definition for which we
-know the specification.
+\paragraph{Concrete syntax.}
+In the Coq system, the context of parameters is given explicitly
+after the name of the inductive definitions and is shared between the
+arities and the type of constructors.
+% The vernacular declaration of polymorphic trees and forests will be:\\
+% \begin{coq_example*}
+% Inductive Tree (A:Set) : Set := 
+%    Node : A -> Forest A -> Tree A
+% with Forest (A : Set) : Set := 
+%    Empty : Forest A
+%  | Cons  : Tree A -> Forest A -> Forest A
+% \end{coq_example*}
+% will correspond in our formalism to:
+% \[\NInd{}{{\tt Tree}:\Set\ra\Set;{\tt Forest}:\Set\ra \Set}
+%   {{\tt Node} : \forall A:\Set, A \ra {\tt Forest}~A \ra {\tt Tree}~A,
+%    {\tt Empty} : \forall A:\Set, {\tt Forest}~A,
+%    {\tt Cons} : \forall A:\Set, {\tt Tree}~A \ra {\tt Forest}~A \ra
+%    {\tt Forest}~A}\]
+We keep track in the syntax of the number of
+parameters. 
 
 Formally the representation of an inductive declaration
 will be 
-\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} for an inductive
-definition valid in a context $\Gamma$ with parameters $\Gamma_P$, a
+\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} for an inductive
+definition valid in a context $\Gamma$ with $p$ parameters, a
 context of definitions $\Gamma_I$ and a context of constructors
 $\Gamma_C$.
-The occurrences of the variables of $\Gamma_P$ in the contexts
-$\Gamma_I$ and $\Gamma_C$ are bound.
 
-The definition \Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} will be
-well-formed exactly when \NInd{\Gamma,\Gamma_P}{\Gamma_I}{\Gamma_C} is.
-If $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$, an object in 
-\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} applied to $q_1,\ldots,q_r$
-will behave as the corresponding object of 
-\NInd{\Gamma}{\substs{\Gamma_I}{p_i}{q_i}{i=1..r}}{\substs{\Gamma_C}{p_i}{q_i}{i=1..r}}.
+The definition \Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} will be
+well-formed exactly when \NInd{\Gamma}{\Gamma_I}{\Gamma_C} is and 
+when $p$ is (less or equal than) the number of parameters in
+\NInd{\Gamma}{\Gamma_I}{\Gamma_C}. 
 
 \paragraph{Examples}
 The declaration for parameterized lists is:
-\[\Ind{}{A:\Set}{\List:\Set}{\Nil:\List,\cons : A \ra \List \ra
-  \List}\]
+\[\Ind{}{1}{\List:\Set\ra\Set}{\Nil:\forall A:\Set,\List~A,\cons : \forall
+  A:\Set, A \ra \List~A \ra   \List~A}\]
 
 The declaration for the length of lists is:
-\[\Ind{}{A:\Set}{\Length:(\List~A)\ra \nat\ra\Prop}
-      {\LNil:(\Length~(\Nil~A)~\nO),\\ 
-     \LCons :\forall a:A, \forall l:(\List~A),\forall n:\nat, (\Length~l~n)\ra (\Length~(\cons~A~a~l)~(\nS~n))}\]
+\[\Ind{}{1}{\Length:\forall A:\Set, (\List~A)\ra \nat\ra\Prop}
+      {\LNil:\forall A:\Set, \Length~A~(\Nil~A)~\nO,\\ 
+     \LCons :\forall A:\Set,\forall a:A, \forall l:(\List~A),\forall n:\nat, (\Length~A~l~n)\ra (\Length~A~(\cons~A~a~l)~(\nS~n))}\]
 
 The declaration for a mutual inductive definition of forests and trees is:
 \[\NInd{}{\tree:\Set,\forest:\Set}
@@ -647,14 +696,17 @@ with forest : Set :=
   | emptyf : forest
   | consf : tree -> forest -> forest.
 \end{coq_example*}
-The inductive declaration in \Coq\ is slightly different from the one
-we described theoretically. The difference is that in the type of
-constructors the inductive definition is explicitly applied to the
-parameters variables. The \Coq\ type-checker verifies that all
-parameters are applied in the correct manner in each recursive call.
+% The inductive declaration in \Coq\ is slightly different from the one
+% we described theoretically. The difference is that in the type of
+% constructors the inductive definition is explicitly applied to the
+% parameters variables.
+The \Coq\ type-checker verifies that all
+parameters are applied in the correct manner in the conclusion of the
+type of each constructors~:
+
 In particular, the following definition will not be accepted because 
 there is an occurrence of \List\ which is not applied to the parameter
-variable:
+variable in the conclusion of the type of {\tt cons'}:
 \begin{coq_eval}
 Set Printing Depth 50.
 (********** The following is not correct and should produce **********)
@@ -663,25 +715,33 @@ Set Printing Depth 50.
 \begin{coq_example}
 Inductive list' (A:Set) : Set :=
   | nil' : list' A
-  | cons' : A -> list' (A -> A) -> list' A.
+  | cons' : A -> list' A -> list' (A*A).
+\end{coq_example}
+Since \Coq{} version 8.1, there is no restriction about parameters in
+the types of arguments of constructors. The following definition is
+valid:
+\begin{coq_example}
+Inductive list' (A:Set) : Set :=
+  | nil' : list' A
+  | cons' : A -> list' (A->A) -> list' A.
 \end{coq_example}
 
+
 \subsection{Types of inductive objects}
 We have to give the type of constants in an environment $E$ which
 contains an inductive declaration.
 
 \begin{description}
-\item[Ind-Const] Assuming $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
+\item[Ind-Const] Assuming 
   $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
   $[c_1:C_1;\ldots;c_n:C_n]$,
    
-\inference{\frac{\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} \in E
-    ~~j=1\ldots k}{(I_j:\forall~p_1:P_1,\ldots\forall p_r:P_r,A_j) \in E}}
+\inference{\frac{\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E
+    ~~j=1\ldots k}{(I_j:A_j) \in E}}
 
-\inference{\frac{\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} \in E
+\inference{\frac{\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E
     ~~~~i=1.. n}
-   {(c_i:\forall~p_1:P_1,\ldots \forall p_r:P_r,\subst{C_i}{I_j}{(I_j~p_1\ldots
-       p_r)}_{j=1\ldots k})\in E}}
+   {(c_i:C_i)\in E}}
 \end{description}
 
 \paragraph{Example.}
@@ -745,10 +805,13 @@ following cases:
   type $U$ but occurs strictly positively in type $V$
 \item $T$ converts to $(I~a_1 \ldots ~a_m ~ t_1 \ldots ~t_p)$ where
   $I$ is the name of an inductive declaration of the form
-  $\Ind{\Gamma}{p_1:P_1;\ldots;p_m:P_m}{I:A}{c_1:C_1;\ldots;c_n:C_n}$
+  $\Ind{\Gamma}{m}{I:A}{c_1:\forall p_1:P_1,\ldots \forall
+    p_m:P_m,C_1;\ldots;c_n:\forall p_1:P_1,\ldots \forall
+    p_m:P_m,C_n}$ 
   (in particular, it is not mutually defined and it has $m$
   parameters) and $X$ does not occur in any of the $t_i$, and the
-  types of constructor $C_i\{p_j/a_j\}_{j=1\ldots m}$ of $I$ satisfy
+  (instantiated) types of constructor $C_i\{p_j/a_j\}_{j=1\ldots m}$
+  of $I$ satisfy 
   the nested positivity condition for $X$
 %\item more generally, when $T$ is not a type, $X$ occurs strictly
 %positively in $T[x:U]u$ if $X$ does not occur in $U$ but occurs
@@ -760,15 +823,16 @@ positivity condition} for a constant $X$ in the following
 cases:
 
 \begin{itemize}
-\item $T=(I~t_1\ldots ~t_n)$ and $X$ does not occur in
-any $t_i$
+\item $T=(I~b_1\ldots b_m~u_1\ldots ~u_{p})$, $I$ is an inductive
+  definition with $m$ parameters and $X$ does not occur in
+any $u_i$
 \item $T=\forall~x:U,V$ and $X$ occurs only strictly positively in $U$ and
 the type $V$ satisfies the nested positivity condition for $X$
 \end{itemize}
 
 \paragraph{Example}
 
-$X$ occurs strictly positively in $A\ra X$ or $X*A$ or $({\tt list}
+$X$ occurs strictly positively in $A\ra X$ or $X*A$ or $({\tt list}~
 X)$ but not in $X \ra A$ or $(X \ra A)\ra A$ nor $({\tt neg}~A)$
 assuming the notion of product and lists were already defined and {\tt
   neg} is an inductive definition with declaration \Ind{}{A:\Set}{{\tt
@@ -784,17 +848,20 @@ inductive definition.
 \begin{description}
 \item[W-Ind] Let $E$ be an environment and
   $\Gamma,\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that
-  $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$ and $\Gamma_C$ is
-  $[c_1:C_1;\ldots;c_n:C_n]$. 
+  $\Gamma_I$ is $[I_1:\forall \Gamma_p,A_1;\ldots;I_k:\forall
+  \Gamma_P,A_k]$ and $\Gamma_C$ is 
+  $[c_1:\forall \Gamma_p,C_1;\ldots;c_n:\forall \Gamma_p,C_n]$. 
 \inference{
   \frac{
   (\WTE{\Gamma;\Gamma_P}{A_j}{s'_j})_{j=1\ldots  k}
-  ~~ (\WTE{\Gamma;\Gamma_P;\Gamma_I}{C_i}{s_{p_i}})_{i=1\ldots  n}
+  ~~ (\WTE{\Gamma;\Gamma_I;\Gamma_P}{C_i}{s_{p_i}})_{i=1\ldots  n}
 }
-  {\WF{E;\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C}}{\Gamma}}}
+  {\WF{E;\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}}
 providing the following side conditions hold:
 \begin{itemize}
 \item $k>0$, $I_j$, $c_i$ are different names for $j=1\ldots  k$ and $i=1\ldots  n$,
+\item $p$ is the number of parameters of \NInd{\Gamma}{\Gamma_I}{\Gamma_C}
+  and $\Gamma_P$ is the context of parameters, 
 \item for $j=1\ldots  k$ we have $A_j$ is an arity of sort $s_j$ and $I_j
   \notin \Gamma \cup E$,
 \item for $i=1\ldots  n$ we have $C_i$ is a type of constructor of
@@ -809,7 +876,7 @@ constructors which will always be satisfied for the impredicative sort
 on sort \Set{} and generate constraints between universes for
 inductive definitions in types.
 
-\paragraph{Examples}
+\paragraph{Examples.}
 It is well known that existential quantifier can be encoded as an
 inductive definition.
 The following declaration introduces the second-order existential
@@ -862,7 +929,7 @@ ourselves to primitive recursive functions and functionals.
 
 For instance, assuming a parameter $A:\Set$ exists in the context, we
 want to build a function \length\ of type $\ListA\ra \nat$ which
-computes the length of the list, so such that $(\length~\Nil) = \nO$
+computes the length of the list, so such that $(\length~(\Nil~A)) = \nO$
 and $(\length~(\cons~A~a~l)) = (\nS~(\length~l))$.  We want these
 equalities to be recognized implicitly and taken into account in the
 conversion rule.
@@ -883,7 +950,7 @@ principles.
 For instance, in order to prove $\forall l:\ListA,(\LengthA~l~(\length~l))$
 it is enough to prove:
 
-\noindent $(\LengthA~\Nil~(\length~\Nil))$ and
+\noindent $(\LengthA~(\Nil~A)~(\length~(\Nil~A)))$ and
 
 \smallskip
 $\forall a:A, \forall l:\ListA, (\LengthA~l~(\length~l)) \ra
@@ -892,7 +959,7 @@ $\forall a:A, \forall l:\ListA, (\LengthA~l~(\length~l)) \ra
 
 \noindent which given the conversion equalities satisfied by \length\ is the
 same as proving:
-$(\LengthA~\Nil~\nO)$ and $\forall a:A, \forall l:\ListA, 
+$(\LengthA~(\Nil~A)~\nO)$ and $\forall a:A, \forall l:\ListA, 
 (\LengthA~l~(\length~l)) \ra
 (\LengthA~(\cons~A~a~l)~(\nS~(\length~l)))$.
 
@@ -928,35 +995,51 @@ by the $u_1\ldots u_p$ according to the $\iota$-reduction.
 
 Actually, for type-checking a \kw{match\ldots with\ldots end}
 expression we also need to know the predicate $P$ to be proved by case
-analysis.  \Coq{} can sometimes infer this predicate but sometimes
-not. The concrete syntax for describing this predicate uses the
-\kw{as\ldots return} construction. 
-The predicate is made explicit using the syntax~:
-\[\kw{match}~m~\kw{as}~ x~ \kw{return}~ (P~ x) ~\kw{with}~ (c_1~x_{11}~...~x_{1p_1}) \Ra f_1 ~|~\ldots~|~
+analysis. In the general case where $I$ is an inductively defined
+$n$-ary relation, $P$ is a $n+1$-ary relation: the $n$ first arguments
+correspond to the arguments of $I$ (parameters excluded), and the last
+one corresponds to object $m$. \Coq{} can sometimes infer this
+predicate but sometimes not. The concrete syntax for describing this
+predicate uses the \kw{as\ldots in\ldots return} construction. For
+instance, let us assume that $I$ is an unary predicate with one
+parameter. The predicate is made explicit using the syntax~:
+\[\kw{match}~m~\kw{as}~ x~ \kw{in}~ I~\verb!_!~a~ \kw{return}~ (P~ x)
+ ~\kw{with}~ (c_1~x_{11}~...~x_{1p_1}) \Ra f_1 ~|~\ldots~|~
   (c_n~x_{n1}...x_{np_n}) \Ra f_n \kw{end}\]
+The \kw{as} part can be omitted if either the result type does not
+depend on $m$ (non-dependent elimination) or $m$ is a variable (in
+this case, the result type can depend on $m$). The \kw{in} part can be
+omitted if the result type does not depend on the arguments of
+$I$. Note that the arguments of $I$ corresponding to parameters
+\emph{must} be \verb!_!, because the result type is not generalized to
+all possible values of the parameters. The expression after \kw{in}
+must be seen as an \emph{inductive type pattern}. As a final remark,
+expansion of implicit arguments and notations apply to this pattern.
+
 For the purpose of presenting the inference rules, we use a more
 compact notation~:
-\[ \Case{(\lb x \mto P)}{m}{ \lb x_{11}~...~x_{1p_1} \mto f_1 ~|~\ldots~|~
+\[ \Case{(\lb a x \mto P)}{m}{ \lb x_{11}~...~x_{1p_1} \mto f_1 ~|~\ldots~|~
   \lb x_{n1}...x_{np_n} \mto f_n}\]
 
-This is the basic idea which is generalized to the case where $I$ is
-an inductively defined $n$-ary relation (in which case the property
-$P$ to be proved will be a $n+1$-ary relation).
-
-
-\paragraph{Non-dependent elimination.}
-When defining a function by case analysis, we build an object of type $I
-\ra C$ and the minimality principle on an inductively defined logical
-predicate of type $A \ra \Prop$ is often used to prove a property
-$\forall x:A,(I~x)\ra (C~x)$.  This is a particular case of the dependent
-principle that we stated before with a predicate which does not depend
-explicitly on the object in the inductive definition.
-
-For instance, a function testing whether a list is empty 
-can be
-defined as:
-
-\[\lb~l:\ListA \mto\Case{\bool}{l}{\Nil~ \Ra~\true~ |~ (\cons~a~m)~ \Ra~\false}\]
+%% CP 06/06 Obsolete avec la nouvelle syntaxe et incompatible avec la
+%% presentation theorique qui suit
+% \paragraph{Non-dependent elimination.}
+%
+% When defining a function of codomain $C$ by case analysis over an
+% object in an inductive type $I$, we build an object of type $I
+% \ra C$. The minimality principle on an inductively defined logical
+% predicate $I$ of type $A \ra \Prop$ is often used to prove a property
+% $\forall x:A,(I~x)\ra (C~x)$.  These are particular cases of the dependent
+% principle that we stated before with a predicate which does not depend
+% explicitly on the object in the inductive definition.
+
+% For instance, a function testing whether a list is empty 
+% can be
+% defined as:
+% \[\kw{fun} l:\ListA \Ra \kw{match}~l~\kw{with}~ \Nil \Ra \true~
+% |~(\cons~a~m) \Ra \false \kw{end}\]
+% represented by
+% \[\lb~l:\ListA \mto\Case{\bool}{l}{\true~ |~ \lb a~m,~\false}\]
 %\noindent {\bf Remark. } 
 
 % In the system \Coq\ the expression above, can be
@@ -973,9 +1056,9 @@ what can be the type of $P$ with respect to the type of the inductive
 definitions.
 
 We define now a relation \compat{I:A}{B} between an inductive
-definition $I$ of type $A$, an arity $B$ which says that an object in
-the inductive definition $I$ can be eliminated for proving a property
-$P$ of type $B$.
+definition $I$ of type $A$ and an arity $B$. This relation states that
+an object in the inductive definition $I$ can be eliminated for
+proving a property $P$ of type $B$.
 
 The case of inductive definitions in sorts \Set\ or \Type{} is simple.
 There is no restriction on the sort of the predicate to be
@@ -995,7 +1078,7 @@ $I$.
     s_2 \in \Sort}{\compat{I:s_1}{I\ra s_2}}}
 \end{description}
 
-The case of Inductive Definitions of sort \Prop{} is a bit more
+The case of Inductive definitions of sort \Prop{} is a bit more
 complicated, because of our interpretation of this sort. The only
 harmless allowed elimination, is the one when predicate $P$ is also of
 sort \Prop.
@@ -1161,10 +1244,10 @@ following typing rule
   \WTEG{P}{B}~~\compat{(I~q_1\ldots  q_r)}{B}
  ~~
 (\WTEG{f_i}{\CI{(c_{p_i}~q_1\ldots  q_r)}{P}})_{i=1\ldots  l}}
-{\WTEG{\Case{P}{c}{f_1\ldots  f_l}}{(P\ t_1\ldots  t_s\ c)}}}%\\[3mm]
+{\WTEG{\Case{P}{c}{f_1|\ldots  |f_l}}{(P\ t_1\ldots  t_s\ c)}}}%\\[3mm]
 
 provided $I$ is an inductive type in a declaration
-\Ind{\Delta}{\Gamma_P}{\Gamma_I}{\Gamma_C} with $|\Gamma_P| = r$,
+\Ind{\Delta}{r}{\Gamma_I}{\Gamma_C} with 
 $\Gamma_C = [c_1:C_1;\ldots;c_n:C_n]$ and $c_{p_1}\ldots  c_{p_l}$ are the
 only constructors of $I$.
 \end{description}
@@ -1176,7 +1259,7 @@ context being the same in all the judgments).
 
 \[\frac{l:\ListA~~P:\ListA\ra s~~~f_1:(P~(\Nil~A))~~
       f_2:\forall a:A, \forall l:\ListA, (P~(\cons~A~a~l))}
-    {\Case{P}{l}{f_1~f_2}:(P~l)}\]
+    {\Case{P}{l}{f_1~|~f_2}:(P~l)}\]
 
 \[\frac{
      \begin{array}[b]{@{}c@{}} 
@@ -1186,21 +1269,21 @@ H:(\LengthA~L~N) \\ P:\forall l:\ListA, \forall n:\nat, (\LengthA~l~n)\ra
    f_2:\forall a:A, \forall l:\ListA, \forall n:\nat, \forall
   h:(\LengthA~l~n), (P~(\cons~A~a~n)~(\nS~n)~(\LCons~A~a~l~n~h)) 
       \end{array}}
-    {\Case{P}{H}{f_1~f_2}:(P~L~N~H)}\]
+    {\Case{P}{H}{f_1~|~f_2}:(P~L~N~H)}\]
 
 \paragraph{Definition of $\iota$-reduction.}\label{iotared}
 \index{iota-reduction@$\iota$-reduction}
 We still have to define the $\iota$-reduction in the general case.
 
 A $\iota$-redex is a term of the following form:
-\[\Case{P}{(c_{p_i}~q_1\ldots  q_r~a_1\ldots  a_m)}{f_1\ldots 
+\[\Case{P}{(c_{p_i}~q_1\ldots  q_r~a_1\ldots  a_m)}{f_1|\ldots |
     f_l}\]
 with $c_{p_i}$ the $i$-th constructor of the inductive type $I$ with $r$
 parameters.
 
 The $\iota$-contraction of this term is $(f_i~a_1\ldots a_m)$ leading
 to the general reduction rule:
-\[ \Case{P}{(c_{p_i}~q_1\ldots  q_r~a_1\ldots  a_m)}{f_1\ldots 
+\[ \Case{P}{(c_{p_i}~q_1\ldots  q_r~a_1\ldots  a_m)}{f_1|\ldots |
     f_n} \triangleright_{\iota} (f_i~a_1\ldots a_m) \]
 
 \subsection{Fixpoint definitions}
@@ -1245,13 +1328,13 @@ calls are done on variables coming from patterns and representing subterms.
 
 For instance in the case of natural numbers, a proof of the induction
 principle of type 
-\[\forall P:\nat\ra\Prop, (P~\nO)\ra((n:\nat)(P~n)\ra(P~(\nS~n)))\ra
+\[\forall P:\nat\ra\Prop, (P~\nO)\ra(\forall n:\nat, (P~n)\ra(P~(\nS~n)))\ra
 \forall n:\nat, (P~n)\]
 can be represented by the term:
 \[\begin{array}{l}
 \lb P:\nat\ra\Prop\mto\lb f:(P~\nO)\mto \lb g:(\forall n:\nat,
 (P~n)\ra(P~(\nS~n))) \mto\\
-\Fix{h}{h:\forall n:\nat, (P~n):=\lb n:\nat\mto \Case{P}{n}{f~\lb
+\Fix{h}{h:\forall n:\nat, (P~n):=\lb n:\nat\mto \Case{P}{n}{f~|~\lb
     p:\nat\mto (g~p~(h~p))}}
 \end{array}
 \]
@@ -1280,8 +1363,8 @@ syntactically recognized as structurally smaller than $y_{k_i}$
 The definition of being structurally smaller is a bit technical.
 One needs first to  define the notion of 
 {\em recursive arguments of a constructor}\index{Recursive arguments}.
-For an inductive definition \Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C},
-the type of a constructor $c$ have the form
+For an inductive definition \Ind{\Gamma}{r}{\Gamma_I}{\Gamma_C},
+the type of a constructor $c$ has the form
 $\forall p_1:P_1,\ldots \forall p_r:P_r, 
 \forall x_1:T_1, \ldots \forall x_r:T_r, (I_j~p_1\ldots 
 p_r~t_1\ldots  t_s)$ the recursive arguments will correspond to $T_i$ in
@@ -1291,7 +1374,7 @@ which one of the $I_l$ occurs.
 The main rules for being structurally smaller are the following:\\
 Given a variable $y$ of type an inductive
 definition in a declaration 
-\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C}
+\Ind{\Gamma}{r}{\Gamma_I}{\Gamma_C}
 where $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
   $[c_1:C_1;\ldots;c_n:C_n]$.
 The terms structurally smaller than $y$ are:
@@ -1303,7 +1386,7 @@ The terms structurally smaller than $y$ are:
   definition $I_p$ part of the inductive
   declaration corresponding to $y$. 
   Each $f_i$ corresponds to a type of constructor $C_q \equiv
-  \forall y_1:B_1, \ldots \forall y_k:B_k, (I~a_1\ldots a_k)$ 
+  \forall p_1:P_1,\ldots,\forall p_r:P_r, \forall y_1:B_1, \ldots \forall y_k:B_k, (I~a_1\ldots a_k)$ 
   and can consequently be
   written $\lb y_1:B'_1\mto \ldots \lb y_k:B'_k\mto g_i$.
   ($B'_i$ is obtained from $B_i$ by substituting parameters variables)
@@ -1420,7 +1503,7 @@ 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}.
-%They are described inchapter~\ref{Coinductives}.
+%They are described in chapter~\ref{Coinductives}.
 
 \section{\iCIC : the Calculus of Inductive Construction with
   impredicative \Set}\label{impredicativity}
@@ -1470,7 +1553,7 @@ impredicative system for sort \Set{} become~:
      
 
 
-% $Id: RefMan-cic.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ 
+% $Id: RefMan-cic.tex 8914 2006-06-07 14:57:22Z cpaulin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index ce2b75b8..2214864a 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -851,7 +851,8 @@ The type {\tt nat} is defined as the least \verb:Set: containing {\tt
   O} and closed by the {\tt S} constructor. The constants {\tt nat},
 {\tt O} and {\tt S} are added to the environment.
 
-Now let us have a look at the elimination principles. They are three :
+Now let us have a look at the elimination principles. They are three
+of them:
 {\tt nat\_ind}, {\tt nat\_rec} and {\tt nat\_rect}.  The type of {\tt
   nat\_ind} is:
 \begin{coq_example}
@@ -880,8 +881,9 @@ Reset Initial.
 Inductive nat : Set := O | S (_:nat).
 \end{coq_example*}
 In the case where inductive types have no annotations (next section
-gives an example of such annotations), the positivity condition
-implies that a constructor can be defined by only giving the type of
+gives an example of such annotations), 
+%the positivity condition implies that 
+a constructor can be defined by only giving the type of
 its arguments.
 \end{Variants}
 
@@ -910,13 +912,13 @@ Check even_ind.
 \end{coq_example}
 
 From a mathematical point of view it asserts that the natural numbers
-satisfying the predicate {\tt even} are exactly the naturals satisfying
-the clauses {\tt even\_0} or {\tt even\_SS}. This is why, when we want
-to prove any predicate {\tt P} over elements of {\tt even}, it is
-enough to prove it for {\tt O} and to prove that if any natural number
-{\tt n} satisfies {\tt P} its double successor {\tt (S (S n))}
-satisfies also {\tt P}. This is indeed analogous to the structural
-induction principle we got for {\tt nat}.
+satisfying the predicate {\tt even} are exactly in the smallest set of
+naturals satisfying the clauses {\tt even\_0} or {\tt even\_SS}. This
+is why, when we want to prove any predicate {\tt P} over elements of
+{\tt even}, it is enough to prove it for {\tt O} and to prove that if
+any natural number {\tt n} satisfies {\tt P} its double successor {\tt
+  (S (S n))} satisfies also {\tt P}. This is indeed analogous to the
+structural induction principle we got for {\tt nat}.
 
 \begin{ErrMsgs}
 \item \errindex{Non strictly positive occurrence of {\ident} in {\type}}
@@ -925,11 +927,17 @@ built from {\ident}}
 \end{ErrMsgs}
 
 \subsubsection{Parameterized inductive types}
-
-Inductive types may be parameterized. Parameters differ from inductive
-type annotations in the fact that recursive invokations of inductive
-types must always be done with the same values of parameters as its
-specification.
+In the previous example, each constructor introduces a
+different instance of the predicate {\tt even}. In some cases, 
+all the constructors introduces the same generic instance of the
+inductive definition, in which case, instead of an annotation, we use
+a context of parameters which are binders shared by all the
+constructors of the definition.
+
+% Inductive types may be parameterized. Parameters differ from inductive
+% type annotations in the fact that recursive invokations of inductive
+% types must always be done with the same values of parameters as its
+% specification.
 
 The general scheme is:
 \begin{center}
@@ -937,6 +945,11 @@ The general scheme is:
     {\ident$_1$}: {\term$_1$} | {\ldots} | {\ident$_n$}: \term$_n$
 {\tt .}
 \end{center}
+Parameters differ from inductive type annotations in the fact that the
+conclusion of each type of constructor {\term$_i$} invoke the inductive
+type with the same values of parameters as its specification.
+
+
 
 A typical example is the definition of polymorphic lists:
 \begin{coq_example*}
@@ -972,7 +985,39 @@ arguments of the constructors rather than their full type.
 \item \errindex{The {\num}th argument of {\ident} must be {\ident'} in {\type}}
 \end{ErrMsgs}
 
-\SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{elim}.
+\paragraph{New from \Coq{} V8.1} The condition on parameters for
+inductive definitions has been relaxed since \Coq{} V8.1. It is now
+possible in the type of a constructor, to invoke recursively the
+inductive definition on an argument which is not the parameter itself.
+
+One can define~:
+\begin{coq_example}
+Inductive list2 (A:Set) : Set :=
+  | nil2 : list2 A
+  | cons2 : A -> list2 (A*A) -> list2 A.
+\end{coq_example}
+\begin{coq_eval}
+Reset list2.
+\end{coq_eval}
+that can also be written by specifying only the type of the arguments:
+\begin{coq_example*}
+Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)).
+\end{coq_example*}
+But the following definition will give an error:
+\begin{coq_example}
+Inductive listw (A:Set) : Set :=
+  | nilw : listw (A*A)
+  | consw : A -> listw (A*A) -> listw (A*A).
+\end{coq_example}
+Because the conclusion of the type of constructors should be {\tt
+  listw A} in both cases. 
+
+A parameterized inductive definition can be defined using
+annotations instead of parameters but it will sometimes give a
+different (bigger) sort for the inductive definition and will produce
+a less convenient rule for case elimination.
+
+\SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{Tac-induction}.
 
 
 \subsubsection{Mutually defined inductive types
@@ -1091,7 +1136,7 @@ definition.
 
 The objects of an inductive type are well-founded with respect to the
 constructors of the type. In other words, such objects contain only a
-{\it finite} number constructors. Co-inductive types arise from
+{\it finite} number of constructors. Co-inductive types arise from
 relaxing this condition, and admitting types whose objects contain an
 infinity of constructors. Infinite objects are introduced by a
 non-ending (but effective) process of construction, defined in terms
@@ -1130,7 +1175,7 @@ CoInductive EqSt : Stream -> Stream -> Prop :=
 \end{coq_example}
 
 In order to prove the extensionally equality of two streams $s_1$ and
-$s_2$ we have to construct and infinite proof of equality, that is,
+$s_2$ we have to construct an infinite proof of equality, that is,
 an infinite object of type $(\texttt{EqSt}\;s_1\;s_2)$. We will see
 how to introduce infinite objects in Section~\ref{CoFixpoint}.
 
@@ -1146,8 +1191,9 @@ how to introduce infinite objects in Section~\ref{CoFixpoint}.
 
 This command allows to define inductive objects using a fixed point
 construction. The meaning of this declaration is to define {\it ident}
-a recursive function with arguments specified by
-{\binder$_1$}\ldots{\binder$_n$} such that {\it ident} applied to
+a recursive function with arguments specified by the binders in
+\params{} % {\binder$_1$}\ldots{\binder$_n$} 
+such that {\it ident} applied to
 arguments corresponding to these binders has type \type$_0$, and is
 equivalent to the expression \term$_0$. The type of the {\ident} is
 consequently {\tt forall {\params} {\tt,} \type$_0$}
@@ -1277,6 +1323,196 @@ Fixpoint tree_size (t:tree) : nat :=
 A generic command {\tt Scheme} is useful to build automatically various
 mutual induction principles. It is described in Section~\ref{Scheme}.
 
+\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ {\tt \{}decrease\_annot{\tt\}} : type$_0$ := \term$_0$.
+}
+\comindex{Function}
+\label{Function}
+
+This \emph{experimental} command 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 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 necessary be \emph{structurally}
+decreasing. The point of the {\tt
+\{\}} annotation is to name the decreasing argument \emph{and} to
+describe which kind of decreasing criteria must be used to ensure
+termination of recursive calls.
+
+The {\tt Function} construction enjoys also the {\tt with} extension
+to define mutually recursive definitions. However, this feature does
+not work for non structural recursive functions. % VRAI??
+
+See the documentation of {\tt functional induction} (section
+\ref{FunInduction}) and {\tt Functional Scheme} (section
+\ref{FunScheme} and \ref{FunScheme-examples}) for how to use the 
+induction principle to easily reason about the function.
+
+\noindent {\bf Remark: } To obtain the right principle, it is better
+to put rigid parameters of the function as first arguments. For
+example it is better to define plus like this:
+
+\begin{coq_example*}
+Function plus (m n : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (plus m p)
+  end.
+\end{coq_example*}
+\noindent than like this:
+\begin{coq_eval}
+Reset plus.
+\end{coq_eval}
+\begin{coq_example*}
+Function plus (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (plus p m)
+  end.
+\end{coq_example*}
+
+\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.
+
+\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 
+
+\errindex{while trying to define Inductive R\_\ident ...}
+
+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.
+
+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}
+
+
+
+\SeeAlso{\ref{FunScheme},\ref{FunScheme-examples},\ref{FunInduction}}
+
+Depending on the {\tt \{\}} annotation, different definition
+mechanisms are used by {\tt Function}. More precise description
+given below.
+
+
+
+\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ : type$_0$ := \term$_0$.
+\comindex{Function}
+}
+
+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$.
+
+
+\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$.
+\comindex{Function}
+}
+
+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.
+
+\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ {\tt \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$.
+\comindex{Function}}
+
+\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$.
+\comindex{Function}}
+
+Defines a recursive function by well founded recursion. \textbf{The
+module \texttt{Recdef} of the standard library must be loaded for this
+feature}. The {\tt \{\}} annotation is mandatory and must be one of
+the following:
+\begin{itemize}
+\item {\tt \{measure} \term$_1$ \ident$_0${\tt\}} with \ident$_0$
+      being the decreasing argument and \term$_1$ being a function
+      from type of \ident$_0$ to \texttt{nat} for which value on the
+      decreasing argument decreases (for the {\tt lt} order on {\tt
+      nat}) at each recursive call of \term$_0$, parameters of the
+      function are bound in  \term$_0$;
+\item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being
+      the decreasing argument and \term$_1$ an ordering relation on
+      the type of \ident$_0$ (i.e. of type T$_{\ident_0}$
+      $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which
+      the decreasing argument decreases at each recursive call of
+      \term$_0$. The order must be well founded. parameters of the
+      function are bound in  \term$_0$.
+\end{itemize} 
+
+Depending on the annotation, the user is left with some proof
+obligations that will be used to define the function. These proofs
+are: proofs that each recursive call is actually decreasing with
+respect to the given criteria, and (if the criteria is \texttt{wf}) a
+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$.
+
+
+
+%Complete!!
+The way this recursive function is defined is the subject of several
+papers by Yves Bertot, Julien Forest, David Pichardie.
+
+%Exemples ok ici
+
+\bigskip
+
+\noindent {\bf Remark: } Proof obligations are presented as several
+subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independent which means that in order to
+% abort them you will have to abort each separately.
+
+
+
+%The decreasing argument cannot be dependent of another??
+
+%Exemples faux ici
+
+
+
+
+
 \subsubsection{\tt CoFixpoint {\ident} : \type$_0$ := \term$_0$.
 \comindex{CoFixpoint}
 \label{CoFixpoint}}
@@ -1448,4 +1684,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 8606 2006-02-23 13:58:10Z herbelin $ 
+% $Id: RefMan-gal.tex 8915 2006-06-07 15:17:13Z courtieu $ 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index eced8099..de9897c4 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -539,8 +539,8 @@ 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 clause succeeds, i.e. all matching patterns, if any,
+fail at the application of the right-hand-side.
 
 \medskip
 
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index f8a9622c..2f79e5f0 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -536,8 +536,8 @@ Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new
 more efficient and more general simplification algorithm on rings and
 semi-rings.
 
-Hugo Herbelin, Pierre Letouzey and Claudio Sacerdoti Coen added new
-tactic features.
+Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and
+Claudio Sacerdoti Coen added new tactic features.
 
 Hugo Herbelin implemented matching on disjunctive patterns.
 
@@ -547,7 +547,8 @@ connections with the provers {\sc cvcl}, {\sc Simplify} and {\sc
 zenon}. Hugo Herbelin implemented an experimental protocol for calling
 external tools from the tactic language.
 
-%Matthieu Sozeau developed an experimental language to reason over subtypes.
+Matthieu Sozeau developed \textsc{Russell}, an experimental language
+to specify the behavior of programs with subtypes.
 
 A mechanism to automatically use some specific tactic to solve
 unresolved implicit has been implemented by Hugo Herbelin.
@@ -556,13 +557,15 @@ Laurent Théry's contribution on strings and Pierre Letouzey and
 Jean-Christophe Filliâtre's contribution on finite maps have been
 integrated to the {\Coq} standard library. Pierre Letouzey developed a
 library about finite sets ``à la Objective Caml'' and extended the
-lists library.
+lists library. Pierre Letouzey's contribution on rational numbers
+has been integrated too.
 
 Pierre Corbineau extended his tactic for solving first-order
 statements. He wrote a reflexion-based intuitionistic tautology
 solver.
 
-Jean-Marc Notin took care of the general maintenance of the system.
+Jean-Marc Notin took care of {\textsf{coqdoc}} and of the general
+maintenance of the system.
 
 \begin{flushright}
 Palaiseau, Apr. 2006\\
@@ -574,7 +577,7 @@ Hugo Herbelin
 % Integration of ZArith lemmas from Sophia and Nijmegen.
 
 
-% $Id: RefMan-pre.tex 8707 2006-04-13 18:23:35Z herbelin $ 
+% $Id: RefMan-pre.tex 8941 2006-06-09 16:43:42Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 72df6005..f034df41 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1015,7 +1015,7 @@ equivalent to {\tt intros; apply ci}.
 \end{Variants}
 
 \section{Eliminations (Induction and Case Analysis)}
-
+\label{Tac-induction}
 Elimination tactics are useful to prove statements by induction or
 case analysis.  Indeed, they make use of the elimination (or
 induction) principles generated with inductive definitions (see
@@ -1387,42 +1387,83 @@ Qed.
 \end{Variants}
 
 
-\subsection{\tt functional induction \ident\ \term$_1$ \dots\ \term$_n$.
+\subsection{\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$).
 \tacindex{functional induction}
 \label{FunInduction}}
 
-The \emph{experimental} tactic \texttt{functional induction}
-performs case analysis and induction following the definition of
-a (not mutually recursive) function.
+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.
 
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
+Functional Scheme minus_ind := Induction for minus Sort Prop.
+
 Lemma le_minus : forall n m:nat, (n - m <= n).
 intros n m.
-functional induction minus n m; simpl; auto.
+functional induction (minus n m); simpl; auto.
 \end{coq_example}
 \begin{coq_example*}
 Qed.
 \end{coq_example*}
 
-\texttt{functional induction} is a shorthand for the more general
-command \texttt{Functional Scheme} which builds induction
-principles following the recursive structure of (possibly
-mutually recursive)
-functions. \SeeAlso{\ref{FunScheme-examples}} for the difference
-between using one or the other.
+\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
+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 \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 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 normal definition using
+\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
+details.
+
+\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples}}
+
+\ErrMsg 
+
+\errindex{The reference \ident\_ind was not found in the current
+environment}
+
+~
 
-\Rem \texttt{functional induction} may fail on functions built by
-tactics. In particular case analysis of a function are considered
-only if they are not inside an application.
+\errindex{Not the right number of induction arguments}
+ 
+
+\begin{Variants}
+\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
+   using \term$_{m+1}$ with {\term$_{n+1}$} \dots {\term$_m$}}
 
-\Rem Arguments of the function must be given, including the
-implicit ones. If the function is recursive, arguments must be
-variables, otherwise they may be any term.
+ 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.
 
-\SeeAlso{\ref{FunScheme},\ref{FunScheme-examples}}
+\item {\tt functional induction (\ident\ \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}).
+\end{Variants}
 
 \section{Equality}
 
@@ -2067,6 +2108,17 @@ datatype: see~\ref{quote-examples} for the full details.
 % En attente d'un moyen de valoriser les fichiers de demos
 % \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} in the distribution
 
+\section{Classical tactics}
+\label{ClassicalTactics}
+
+In order to ease the proving process, when the {\tt Classical} module is loaded. A few more tactics are available. Make sure to load the module using the \texttt{Require Import} command.
+
+\subsection{{\tt classical\_left, classical\_right} \tacindex{classical\_left} \tacindex{classical\_right}}
+
+The tactics \texttt{classical\_left} and \texttt{classical\_right} are the analog of the \texttt{left} and \texttt{right} but using classical logic. They can only be used for disjunctions.
+Use  \texttt{classical\_left} to prove the left part of the disjunction with the assumption that the negation of right part holds. 
+Use \texttt{classical\_left} to prove the right part of the disjunction with the assumption that the negation of left part holds. 
+
 \section{Automatizing
 \label{Automatizing}}
 
@@ -3087,7 +3139,7 @@ The chapter~\ref{TacticLanguage} gives examples of more complex
 user-defined tactics.
 
 
-% $Id: RefMan-tac.tex 8606 2006-02-23 13:58:10Z herbelin $ 
+% $Id: RefMan-tac.tex 8938 2006-06-09 16:29:01Z jnarboux $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index ecd54f44..57155d21 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -289,10 +289,8 @@ Require Import Arith.
 Fixpoint div2 (n:nat) : nat :=
   match n with
   | O => 0
-  | S n0 => match n0 with
-            | O => 0
-            | S n' => S (div2 n')
-            end
+  | S O => 0
+  | S (S n') => S (div2 n')
   end.
 \end{coq_example*}
 
@@ -300,7 +298,7 @@ The definition of a principle of induction corresponding to the
 recursive structure of \texttt{div2} is defined by the command:
 
 \begin{coq_example}
-Functional Scheme div2_ind := Induction for div2.
+Functional Scheme div2_ind := Induction for div2 Sort Prop.
 \end{coq_example}
 
 You may now look at the type of {\tt div2\_ind}:
@@ -315,7 +313,7 @@ We can now prove the following lemma using this principle:
 \begin{coq_example*}
 Lemma div2_le' : forall n:nat, div2 n <= n.
 intro n.
- pattern n.
+ pattern n , (div2 n).
 \end{coq_example*}
 
 
@@ -330,18 +328,17 @@ simpl; auto with arith.
 Qed.
 \end{coq_example*}
 
-Since \texttt{div2} is not mutually recursive, we can use
-directly the \texttt{functional induction} tactic instead of
-building the principle:
+We can use directly the \texttt{functional induction}
+(\ref{FunInduction}) tactic instead of the pattern/apply trick:
 
 \begin{coq_example*}
-Reset div2_ind.
+Reset div2_le'.
 Lemma div2_le : forall n:nat, div2 n <= n.
 intro n.
 \end{coq_example*}
 
 \begin{coq_example}
-functional induction div2 n.
+functional induction (div2 n).
 \end{coq_example}
 
 \begin{coq_example*}
@@ -351,14 +348,11 @@ auto with arith.
 Qed.
 \end{coq_example*}
 
-\paragraph{remark:} \texttt{functional induction} makes no use of
-an induction principle, so be warned that each time it is
-applied, a term mimicking the structure of \texttt{div2} (roughly
-the size of {\tt div2\_ind}) is built. Using \texttt{Functional
-  Scheme} is generally faster and less memory consuming.  On the
-other hand \texttt{functional induction} performs some extra
-simplifications that \texttt{Functional Scheme} does not, and as
-it is a tactic it can be used in tactic definitions.
+\Rem 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 normal definition using
+\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
+details.
 
 
 \example{Induction scheme for \texttt{tree\_size}}
@@ -398,14 +392,14 @@ recursive structure of \texttt{tree\_size} is defined by the
 command:
 
 \begin{coq_example*}
-Functional Scheme treeInd := Induction for tree_size
- with tree_size forest_size.
+Functional Scheme tree_size_ind := Induction for tree_size Sort Prop
+with forest_size_ind := Induction for forest_size Sort Prop.
 \end{coq_example*}
 
-You may now look at the type of {\tt treeInd}:
+You may now look at the type of {\tt tree\_size\_ind}:
 
 \begin{coq_example}
-Check treeInd.
+Check tree_size_ind.
 \end{coq_example}
 
 
@@ -706,7 +700,7 @@ theorem \texttt{simplify\_ok: (f:formula)(interp\_f (simplify f)) ->
 \end{verbatim}
 But there is a problem with leafs: in the example above one cannot
 write a function that implements, for example, the logical simplifications 
-$A \wedge A \ra A$ or $A \wedge \neg A \ra \texttt{False}$. This is
+$A \land A \ra A$ or $A \land \lnot A \ra \texttt{False}$. This is
 because the \Prop{} is impredicative.
 
 It is better to use that type of formulas:
@@ -724,7 +718,7 @@ Inductive formula : Set :=
 \end{coq_example*}
 
 \texttt{index} is defined in module \texttt{quote}. Equality on that
-type is decidable so we are able to simplify $A \wedge A$ into $A$ at
+type is decidable so we are able to simplify $A \land A$ into $A$ at
 the abstract level. 
 
 When there are variables, there are bindings, and \texttt{quote}
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 867d6036..10cd5b3e 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -1,156 +1,555 @@
-\achapter{\protect{The \texttt{setoid$\_$replace} tactic}}
-\aauthor{Cl\'ement Renard}
+\newtheorem{cscexample}{Example}
+
+\achapter{\protect{User defined equalities and relations}}
+\aauthor{Claudio Sacerdoti Coen\footnote{Based on previous work by
+Cl\'ement Renard}}
 \label{setoid_replace}
 \tacindex{setoid\_replace}
 
-This chapter presents  the \texttt{setoid\_replace} tactic.
-
-\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 allows 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.
-
-\asection{Adding new setoid or morphisms}
-
-Under the toplevel
-load the \texttt{setoid\_replace} files with the command:
-
-\begin{coq_example*}
-  Require Setoid.
-\end{coq_example*}
+This chapter presents the extension of several equality related tactics to
+work over user-defined structures (called setoids) that are equipped with
+ad-hoc equivalence relations meant to behave as equalities.
+Actually, the tactics have also been generalized to relations weaker then
+equivalences (e.g. rewriting systems).
+
+The work generalizes, and is partially based on, a previous implementation of
+the \texttt{setoid\_replace} tactic by Cl\'ement Renard.
+
+\asection{Relations and morphisms}
+
+A parametric \emph{relation} \texttt{R} is any term of type
+\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), relation $A$}. The
+expression $A$, which depends on $x_1$ \ldots $x_n$, is called the
+\emph{carrier} of the relation and \texttt{R} is
+said to be a relation over \texttt{A}; the list $x_1,\ldots,x_n$
+is the (possibly empty) list of parameters of the relation.
+
+\firstexample
+\begin{cscexample}[Parametric relation]
+It is possible to implement finite sets of elements of type \texttt{A}
+as unordered list of elements of type \texttt{A}. The function
+\texttt{set\_eq: forall (A: Type), relation (list A)} satisfied by two lists
+with the same elements is a parametric relation over \texttt{(list A)} with
+one parameter \texttt{A}. The type of \texttt{set\_eq} is convertible with
+\texttt{forall (A: Type), list A -> list A -> Prop}.
+\end{cscexample}
+
+An \emph{instance} of a parametric relation \texttt{R} with $n$ parameters
+is any term \texttt{(R $t_1$ \ldots $t_n$)}.
+
+Let \texttt{R} be a relation over \texttt{A} with $n$ parameters.
+A term is a parametric proof of reflexivity for \texttt{R} if it has type
+\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$),
+ reflexive (R $x_1$ \ldots $x_n$)}. Similar definitions are given for
+parametric proofs of symmetry and transitivity.
+
+\begin{cscexample}[Parametric relation (cont.)]
+The \texttt{set\_eq} relation of the previous example can be proved to be
+reflexive, symmetric and transitive.
+\end{cscexample}
+
+A parametric unary function $f$ of type
+\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), $A_1$ -> $A_2$}
+covariantly respects two parametric relation instances $R_1$ and $R_2$ if,
+whenever $m, n$ satisfy $R_1~x~y$, their images $(f~x)$ and $(f~y)$ 
+satisfy $R_2~(f~x)~(f~y)$ . An $f$ that respects its input and output relations
+will be called a unary covariant \emph{morphism}. We can also say that $f$ is
+a monotone function with respect to $R_1$ and $R_2$. The sequence $x_1,\ldots x_n$ represents the parameters of the morphism.
+
+Let $R_1$ and $R_2$ be two parametric relations.
+The \emph{signature} of a parametric morphism of type
+\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), $A_1$ -> $A_2$} that
+covariantly respects two parametric relations that are instances of
+$R_1$ and $R_2$ is written $R_1 \texttt{++>} R_2$.
+Notice that the special arrow \texttt{++>}, which reminds the reader
+of covariance, is placed between the two parametric relations, not
+between the two carriers or the two relation instances.
+
+The previous definitions are extended straightforwardly to $n$-ary morphisms,
+that are required to be simultaneously monotone on every argument.
+
+Morphisms can also be contravariant in one or more of their arguments.
+A morphism is contravariant on an argument associated to the relation instance
+$R$ if it is covariant on the same argument when the inverse relation
+$R^{-1}$ is considered. The special arrow \texttt{-{}->} is used in signatures
+for contravariant morphisms.
+
+Functions having arguments related by symmetric relations instances are both
+covariant and contravariant in those arguments. The special arrow
+\texttt{==>} is used in signatures for morphisms that are both covariant
+and contravariant.
+
+An instance of a parametric morphism $f$ with $n$ parameters is any term
+\texttt{f $t_1$ \ldots $t_n$}.
+
+\begin{cscexample}[Morphisms]
+Continuing the previous example, let
+\texttt{union: forall (A: Type), list A -> list A -> list A} perform the union
+of two sets by appending one list to the other. \texttt{union} is a binary
+morphism parametric over \texttt{A} that respects the relation instance
+\texttt{(set\_eq A)}. The latter condition is proved by showing
+\texttt{forall (A: Type) (S1 S1' S2 S2': list A), set\_eq A S1 S1' ->
+ set\_eq A S2 S2' -> set\_eq A (union A S1 S2) (union A S1' S2')}.
+
+The signature of the function \texttt{union} is
+\texttt{set\_eq ==> set\_eq ==> set\_eq}.
+\end{cscexample}
+
+\begin{cscexample}[Contravariant morphism]
+The division function \texttt{Rdiv: R -> R -> R} is a morphism of
+signature \texttt{le ++> le -{}-> le} where \texttt{le} is
+the usual order relation over real numbers. Notice that division is
+covariant in its first argument and contravariant in its second
+argument.
+\end{cscexample}
+
+Notice that Leibniz equality is a relation and that every function is a
+morphism that respects Leibniz equality. Unfortunately, Leibniz equality
+is not always the intended equality for a given structure.
+
+In the next section we will describe the commands to register terms as
+parametric relations and morphisms. Several tactics that deal with equality
+in \Coq\ can also work with the registered relations.
+The exact list of tactic will be given in Sect.~\ref{setoidtactics}.
+For instance, the
+tactic \texttt{reflexivity} can be used to close a goal $R~n~n$ whenever
+$R$ is an instance of a registered reflexive relation. However, the tactics
+that replace in a context $C[]$ one term with another one related by $R$
+must verify that $C[]$ is a morphism that respects the intended relation.
+Currently the verification consists in checking whether $C[]$ is a syntactic
+composition of morphism instances that respects some obvious
+compatibility constraints.
+
+\begin{cscexample}[Rewriting]
+Continuing the previous examples, suppose that the user must prove
+\texttt{set\_eq int (union int (union int S1 S2) S2) (f S1 S2)} under the
+hypothesis \texttt{H: set\_eq int S2 (nil int)}. It is possible to
+use the \texttt{rewrite} tactic to replace the first two occurrences of
+\texttt{S2} with \texttt{nil int} in the goal since the context
+\texttt{set\_eq int (union int (union int S1 nil) nil) (f S1 S2)}, being
+a composition of morphisms instances, is a morphism. However the tactic
+will fail replacing the third occurrence of \texttt{S2} unless \texttt{f}
+has also been declared as a morphism.
+\end{cscexample}
+
+\asection{Adding new relations and morphisms}
+A parametric relation
+\textit{Aeq}\texttt{: forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$),
+ relation (A $x_1$ \ldots $x_n$)} over \textit{(A $x_1$ \ldots $x_n$)}
+can be declared with the following command
+
+\comindex{Add Relation}
+\begin{verse}
+  \texttt{Add Relation} \textit{A Aeq}\\
+  ~\zeroone{\texttt{reflexivity proved by} \textit{refl}}\\
+  ~\zeroone{\texttt{symmetry proved by} \textit{sym}}\\
+  ~\zeroone{\texttt{transitivity proved by} \textit{trans}}\\
+  \texttt{~as} \textit{id}.
+\end{verse}
+after having required the \texttt{Setoid} module with the
+\texttt{Require Setoid} command.
+
+The identifier \textit{id} gives a unique name to the morphism and it is
+used by the command to generate fresh names for automatically provided lemmas
+used internally.
+
+Notice that \textit{A} is required to be a term having the same parameters
+of \textit{Aeq}. This is a limitation of the tactic that is often unproblematic
+in practice.
+
+The proofs of reflexivity, symmetry and transitivity can be omitted if the
+relation is not an equivalence relation.
+
+If \textit{Aeq} is a transitive relation, then the command also generates
+a lemma of type:
+\begin{quote}
+\texttt{forall ($x_1$:$T_1$)\ldots($x_n$:$T_n$)
+ (x y x' y': (A $x_1$ \ldots $x_n$))\\
+  Aeq $x_1$ \ldots $x_n$ x' x -> Aeq $x_1$ \ldots $x_n$ y y' ->\\
+  (Aeq $x_1$ \ldots $x_n$ x y -> Aeq $x_1$ \ldots $x_n$ x' y')}
+\end{quote}
+that is used to declare \textit{Aeq} as a parametric morphism of signature
+\texttt{Aeq -{}-> Aeq ++> impl} where \texttt{impl} is logical implication
+seen as a parametric relation over \texttt{Aeq}.
+
+Some tactics
+(\texttt{reflexivity}, \texttt{symmetry}, \texttt{transitivity}) work only
+on relations that respect the expected properties. The remaining tactics
+(\texttt{replace}, \texttt{rewrite} and derived tactics such as
+\texttt{autorewrite}) do not require any properties over the relation.
+However, they are able to replace terms with related ones only in contexts
+that are syntactic compositions of parametric morphism instances declared with
+the following command.
 
-A setoid is just a type \verb+A+ and an equivalence relation on \verb+A+.
+\comindex{Add Morphism}
+\begin{verse}
+  \texttt{Add Morphism} \textit{f}\\
+  \texttt{~with signature} \textit{sig}\\
+  \texttt{~as id}.\\
+  \texttt{Proof}\\
+  ~\ldots\\
+  \texttt{Qed}
+\end{verse}
+
+The command declares \textit{f} as a parametric morphism of signature
+\textit{sig}. The identifier \textit{id} gives a unique name to the morphism
+and it is used by the command to generate fresh names for automatically
+provided lemmas used internally. The number of parameters for \textit{f}
+is inferred by comparing its type with the provided signature.
+The command asks the user to prove interactively that \textit{f} respects
+the relations identified from the signature.
+
+\begin{cscexample}
+We start the example by assuming a small theory over homogeneous sets and
+we declare set equality as a parametric equivalence relation and
+union of two sets as a parametric morphism.
+\begin{verbatim}
+Require Export Relation_Definitions.
+Require Export Setoid.
+Set Implicit Arguments.
+Set Contextual Implicit.
+Parameter set: Type -> Type.
+Parameter empty: forall A, set A.
+Parameter eq_set: forall A, set A -> set A -> Prop.
+Parameter union: forall A, set A -> set A -> set A.
+Axiom eq_set_refl: forall A, reflexive _ (eq_set (A:=A)).
+Axiom eq_set_sym: forall A, symmetric _ (eq_set (A:=A)).
+Axiom eq_set_trans: forall A, transitive _ (eq_set (A:=A)).
+Axiom empty_neutral: forall A (S: set A), eq_set (union S empty) S.
+Axiom union_compat:
+ forall (A : Type),
+  forall x x' : set A, eq_set x x' ->
+  forall y y' : set A, eq_set y y' ->
+   eq_set (union x y) (union x' y').
+
+Add Relation set eq_set
+ reflexivity proved by (@eq_set_refl)
+ symmetry proved by (@eq_set_sym)
+ transitivity proved by (@eq_set_trans)
+ as eq_set_rel.
+
+Add Morphism union
+ with signature eq_set ==> eq_set ==> eq_set
+ as union_mor.
+Proof.
+ exact union_compat.
+Qed.
+\end{verbatim}
 
-The specification of a setoid can be found in the file
+We proceed now by proving a simple lemma performing a rewrite step
+and then applying reflexivity, as we would do working with Leibniz
+equality. Both tactic applications are accepted
+since the required properties over \texttt{eq\_set} and
+\texttt{union} can be established from the two declarations above.
 
-\begin{quotation}
 \begin{verbatim}
-theories/Setoids/Setoid.v
+Goal forall (S: set nat),
+ eq_set (union (union S empty) S) (union S S).
+Proof.
+ intros.
+ rewrite (@empty_neutral).
+ reflexivity.
+Qed.
 \end{verbatim}
-\end{quotation}
-
-It looks like :
-\begin{small}
-\begin{flushleft}
+\end{cscexample}
+
+The tables of relations and morphisms are compatible with the \Coq\ 
+sectioning mechanism. If you declare a relation or a morphism inside a section,
+the declaration will be thrown away when closing the section.
+And when you load a compiled file, all the declarations
+of this file that were not inside a section will be loaded.
+
+\asection{Rewriting and non reflexive relations}
+To replace only one argument of an n-ary morphism it is necessary to prove
+that all the other arguments are related to themselves by the respective
+relation instances.
+
+\begin{cscexample}
+To replace \texttt{(union S empty)} with \texttt{S} in
+\texttt{(union (union S empty) S) (union S S)} the rewrite tactic must
+exploit the monotony of \texttt{union} (axiom \texttt{union\_compat} in
+the previous example). Applying \texttt{union\_compat} by hand we are left
+with the goal \texttt{eq\_set (union S S) (union S S)}.
+\end{cscexample}
+
+When the relations associated to some arguments are not reflexive, the tactic
+cannot automatically prove the reflexivity goals, that are left to the user.
+
+Setoids whose relation are partial equivalence relations (PER)
+are useful to deal with partial functions. Let \texttt{R} be a PER. We say
+that an element \texttt{x} is defined if \texttt{R x x}. A partial function
+whose domain comprises all the defined elements only is declared as a
+morphism that respects \texttt{R}. Every time a rewriting step is performed
+the user must prove that the argument of the morphism is defined.
+
+\begin{cscexample}
+Let \texttt{eqO} be \texttt{fun x y => x = y $\land$ ~x$\neq$ 0} (the smaller PER over
+non zero elements). Division can be declared as a morphism of signature
+\texttt{eq ==> eq0 ==> eq}. Replace \texttt{x} with \texttt{y} in
+\texttt{div x n = div y n} opens the additional goal \texttt{eq0 n n} that
+is equivalent to \texttt{n=n $\land$ n$\neq$0}.
+\end{cscexample}
+
+\asection{Rewriting and non symmetric relations}
+When the user works up to relations that are not symmetric, it is no longer
+the case that any covariant morphism argument is also contravariant. As a
+result it is no longer possible to replace a term with a related one in
+every context, since the obtained goal implies the previous one if and
+only if the replacement has been performed in a contravariant position.
+In a similar way, replacement in an hypothesis can be performed only if
+the replaced term occurs in a covariant position.
+
+\begin{cscexample}[Covariance and contravariance]
+Suppose that division over real numbers has been defined as a
+morphism of signature \texttt{Zdiv: Zlt ++> Zlt -{}-> Zlt} (i.e.
+\texttt{Zdiv} is increasing in its first argument, but decreasing on the
+second one). Let \texttt{<} denotes \texttt{Zlt}. 
+Under the hypothesis \texttt{H: x < y} we have
+\texttt{k < x / y -> k < x / x}, but not
+\texttt{k < y / x -> k < x / x}.
+Dually, under the same hypothesis \texttt{k < x / y -> k < y / y} holds,
+but \texttt{k < y / x -> k < y / y} does not.
+Thus, if the current goal is \texttt{k < x / x}, it is possible to replace
+only the second occurrence of \texttt{x} (in contravariant position)
+with \texttt{y} since the obtained goal must imply the current one.
+On the contrary, if \texttt{k < x / x} is
+an hypothesis, it is possible to replace only the first occurrence of
+\texttt{x} (in covariant position) with \texttt{y} since
+the current hypothesis must imply the obtained one.
+\end{cscexample}
+
+An error message will be raised by the \texttt{rewrite} and \texttt{replace}
+tactics when the user is trying to replace a term that occurs in the
+wrong position.
+
+As expected, composing morphisms together propagates the variance annotations by
+switching the variance every time a contravariant position is traversed.
+\begin{cscexample}
+Let us continue the previous example and let us consider the goal
+\texttt{x / (x / x) < k}. The first and third occurrences of \texttt{x} are
+in a contravariant position, while the second one is in covariant position.
+More in detail, the second occurrence of \texttt{x} occurs
+covariantly in \texttt{(x / x)} (since division is covariant in its first
+argument), and thus contravariantly in \texttt{x / (x / x)} (since division
+is contravariant in its second argument), and finally covariantly in
+\texttt{x / (x / x) < k} (since \texttt{<}, as every transitive relation,
+is contravariant in its first argument with respect to the relation itself).
+\end{cscexample}
+
+\asection{Rewriting in ambiguous setoid contexts}
+One function can respect several different relations and thus it can be
+declared as a morphism having multiple signatures.
+
+\begin{cscexample}
+Union over homogeneous lists can be given all the following signatures:
+\texttt{eq ==> eq ==> eq} (\texttt{eq} being the equality over ordered lists)
+\texttt{set\_eq ==> set\_eq ==> set\_eq} (\texttt{set\_eq} being the equality
+over unordered lists up to duplicates),
+\texttt{multiset\_eq ==> multiset\_eq ==> multiset\_eq} (\texttt{multiset\_eq}
+being the equality over unordered lists).
+\end{cscexample}
+
+To declare multiple signatures for a morphism, repeat the \texttt{Add Morphism}
+command.
+
+When morphisms have multiple signatures it can be the case that a rewrite
+request is ambiguous, since it is unclear what relations should be used to
+perform the rewriting. When non reflexive relations are involved, different
+choices lead to different sets of new goals to prove. In this case the
+tactic automatically picks one choice, but raises a warning describing the
+set of alternative new goals. To force one particular choice, the user
+can switch to the following alternative syntax for rewriting:
+
+\comindex{setoid\_rewrite}
+\begin{verse}
+  \texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}
+  \zeroone{\texttt{in} \textit{ident}}\\
+  \texttt{~generate side conditions}
+  \textit{term}$_1$ \ldots \textit{term}$_n$\\
+\end{verse}
+Up to the \texttt{generate side conditions} part, the syntax is 
+equivalent to the
+one of the \texttt{rewrite} tactic. Additionally, the user can specify a list
+of new goals that the tactic must generate. The tactic will prune out from
+the alternative choices those choices that do not open at least the user
+proposed goals. Thus, providing enough side conditions, the user can restrict
+the tactic to at most one choice.
+
+\begin{cscexample}
+Let \texttt{[=]+} and \texttt{[=]-} be the smaller partial equivalence
+relations over positive (resp. negative) integers. Integer multiplication
+can be declared as a morphism with the following signatures:
+\texttt{Zmult: Zlt ++> [=]+ ==> Zlt} (multiplication with a positive number
+is increasing) and
+\texttt{Zmult: Zlt -{}-> [=]- ==> Zlt} (multiplication with a negative number
+is decreasing).
+Given the hypothesis \texttt{H: x < y} and the goal
+\texttt{(x * n) * m < 0} the tactic \texttt{rewrite H} proposes
+two alternative sets of goals that correspond to proving that \texttt{n}
+and \texttt{m} are both positive or both negative.
+\begin{itemize}
+ \item \texttt{\ldots $\vdash$ (y * n) * m < 0}\\
+       \texttt{\ldots $\vdash$ n [=]+ n}\\
+       \texttt{\ldots $\vdash$ m [=]+ m}\\
+ \item \texttt{\ldots $\vdash$ (y * n) * m < 0}\\
+       \texttt{\ldots $\vdash$ n [=]- n} \\
+       \texttt{\ldots $\vdash$ m [=]- m}
+\end{itemize}
+Remember that \texttt{n [=]+ n} is equivalent to \texttt{n=n $\land$ n > 0}.
+
+To pick the second set of goals it is sufficient to use
+\texttt{setoid\_rewrite H generate side conditions (m [=]- m)}
+since the side condition \texttt{m [=]- m} is contained only in the second set
+of goals.
+\end{cscexample}
+
+\asection{First class setoids and morphisms}
+First class setoids and morphisms can also be handled by encoding them
+as records. The projections of the setoid relation and of the morphism
+function can be registered as parametric relations and morphisms, as
+illustrated by the following example.
+\begin{cscexample}[First class setoids]
 \begin{verbatim}
-Section Setoid.
+Require Export Relation_Definitions.
+Require Setoid.
+
+Record Setoid: Type :=
+{ car:Type;
+  eq:car->car->Prop;
+  refl: reflexive _ eq;
+  sym: symmetric _ eq;
+  trans: transitive _ eq
+}.
 
-Variable A : Type.
-Variable Aeq : A -> A -> Prop.
+Add Relation car eq
+ reflexivity proved by refl
+ symmetry proved by symm
+ transitivity proved by trans
+as eq_rel.
 
-Record Setoid_Theory : Prop :=
-{ Seq_refl : (x:A) (Aeq x x);
-  Seq_sym : (x,y:A) (Aeq x y) -> (Aeq y x);
-  Seq_trans : (x,y,z:A) (Aeq x y) -> (Aeq y z) -> (Aeq x z)
+Record Morphism (S1 S2:Setoid): Type :=
+{ f:car S1 ->car S2;
+  compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2)
 }.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-To define a setoid structure on \verb+A+, you must provide a relation
-\verb|Aeq| on \verb+A+ and prove that \verb|Aeq| is an equivalence
-relation. That is, you have to define an object of type
-\verb|(Setoid_Theory A Aeq)|.
 
-Finally to register a setoid the syntax is:
+Add Morphism f with signature eq ==> eq as apply_mor.
+Proof.
+ intros S1 S2 m.
+ apply (compat S1 S2 m).
+Qed.
+
+Lemma test: forall (S1 S2:Setoid) (m: Morphism S1 S2)
+ (x y: car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y).
+Proof.
+ intros.
+ rewrite H.
+ reflexivity.
+Qed.
+\end{verbatim}
+\end{cscexample}
+
+\asection{Tactics enabled on user provided relations}
+\label{setoidtactics}
+The following tactics, all prefixed by \texttt{setoid\_}, 
+deal with arbitrary
+registered relations and morphisms. Moreover, all the corresponding unprefixed
+tactics (i.e. \texttt{reflexivity, symmetry, transitivity, replace, rewrite})
+have been extended to fall back to their prefixed counterparts when
+the relation involved is not Leibniz equality. Notice, however, that using
+the prefixed tactics it is possible to pass additional arguments such as
+\texttt{generate side conditions} or \texttt{using relation}.
+
+\comindex{setoid\_reflexivity}
+\begin{verse}
+  \texttt{setoid\_reflexivity}
+\end{verse}
+
+\comindex{setoid\_symmetry}
+\begin{verse}
+  \texttt{setoid\_symmetry}
+  \zeroone{\texttt{in} \textit{ident}}\\
+\end{verse}
+
+\comindex{setoid\_transitivity}
+\begin{verse}
+  \texttt{setoid\_transitivity}
+\end{verse}
+
+\comindex{setoid\_rewrite}
+\begin{verse}
+  \texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}\\
+  ~\zeroone{\texttt{in} \textit{ident}}\\
+  ~\zeroone{\texttt{generate side conditions}
+  \textit{term}$_1$ \ldots \textit{term}$_n$}\\
+\end{verse}
+
+The \texttt{generate side conditions} argument cannot be passed to the
+unprefixed form.
+
+\comindex{setoid\_replace}
+\begin{verse}
+  \texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term}
+  ~\zeroone{\texttt{in} \textit{ident}}\\
+  ~\zeroone{\texttt{using relation} \textit{term}}\\
+  ~\zeroone{\texttt{generate side conditions}
+  \textit{term}$_1$ \ldots \textit{term}$_n$}\\
+\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.
+
+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,
+it is possible to register hints for \texttt{autorewrite} that are
+not proof of Leibniz equalities. In particular it is possible to exploit
+\texttt{autorewrite} to simulate normalization in a term rewriting system
+up to user defined equalities.
+
+\asection{Printing relations and morphisms}
+The \texttt{Print Setoids} command shows the list of currently registered
+parametric relations and morphisms. For each morphism its signature is also
+given. When the rewriting tactics refuse to replace a term in a context
+because the latter is not a composition of morphisms, the \texttt{Print Setoids}
+command is useful to understand what additional morphisms should be registered.
+
+\asection{Deprecated syntax and backward incompatibilities}
+Due to backward compatibility reasons, the following syntax for the
+declaration of setoids and morphisms is also accepted.
 
 \comindex{Add Setoid}
-\begin{quotation}
-  \texttt{Add Setoid} \textit{ A Aeq ST}
-\end{quotation}
-
-\noindent where \textit{Aeq} is a term of type \texttt{A->A->Prop} and
-\textit{ST} is a term of type 
-\texttt{(Setoid\_Theory }\textit{A Aeq}\texttt{)}.
-
-\begin{ErrMsgs}
-\item \errindex{Not a valid setoid theory}.\\ 
-  That happens when the typing condition does not hold.
-\item \errindex{A Setoid Theory is already declared for \textit{A}}.\\
-  That happens when you try to declare a second setoid theory for the
-  same type.
-\end{ErrMsgs}
-
-Currently, only one setoid structure
-may be declared for a given type.
-This allows automatic detection of the theory used to achieve the
-replacement.
-
-The table of setoid theories is compatible with the \Coq\ 
-sectioning mechanism. If you declare a setoid inside a section, the
-declaration will be thrown away when closing the section.
-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{iff} {\it i.e.} the logical equivalence.
-
-\asection{Adding new morphisms}
-
-A morphism is nothing else than a function compatible with the
-equivalence relation. 
-You can only replace a term by an equivalent in position of argument
-of a morphism. That's why each morphism has to be
-declared to the system, which will ask you to prove the accurate
-compatibility lemma.
-
-The syntax is the following :
-\comindex{Add Morphism}
-\begin{quotation}
-  \texttt{Add Morphism} \textit{ f }:\textit{ ident}
-\end{quotation}
-
-\noindent where f is the name of a term which type is a non dependent
-product (the term you want to declare as a morphism) and
-\textit{ident} is a new identifier which will denote the
-compatibility lemma.
-
-\begin{ErrMsgs}
-\item \errindex{The term \term \ is already declared as a morphism}
-\item \errindex{The term \term \ is not a product}
-\item \errindex{The term \term \ should not be a dependent product}
-\end{ErrMsgs}
-
-The compatibility lemma generated depends on the setoids already
-declared.
-
-\asection{The tactic itself}
-\tacindex{setoid\_replace}
-\tacindex{setoid\_rewrite}
+\begin{verse}
+  \texttt{Add Setoid} \textit{A Aeq ST} \texttt{as} \textit{ident}
+\end{verse}
+where \textit{Aeq} is a congruence relation without parameters,
+\textit{A} is its carrier and \textit{ST} is an object of type
+\verb|(Setoid_Theory A Aeq)| (i.e. a record packing together the reflexivity,
+symmetry and transitivity lemmas). Notice that the syntax is not completely
+backward compatible since the identifier was not required.
 
-After having registered all the setoids and morphisms you need, you can
-use the tactic called \texttt{setoid\_replace}. The syntax is
-
-\begin{quotation}
-\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
-equivalent of \texttt{rewrite} for setoids. The syntax is 
-
-\begin{quotation}
-\texttt{setoid\_rewrite} \term
-\end{quotation}
-
-\begin{Variants}
- \item \texttt{setoid\_rewrite ->} \term
- \item \texttt{setoid\_rewrite <-} \term
-\end{Variants}
-
-The arrow tells the system in which direction the rewriting has to be
-done. Moreover, you can use \texttt{rewrite} for setoid
-rewriting. In that case the system will check if the term you give is
-an equality or a setoid equivalence and do the appropriate work.
+\comindex{Add Morphism}
+\begin{verse}
+  \texttt{Add Morphism} \textit{ f }:\textit{ ident}.\\
+  Proof.\\
+  \ldots\\
+  Qed.
+\end{verse}
+
+The latter command is restricted to the declaration of morphisms without
+parameters. It is not fully backward compatible since the property the user
+is asked to prove is slightly different: for $n$-ary morphisms the hypotheses
+of the property are permuted; moreover, when the morphism returns a
+proposition, the property is now stated using a bi-implication in place of
+a simple implication. In practice, porting an old development to the new
+semantics is usually quite simple.
+
+Notice that several limitations of the old implementation have been lifted.
+In particular, it is now possible to declare several relations with the
+same carrier and several signatures for the same morphism. Moreover, it is
+now also possible to declare several morphisms having the same signature.
+Finally, the replace and rewrite tactics can be used to replace terms in
+contexts that were refused by the old implementation.
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 378936d9..b9a3a2c5 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -974,6 +974,18 @@ the Calculus of Inductive Constructions}},
         YEAR               = {1992}
 }
 
+@article{Rushby98,
+	TITLE = {Subtypes for Specifications: Predicate Subtyping in
+		{PVS}},
+	AUTHOR = {John Rushby and Sam Owre and N. Shankar},
+	JOURNAL = {IEEE Transactions on Software Engineering},
+	PAGES = {709--720},
+	VOLUME = 24,
+	NUMBER = 9,
+	MONTH = sep,
+	YEAR = 1998
+}
+
 @TECHREPORT{Saibi94,
         AUTHOR             = {A. Sa\"{\i}bi},
         INSTITUTION        = {INRIA},
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index 7862c5c3..f2630da0 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -264,6 +264,10 @@ suffix \verb!.tex!.
   
   Select a \texmacs\ output.
 
+\item[\texttt{--stdout}] ~\par
+
+  Write output to stdout.
+
 \item[\texttt{-o }\textit{file}, \texttt{\mm{}output }\textit{file}] ~\par
   
   Redirect the output into the file `\textit{file}' (meaningless with
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index cbb8580d..10744fe4 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -41,16 +41,20 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Classical_Prop.v
     theories/Logic/Classical_Type.v
     (theories/Logic/Classical.v)
+    theories/Logic/ClassicalFacts.v
     theories/Logic/Decidable.v
+    theories/Logic/DecidableType.v
+    theories/Logic/DecidableTypeEx.v
     theories/Logic/Eqdep_dec.v
     theories/Logic/EqdepFacts.v
     theories/Logic/Eqdep.v
     theories/Logic/JMeq.v
+    theories/Logic/ChoiceFacts.v
     theories/Logic/RelationalChoice.v
     theories/Logic/ClassicalChoice.v
-    theories/Logic/ChoiceFacts.v
     theories/Logic/ClassicalDescription.v
-    theories/Logic/ClassicalFacts.v
+    theories/Logic/ClassicalEpsilon.v
+    theories/Logic/ClassicalUniqueChoice.v
     theories/Logic/Berardi.v
     theories/Logic/Diaconescu.v
     theories/Logic/Hurkens.v
@@ -93,7 +97,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/NArith/BinNat.v
     (theories/NArith/NArith.v)
     theories/NArith/Pnat.v
-  </dd>
+    theories/NArith/Nnat.v
+    theories/NArith/Ndigits.v
+    theories/NArith/Ndist.v
+    theories/NArith/Ndec.v
+.  </dd>
 
   <dt> <b>ZArith</b>:
        Binary integers
@@ -124,6 +132,18 @@ through the <tt>Require Import</tt> command.</p>
     theories/ZArith/Zwf.v
     theories/ZArith/Zbinary.v
     theories/ZArith/Znumtheory.v
+    theories/ZArith/Int.v
+  </dd>
+
+  <dt> <b>Reals</b>:
+    Rational numbers
+  </dt>
+  <dd>
+    theories/QArith/QArith_base.v
+    theories/QArith/Qreduction.v
+    theories/QArith/Qring.v
+    (theories/QArith/QArith.v)
+    theories/QArith/Qreals.v
   </dd>
     
   <dt> <b>Reals</b>:
@@ -185,32 +205,6 @@ through the <tt>Require Import</tt> command.</p>
     (theories/Reals/Reals.v)
   </dd>
     
-  <dt> <b>Bool</b>:
-       Booleans (basic functions and results)
-  </dt>
-  <dd> 
-    theories/Bool/Bool.v
-    theories/Bool/BoolEq.v
-    theories/Bool/DecBool.v
-    theories/Bool/IfProp.v
-    theories/Bool/Sumbool.v
-    theories/Bool/Zerob.v
-    theories/Bool/Bvector.v
-  </dd>
-    
-  <dt> <b>Lists</b>:
-    Polymorphic lists, Streams (infinite sequences)
-  </dt>
-  <dd> 
-    theories/Lists/List.v
-    theories/Lists/ListSet.v
-    theories/Lists/MonoList.v
-    theories/Lists/MoreList.v
-    theories/Lists/SetoidList.v
-    theories/Lists/Streams.v
-    theories/Lists/TheoryList.v
-  </dd>
-  
   <dt> <b>Sets</b>:
        Sets (classical, constructive, finite, infinite, powerset, etc.)
   </dt>
@@ -266,67 +260,89 @@ through the <tt>Require Import</tt> command.</p>
     theories/Wellfounded/Well_Ordering.v
   </dd>
     
-  <dt> <b>Sorting</b>:
-    Axiomatizations of sorts
-  </dt>
-  <dd> 
-    theories/Sorting/Heap.v
-    theories/Sorting/Permutation.v
-    theories/Sorting/Sorting.v
-  </dd>
-  
   <dt> <b>Setoids</b>:
   <dd> 
     theories/Setoids/Setoid.v
   </dd>
     
-  <dt> <b>IntMap</b>:
-    Finite sets/maps as trees indexed by addresses
+  <dt> <b>Bool</b>:
+       Booleans (basic functions and results)
   </dt>
   <dd> 
-    theories/IntMap/Addr.v
-    theories/IntMap/Adist.v
-    theories/IntMap/Addec.v
-    theories/IntMap/Adalloc.v
-    theories/IntMap/Map.v
-    theories/IntMap/Fset.v
-    theories/IntMap/Mapaxioms.v
-    theories/IntMap/Mapiter.v
-    theories/IntMap/Mapcanon.v
-    theories/IntMap/Mapsubset.v
-    theories/IntMap/Lsort.v
-    theories/IntMap/Mapfold.v
-    theories/IntMap/Mapcard.v
-    theories/IntMap/Mapc.v
-    theories/IntMap/Maplists.v
-    theories/IntMap/Allmaps.v
+    theories/Bool/Bool.v
+    theories/Bool/BoolEq.v
+    theories/Bool/DecBool.v
+    theories/Bool/IfProp.v
+    theories/Bool/Sumbool.v
+    theories/Bool/Zerob.v
+    theories/Bool/Bvector.v
   </dd>
     
+  <dt> <b>Lists</b>:
+    Polymorphic lists, Streams (infinite sequences)
+  </dt>
+  <dd> 
+    theories/Lists/List.v
+    theories/Lists/ListSet.v
+    theories/Lists/MonoList.v
+    theories/Lists/SetoidList.v
+    theories/Lists/Streams.v
+    theories/Lists/TheoryList.v
+  </dd>
+
   <dt> <b>FSets</b>:
     Modular implementation of finite sets/maps using lists
   </dt>
   <dd>
-    theories/FSets/DecidableType.v
     theories/FSets/OrderedType.v
+    theories/FSets/OrderedTypeAlt.v
+    theories/FSets/OrderedTypeEx.v
     theories/FSets/FSetInterface.v
     theories/FSets/FSetBridge.v
     theories/FSets/FSetProperties.v
     theories/FSets/FSetEqProperties.v
-    theories/FSets/FSetFacts.v
     theories/FSets/FSetList.v
-    theories/FSets/FSet.v
-    theories/FSets/FMapInterface.v
-    theories/FSets/FMapList.v
-    theories/FSets/FMap.v
+    (theories/FSets/FSets.v)
+    theories/FSets/FSetFacts.v
+    theories/FSets/FSetAVL.v
+    theories/FSets/FSetToFiniteSet.v
+    theories/FSets/FSetWeakProperties.v
     theories/FSets/FSetWeakInterface.v
     theories/FSets/FSetWeakFacts.v
     theories/FSets/FSetWeakList.v
     theories/FSets/FSetWeak.v
+    theories/FSets/FMapInterface.v
+    theories/FSets/FMapList.v
+    theories/FSets/FMapPositive.v
+    theories/FSets/FMapIntMap.v
+    theories/FSets/FMapFacts.v
+    (theories/FSets/FMaps.v)
+    theories/FSets/FMapAVL.v
     theories/FSets/FMapWeakInterface.v
     theories/FSets/FMapWeakList.v
     theories/FSets/FMapWeak.v
+    theories/FSets/FMapWeakFacts.v
   </dd>
 
+  <dt> <b>IntMap</b>:
+    An implementation of finite sets/maps as trees indexed by addresses
+  </dt>
+  <dd> 
+    theories/IntMap/Adalloc.v
+    theories/IntMap/Map.v
+    theories/IntMap/Fset.v
+    theories/IntMap/Mapaxioms.v
+    theories/IntMap/Mapiter.v
+    theories/IntMap/Mapcanon.v
+    theories/IntMap/Mapsubset.v
+    theories/IntMap/Lsort.v
+    theories/IntMap/Mapfold.v
+    theories/IntMap/Mapcard.v
+    theories/IntMap/Mapc.v
+    theories/IntMap/Maplists.v
+    theories/IntMap/Allmaps.v
+  </dd>
+    
   <dt> <b>Strings</b>
     Implementation of string as list of ascii characters
   </dt>
@@ -335,5 +351,15 @@ through the <tt>Require Import</tt> command.</p>
     theories/Strings/String.v
   </dd>
     
+  <dt> <b>Sorting</b>:
+    Axiomatizations of sorts
+  </dt>
+  <dd> 
+    theories/Sorting/Heap.v
+    theories/Sorting/Permutation.v
+    theories/Sorting/Sorting.v
+    theories/Sorting/PermutEq.v
+    theories/Sorting/PermutSetoid.v
   </dd>
+
 </dl>
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 7c840509..73d833c4 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -96,7 +96,6 @@ of the system, called respectively \verb:Prop:, \verb:Set:, and
 Every valid expression $e$ in Gallina is associated with a specification,
 itself a valid expression, called its {\sl type} $\tau(E)$. We write
 $e:\tau(E)$ for the judgment that $e$ is of type $E$. 
-%CP Le role de \tau n'est pas clair.
 You may request \Coq~ to return to you the type of a valid expression by using
 the command \verb:Check::
 
@@ -271,7 +270,6 @@ Goal (A -> B -> C) -> (A -> B) -> A -> C.
 The system displays the current goal below a double line, local hypotheses
 (there are none initially) being displayed above the line. We call 
 the combination of local hypotheses with a goal a {\sl judgment}.
-%The new prompt \verb:Unnamed_thm <: indicates that.
 We are now in an inner 
 loop of the system, in proof mode. 
 New commands are available in this
@@ -287,10 +285,6 @@ of the application to the list of local hypotheses:
 intro H.
 \end{coq_example}
 
-%{\bf Warning} to users of \Coq~ previous versions: The display of a sequent in
-%older versions of \Coq~ is inverse of this convention: the goal is displayed
-%above the double line, the hypotheses below.
-
 Several introductions may be done in one step:
 \begin{coq_example}
 intros H' HA.
@@ -337,7 +331,7 @@ Save trivial_lemma.
 \end{coq_example}
 
 As a comment, the system shows the proof script listing all tactic
-commands used in the proof. % ligne blanche apres exact HA??
+commands used in the proof. 
 
 Let us redo the same proof with a few variations. First of all we may name
 the initial goal as a conjectured lemma:
@@ -345,9 +339,6 @@ the initial goal as a conjectured lemma:
 Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.
 \end{coq_example}
 
-%{\bf Warning} to users of \Coq~ older versions: In order to enter the proof
-%engine, at this point a dummy \verb:Goal.: command had to be typed in.
-
 Next, we may omit the names of local assumptions created by the introduction
 tactics, they can be automatically created by the proof engine as new
 non-clashing names.
@@ -407,7 +398,7 @@ backtrack n steps.
 
 We end this section by showing a useful command, \verb:Inspect n.:,
 which inspects the global \Coq~ environment, showing the last \verb:n: declared
-notions: % Attention ici ??
+notions: 
 \begin{coq_example}
 Inspect 3.
 \end{coq_example}
@@ -522,8 +513,6 @@ such a simple tautology. The reason is that we want to keep
 
 A complete tactic for propositional
 tautologies is indeed available in \Coq~ as the \verb:tauto: tactic. 
-%In order to get this facility, we have to import a library module 
-%called ``Dyckhoff'':
 \begin{coq_example}
 Restart.
 tauto.
@@ -1024,7 +1013,6 @@ more specialised properties.
 
 Assume that we want to develop the theory of sets represented as characteristic
 predicates over some universe \verb:U:. For instance:
-%CP Une petite explication pour le codage de element ?
 \begin{coq_example}
 Variable U : Type.
 Definition set := U -> Prop.
@@ -1099,9 +1087,6 @@ mathematical justification of a logical development relies only on
 
 Conversely, ordinary mathematical definitions can be unfolded at will, they
 are {\sl transparent}. 
-%It is possible to enforce the reverse convention by
-%declaring a definition as {\sl opaque} or a lemma as {\sl transparent}.
-
 \chapter{Induction}
 
 \section{Data Types as Inductively Defined Mathematical Collections}
@@ -1244,8 +1229,7 @@ Reset bool.
 
 
 \subsection{Simple proofs by induction}
-%CP  Pourquoi ne pas commencer par des preuves d'egalite entre termes
-%    convertibles. 
+
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
@@ -1427,7 +1411,6 @@ elim n_le_m.
 What happens here is similar to the behaviour of \verb:elim: on natural
 numbers: it appeals to the relevant induction principle, here \verb:le_ind:,
 which generates the two subgoals, which may then be solved easily
-%as if ``backchaining'' the current goal
 with the help of the defining clauses of \verb:le:.
 \begin{coq_example}
 apply le_n; trivial.
@@ -1519,8 +1502,6 @@ development is not type-checked again.
 You may create your own modules, by writing \Coq~ commands in a file,
 say \verb:my_module.v:. Such a module may be simply loaded in the current
 context, with command \verb:Load my_module:. It may also be compiled,
-%using the command \verb:Compile Module my_module: directly at the
-%\Coq~ toplevel, or else 
 in ``batch'' mode, using the UNIX command
 \verb:coqc:. Compiling the module \verb:my_module.v: creates a 
 file \verb:my_module.vo:{} that can be reloaded with command
@@ -1559,16 +1540,6 @@ provides usual infix notations for arithmetic operators.
 SearchPattern (_ + _ = _).
 \end{coq_example}
 
-% The argument to give is a type and it searches in the current context all
-% constants having the same type modulo certain notion of
-% \textit{isomorphism}. For example~:
-
-% \begin{coq_example}
-% Require Arith.
-% SearchIsos nat -> nat -> Prop.
-% SearchIsos (x,y,z:nat)(le x y) -> (le y z) -> (le x z).
-% \end{coq_example} 
- 
 \section{Now you are on your own}
 
 This tutorial is necessarily incomplete. If you wish to pursue serious
@@ -1581,4 +1552,4 @@ with \Coq, in order to acquaint yourself with various proof techniques.
 
 \end{document}
 
-% $Id: Tutorial.tex 8607 2006-02-23 14:21:14Z herbelin $ 
+% $Id: Tutorial.tex 8715 2006-04-14 12:43:23Z cpaulin $