Merge PR #7104: Sphinx doc chapter 27

5 files changed, 847 insertions, 844 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 8dd73a153..ecc68979e 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-gal.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
   RefMan-pro.v.tex \
-  Setoid.v.tex Universes.v.tex \
+  Universes.v.tex \
   Misc.v.tex)
 
 REFMANTEXFILES:=$(addprefix doc/refman/, \
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 57d867060..cfb3c625b 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -117,7 +117,6 @@ Options A and B of the licence are {\em not} elected.}
 %END LATEX
 \part{Addendum to the Reference Manual}
 \include{AddRefMan-pre}%
-\include{Setoid.v}% Tactique pour les setoides
 \include{AsyncProofs}% Paral-ITP
 \include{Universes.v}% Universe polymorphes
 \include{Misc.v}
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
deleted file mode 100644
index b7b343112..000000000
--- a/doc/refman/Setoid.tex
+++ /dev/null
@@ -1,842 +0,0 @@
-\newtheorem{cscexample}{Example}
-
-\achapter{\protect{Generalized rewriting}}
-%HEVEA\cutname{setoid.html}
-\aauthor{Matthieu Sozeau}
-\label{setoids}
-
-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 toolbox also extends the
-automatic rewriting capabilities of the system, allowing the specification of
-custom strategies for rewriting.
-
-This documentation is adapted from the previous setoid documentation by
-Claudio Sacerdoti Coen (based on previous work by Cl\'ement Renard).
-The new implementation is a drop-in replacement for the old one,\footnote{Nicolas
-Tabareau helped with the gluing.} hence most of the documentation still applies.
-
-The work is a complete rewrite of the previous implementation, based on
-the type class infrastructure. It also improves on and generalizes
-the previous implementation in several ways:
-\begin{itemize}
-\item User-extensible algorithm. The algorithm is separated in two
-  parts: generations of the rewriting constraints (done in ML) and
-  solving of these constraints using type class resolution. As type
-  class resolution is extensible using tactics, this allows users to define
-  general ways to solve morphism constraints.
-\item Sub-relations. An example extension to the base algorithm is the
-  ability to define one relation as a subrelation of another so that
-  morphism declarations on one relation can be used automatically for
-  the other. This is done purely using tactics and type class search.
-\item Rewriting under binders. It is possible to rewrite under binders
-  in the new implementation, if one provides the proper
-  morphisms. Again, most of the work is handled in the tactics.
-\item First-class morphisms and signatures. Signatures and morphisms are
-  ordinary Coq terms, hence they can be manipulated inside Coq, put
-  inside structures and lemmas about them can be proved inside the
-  system. Higher-order morphisms are also allowed.
-\item Performance. The implementation is based on a depth-first search for the first
-  solution to a set of constraints which can be as fast as linear in the
-  size of the term, and the size of the proof term is linear
-  in the size of the original term. Besides, the extensibility allows the
-  user to customize the proof search if necessary.
-\end{itemize}
-
-\asection{Introduction to generalized rewriting}
-
-\subsection{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 $x, y$ 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 instances $I_{R_1}$ and $I_{R_2}$ of $R_1$ and $R_2$ is written $I_{R_1} \texttt{++>} I_{R_2}$.
-Notice that the special arrow \texttt{++>}, which reminds the reader
-of covariance, is placed between the two relation instances, not
-between the two carriers. The signature relation instances and morphism will
-be typed in a context introducing variables for the parameters.
-
-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}$ (\texttt{inverse R} in Coq) 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 A} is
-\texttt{set\_eq A ==> set\_eq A ==> set\_eq A} for all \texttt{A}.
-\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}
-
-Leibniz equality is a relation and 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}
-
-\subsection{Adding new relations and morphisms}
-A parametric relation
-\textit{Aeq}\texttt{: forall ($y_1 : \beta_!$ \ldots $y_m : \beta_m$), relation (A $t_1$ \ldots $t_n$)} over
-\textit{(A : $\alpha_i$ -> \ldots $\alpha_n$ -> }\texttt{Type})
-can be declared with the following command:
-
-\comindex{Add Parametric Relation}
-\begin{quote}
-  \texttt{Add Parametric Relation} ($x_1 : T_1$) \ldots ($x_n : T_k$) :
-  \textit{(A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots $t'_m$)}\\
-  ~\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{quote}
-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 the carrier and relation parameters may refer to the context 
-of variables introduced at the beginning of the declaration, but the
-instances need not be made only of variables.
-Also notice that \textit{A} is \emph{not} required to be a term
-having the same parameters as \textit{Aeq}, although that is often the
-case in practice (this departs from the previous implementation).
-
-\comindex{Add Relation}
-In case the carrier and relations are not parametric, one can use the
-command \texttt{Add Relation} instead, whose syntax is the same except
-there is no local context.
-
-The proofs of reflexivity, symmetry and transitivity can be omitted if the
-relation is not an equivalence relation. The proofs must be instances of the
-corresponding relation definitions: e.g. the proof of reflexivity must
-have a type convertible to \texttt{reflexive (A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots
-  $t'_n$)}. Each proof may refer to the introduced variables as well. 
-
-\begin{cscexample}[Parametric relation]
-For Leibniz equality, we may declare:
-\texttt{Add Parametric Relation (A : Type) :} \texttt{A (@eq A)}\\
-~\zeroone{\texttt{reflexivity proved by} \texttt{@refl\_equal A}}\\
-\ldots
-\end{cscexample}
-
-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.
-
-\comindex{Add Parametric Morphism}
-\begin{quote}
-  \texttt{Add Parametric Morphism} ($x_1 : \T_1$) \ldots ($x_k : \T_k$) :
-  (\textit{f $t_1$ \ldots $t_n$})\\
-  \texttt{~with signature} \textit{sig}\\
-  \texttt{~as id}.\\
-  \texttt{Proof}\\
-  ~\ldots\\
-  \texttt{Qed}
-\end{quote}
-
-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 as the base name of the type class instance definition 
-and as the name of the lemma that proves the well-definedness of the morphism.
-The parameters of the morphism as well as the signature may refer to the
-context of variables.
-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{coq_example*}
-Require Export Setoid.
-Require Export Relation_Definitions.
-Set Implicit Arguments.
-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 A)) 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 Parametric Relation A : (set A) (@eq_set A)
- reflexivity proved by (eq_set_refl (A:=A))
- symmetry proved by (eq_set_sym (A:=A))
- transitivity proved by (eq_set_trans (A:=A))
- as eq_set_rel.
-Add Parametric Morphism A : (@union A) with 
-signature (@eq_set A) ==> (@eq_set A) ==> (@eq_set A) as union_mor.
-Proof. exact (@union_compat A). Qed.
-\end{coq_example*}
-
-\end{cscexample}
-
-It is possible to reduce the burden of specifying parameters using
-(maximally inserted) implicit arguments. If \texttt{A} is always set as
-maximally implicit in the previous example, one can write:
-
-\begin{coq_eval}
-Reset Initial.
-Require Export Setoid.
-Require Export Relation_Definitions.
-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 (set A) eq_set.
-Axiom eq_set_sym: forall {A}, symmetric (set A) eq_set.
-Axiom eq_set_trans: forall {A}, transitive (set A) eq_set.
-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').
-\end{coq_eval}
-
-\begin{coq_example*} 
-Add Parametric Relation A : (set A) 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 Parametric Morphism A : (@union A) with
-  signature eq_set ==> eq_set ==> eq_set as union_mor.
-Proof. exact (@union_compat A). Qed.
-\end{coq_example*}
-
-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{coq_example*}
-Goal forall (S: set nat),
- eq_set (union (union S empty) S) (union S S).
-Proof. intros. rewrite empty_neutral. reflexivity. Qed.
-\end{coq_example*}
-
-The tables of relations and morphisms are managed by the type class
-instance mechanism. The behavior on section close is to generalize
-the instances by the variables of the section (and possibly hypotheses
-used in the proofs of instance declarations) but not to export them in
-the rest of the development for proof search. One can use the
-\texttt{Existing Instance} command to do so outside the section,
-using the name of the declared morphism suffixed by \texttt{\_Morphism}, 
-or use the \texttt{Global} modifier for the corresponding class instance
-declaration (see \S\ref{setoid:first-class}) at definition time.
-When loading a compiled file or importing a module,
-all the declarations of this module will be loaded.
-
-\subsection{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}
-
-\subsection{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{Z.div: Z.lt ++> Z.lt -{}-> Z.lt} (i.e.
-\texttt{Z.div} is increasing in its first argument, but decreasing on the
-second one). Let \texttt{<} denotes \texttt{Z.lt}.
-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}
-
-Contrary to the previous implementation, no specific error message will
-be raised when trying to replace a term that occurs in the wrong
-position. It will only fail because the rewriting constraints are not
-satisfiable. However it is possible to use the \texttt{at} modifier to
-specify which occurrences should be rewritten.
-
-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}
-
-\subsection{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. Contrary to the previous implementation, the
-tactic will always choose the first possible solution to the set of
-constraints generated by a rewrite and will not try to find \emph{all}
-possible solutions to warn the user about.
-
-\asection{Commands and tactics}
-\subsection{First class setoids and morphisms}
-\label{setoid:first-class}
-
-The implementation is based on a first-class representation of
-properties of relations and morphisms as type classes. That is, 
-the various combinations of properties on relations and morphisms 
-are represented as records and instances of theses classes are put
-in a hint database.
-For example, the declaration:
-
-\begin{quote}
-  \texttt{Add Parametric Relation} ($x_1 : T_1$) \ldots ($x_n : T_k$) :
-  \textit{(A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots $t'_m$)}\\
-  ~\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{quote}
-
-is equivalent to an instance declaration:
-
-\begin{quote}
-  \texttt{Instance} ($x_1 : T_1$) \ldots ($x_n : T_k$) \texttt{=>}
-  \textit{id} : \texttt{@Equivalence} \textit{(A $t_1$ \ldots $t_n$) (Aeq
-    $t'_1$ \ldots $t'_m$)} :=\\
-  ~\zeroone{\texttt{Equivalence\_Reflexive :=} \textit{refl}}\\
-  ~\zeroone{\texttt{Equivalence\_Symmetric :=} \textit{sym}}\\
-  ~\zeroone{\texttt{Equivalence\_Transitive :=} \textit{trans}}.
-\end{quote}
-
-The declaration itself amounts to the definition of an object of the
-record type \texttt{Coq.Classes.RelationClasses.Equivalence} and a
-hint added to the \texttt{typeclass\_instances} hint database. 
-Morphism declarations are also instances of a type class defined in
-\texttt{Classes.Morphisms}.
-See the documentation on type classes \ref{typeclasses} and 
-the theories files in \texttt{Classes} for further explanations. 
-
-One can inform the rewrite tactic about morphisms and relations just by
-using the typeclass mechanism to declare them using \texttt{Instance}
-and \texttt{Context} vernacular commands.
-Any object of type \texttt{Proper} (the type of morphism declarations)
-in the local context will also be automatically used by the rewriting 
-tactic to solve constraints.
-
-Other representations of first class setoids and morphisms can also
-be handled by encoding them as records. In the following example,
-the projections of the setoid relation and of the morphism function 
-can be registered as parametric relations and morphisms.
-\begin{cscexample}[First class setoids]
-
-\begin{coq_example*}
-Require Import Relation_Definitions Setoid.
-Record Setoid: Type :=
-{ car:Type;
-  eq:car->car->Prop;
-  refl: reflexive _ eq;
-  sym: symmetric _ eq;
-  trans: transitive _ eq
-}.
-Add Parametric Relation (s : Setoid) : (@car s) (@eq s)
- reflexivity proved by (refl s)
- symmetry proved by (sym s)
- transitivity proved by (trans s) as eq_rel.
-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) }.
-Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) :
- (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor.
-Proof. 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{coq_example*}
-\end{cscexample}
-
-\subsection{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}, \texttt{symmetry}, \texttt{transitivity},
-\texttt{replace}, \texttt{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{using relation}.
-\medskip
-
-\tacindex{setoid\_reflexivity}
-\texttt{setoid\_reflexivity}
-
-\tacindex{setoid\_symmetry}
-\texttt{setoid\_symmetry} \zeroone{\texttt{in} \textit{ident}}
-
-\tacindex{setoid\_transitivity}
-\texttt{setoid\_transitivity}
-
-\tacindex{setoid\_rewrite}
-\texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}
-~\zeroone{\texttt{at} \textit{occs}} ~\zeroone{\texttt{in} \textit{ident}}
-
-\tacindex{setoid\_replace}
-\texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term}
-~\zeroone{\texttt{in} \textit{ident}}
-~\zeroone{\texttt{using relation} \textit{term}}
-~\zeroone{\texttt{by} \textit{tactic}}
-\medskip
-
-The \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 the \texttt{DefaultRelation} instance on the type of the objects.
-By default, it means the most recent \texttt{Equivalence} instance in
-the environment, but it can be customized by declaring new
-\texttt{DefaultRelation} instances. As Leibniz equality is a declared
-equivalence, it will fall back to it if no other relation is declared on
-a given type.
-
-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.
-
-\subsection{Printing relations and morphisms}
-The \texttt{Print Instances} command can be used to show the list of
-currently registered \texttt{Reflexive} (using \texttt{Print Instances Reflexive}),
-\texttt{Symmetric} or \texttt{Transitive} relations,
-\texttt{Equivalence}s, \texttt{PreOrder}s, \texttt{PER}s, and
-Morphisms (implemented as \texttt{Proper} instances). When
- the rewriting tactics refuse to replace a term in a context
-because the latter is not a composition of morphisms, the \texttt{Print Instances}
-commands can be useful to understand what additional morphisms should be
-registered.
-
-\subsection{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{quote}
-  \texttt{Add Setoid} \textit{A Aeq ST} \texttt{as} \textit{ident}
-\end{quote}
-where \textit{Aeq} is a congruence relation without parameters,
-\textit{A} is its carrier and \textit{ST} is an object of type
-\texttt{(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.
-
-\comindex{Add Morphism}
-\begin{quote}
-  \texttt{Add Morphism} \textit{f}:\textit{ident}.\\
-  Proof.\\
-  \ldots\\
-  Qed.
-\end{quote}
-
-The latter command also 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. As discussed in
-the next section, the semantics of the new \texttt{setoid\_rewrite}
-command differs slightly from the old one and \texttt{rewrite}.
-
-\asection{Extensions}
-\subsection{Rewriting under binders}
-
-\textbf{Warning}: Due to compatibility issues, this feature is enabled only when calling 
-the \texttt{setoid\_rewrite} tactics directly and not \texttt{rewrite}.
-
-To be able to rewrite under binding constructs, one must declare
-morphisms with respect to pointwise (setoid) equivalence of functions. 
-Example of such morphisms are the standard \texttt{all} and \texttt{ex}
-combinators for universal and existential quantification respectively. 
-They are declared as morphisms in the \texttt{Classes.Morphisms\_Prop}
-module. For example, to declare that universal quantification is a
-morphism for logical equivalence:
-
-\begin{coq_eval}
-Reset Initial.
-Require Import Setoid Morphisms.
-\end{coq_eval}
-\begin{coq_example}
-Instance all_iff_morphism (A : Type) :
-  Proper (pointwise_relation A iff ==> iff) (@all A).
-Proof. simpl_relation. 
-\end{coq_example}
-\begin{coq_eval}
-Admitted.
-\end{coq_eval}
-
-One then has to show that if two predicates are equivalent at every
-point, their universal quantifications are equivalent. Once we have
-declared such a morphism, it will be used by the setoid rewriting tactic
-each time we try to rewrite under an \texttt{all} application (products
-in \Prop{} are implicitly translated to such applications).
-
-Indeed, when rewriting under a lambda, binding variable $x$, say from
-$P~x$ to $Q~x$ using the relation \texttt{iff}, the tactic will generate
-a proof of \texttt{pointwise\_relation A iff (fun x => P x) (fun x => Q
-x)} from the proof of \texttt{iff (P x) (Q x)} and a constraint of the
-form \texttt{Proper (pointwise\_relation A iff ==> ?) m} will be
-generated for the surrounding morphism \texttt{m}.
-
-Hence, one can add higher-order combinators as morphisms by providing
-signatures using pointwise extension for the relations on the functional
-arguments (or whatever subrelation of the pointwise extension).
-For example, one could declare the \texttt{map} combinator on lists as 
-a morphism:
-\begin{coq_eval}
-Require Import List Setoid Morphisms.
-Set Implicit Arguments.
-Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) :=
-| eq_nil : list_equiv eqA nil nil
-| eq_cons : forall x y, eqA x y ->
-  forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l').
-Generalizable All Variables.
-\end{coq_eval}
-\begin{coq_example*}
-Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} :
-  Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B).
-\end{coq_example*}
-
-where \texttt{list\_equiv} implements an equivalence on lists
-parameterized by an equivalence on the elements.
-
-Note that when one does rewriting with a lemma under a binder
-using \texttt{setoid\_rewrite}, the application of the lemma may capture
-the bound variable, as the semantics are different from rewrite where
-the lemma is first matched on the whole term. With the new
-\texttt{setoid\_rewrite}, matching is done on each subterm separately
-and in its local environment, and all matches are rewritten
-\emph{simultaneously} by default. The semantics of the previous
-\texttt{setoid\_rewrite} implementation can almost be recovered using
-the \texttt{at 1} modifier.
-
-\subsection{Sub-relations}
-
-Sub-relations can be used to specify that one relation is included in
-another, so that morphisms signatures for one can be used for the other.
-If a signature mentions a relation $R$ on the left of an arrow
-\texttt{==>}, then the signature also applies for any relation $S$ that
-is smaller than $R$, and the inverse applies on the right of an arrow. 
-One can then declare only a few morphisms instances that generate the complete set
-of signatures for a particular constant. By default, the only declared
-subrelation is \texttt{iff}, which is a subrelation of \texttt{impl}
-and \texttt{inverse impl} (the dual of implication). That's why we can
-declare only two morphisms for conjunction:
-\texttt{Proper (impl ==> impl ==> impl) and} and 
-\texttt{Proper (iff ==> iff ==> iff) and}. This is sufficient to satisfy
-any rewriting constraints arising from a rewrite using \texttt{iff},
-\texttt{impl} or \texttt{inverse impl} through \texttt{and}.
-
-Sub-relations are implemented in \texttt{Classes.Morphisms} and are a 
-prime example of a mostly user-space extension of the algorithm.
-
-\subsection{Constant unfolding}
-
-The resolution tactic is based on type classes and hence regards user-defined 
-constants as transparent by default. This may slow down the resolution
-due to a lot of unifications (all the declared \texttt{Proper}
-instances are tried at each node of the search tree).
-To speed it up, declare your constant as rigid for proof search
-using the command \texttt{Typeclasses Opaque} (see \S
-\ref{TypeclassesTransparency}).
-
-\asection{Strategies for rewriting}
-
-\subsection{Definitions}
-The generalized rewriting tactic is based on a set of strategies that
-can be combined to obtain custom rewriting procedures. Its set of
-strategies is based on Elan's rewriting strategies
-\cite{Luttik97specificationof}. Rewriting strategies are applied using
-the tactic \texttt{rewrite\_strat $s$} where $s$ is a strategy
-expression. Strategies are defined inductively as described by the
-following grammar:
-
-\def\str#1{\texttt{#1}}
-
-\def\strline#1#2{& \vert & #1 & \text{#2}}
-\def\strlinea#1#2#3{& \vert & \str{#1}~#2 & \text{#3}}
-
-\[\begin{array}{lcll}
-  s, t, u & ::= & ( s ) & \text{strategy} \\
-  \strline{c}{lemma} \\
-  \strline{\str{<-}~c}{lemma, right-to-left} \\
-
-  \strline{\str{fail}}{failure} \\
-  \strline{\str{id}}{identity} \\
-  \strline{\str{refl}}{reflexivity} \\
-  \strlinea{progress}{s}{progress} \\
-  \strlinea{try}{s}{failure catch} \\
-
-  \strline{s~\str{;}~u}{composition} \\
-  \strline{\str{choice}~s~t}{left-biased choice} \\
-
-  \strlinea{repeat}{s}{iteration (+)} \\
-  \strlinea{any}{s}{iteration (*)} \\
-  
-  \strlinea{subterm}{s}{one subterm} \\
-  \strlinea{subterms}{s}{all subterms} \\
-  \strlinea{innermost}{s}{innermost first} \\
-  \strlinea{outermost}{s}{outermost first}\\
-  \strlinea{bottomup}{s}{bottom-up} \\
-  \strlinea{topdown}{s}{top-down} \\
-
-  \strlinea{hints}{hintdb}{apply hint} \\
-  \strlinea{terms}{c \ldots c}{any of the terms}\\
-  \strlinea{eval}{redexpr}{apply reduction}\\
-  \strlinea{fold}{c}{fold expression}
-\end{array}\]
-
-Actually a few of these are defined in term of the others using
-a primitive fixpoint operator:
-
-\[\begin{array}{lcl}
-  \str{try}~s & = & \str{choice}~s~\str{id} \\
-  \str{any}~s & = & \str{fix}~u. \str{try}~(s~\str{;}~u) \\
-  \str{repeat}~s & = & s~\str{;}~\str{any}~s \\
-  \str{bottomup}~s & = &
-  \str{fix}~bu. (\str{choice}~(\str{progress}~(\str{subterms}~bu))~s)~\str{;}~\str{try}~bu \\
-  \str{topdown}~s & = &
-  \str{fix}~td. (\str{choice}~s~(\str{progress}~(\str{subterms}~td)))~\str{;}~\str{try}~td \\
-  \str{innermost}~s & = &  \str{fix}~i. (\str{choice}~(\str{subterm}~i)~s) \\
-  \str{outermost}~s & = &
-  \str{fix}~o. (\str{choice}~s~(\str{subterm}~o))
-\end{array}\]
-
-The basic control strategy semantics are straightforward: strategies are
-applied to subterms of the term to rewrite, starting from the root of
-the term. The lemma strategies unify the left-hand-side of the
-lemma with the current subterm and on success rewrite it to the
-right-hand-side. Composition can be used to continue rewriting on the
-current subterm. The fail strategy always fails while the identity
-strategy succeeds without making progress. The reflexivity strategy
-succeeds, making progress using a reflexivity proof of
-rewriting. Progress tests progress of the argument strategy and fails if
-no progress was made, while \str{try} always succeeds, catching
-failures. Choice is left-biased: it will launch the first strategy and
-fall back on the second one in case of failure. One can iterate a
-strategy at least 1 time using \str{repeat} and at least 0 times using
-\str{any}.
-
-The \str{subterm} and \str{subterms} strategies apply their argument
-strategy $s$ to respectively one or all subterms of the current term
-under consideration, left-to-right. \str{subterm} stops at the first
-subterm for which $s$ made progress. The composite strategies
-\str{innermost} and \str{outermost} perform a single innermost our outermost
-rewrite using their argument strategy. Their counterparts
-\str{bottomup} and \str{topdown} perform as many rewritings as possible,
-starting from the bottom or the top of the term. 
-
-Hint databases created for \texttt{autorewrite} can also be used by
-\texttt{rewrite\_strat} using the \str{hints} strategy that applies any
-of the lemmas at the current subterm. The \str{terms} strategy takes the
-lemma names directly as arguments. The \str{eval} strategy expects a
-reduction expression (see \S\ref{Conversion-tactics}) and succeeds if it
-reduces the subterm under consideration. The \str{fold} strategy takes a
-term $c$ and tries to \emph{unify} it to the current subterm, converting
-it to $c$ on success, it is stronger than the tactic \texttt{fold}. 
-
-
-\subsection{Usage}
-\tacindex{rewrite\_strat}
-
-\texttt{rewrite\_strat}~\textit{s}~\zeroone{\texttt{in} \textit{ident}}: 
-
-  Rewrite using the strategy \textit{s} in hypothesis \textit{ident}
-  or the conclusion.
-
-  \begin{ErrMsgs}
-  \item  \errindex{Nothing to rewrite}. If the strategy failed. 
-  \item  \errindex{No progress made}. If the strategy succeeded but
-    made no progress.
-  \item  \errindex{Unable to satisfy the rewriting constraints}. 
-    If the strategy succeeded and made progress but the corresponding
-    rewriting constraints are not satisfied.
-  \end{ErrMsgs}
-  
-
-The \texttt{setoid\_rewrite}~c tactic is basically equivalent to 
-\texttt{rewrite\_strat}~(\str{outermost}~c).
-
-
-
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
new file mode 100644
index 000000000..da9e97e6f
--- /dev/null
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -0,0 +1,845 @@
+.. _generalizedrewriting:
+
+-----------------------
+ Generalized rewriting
+-----------------------
+
+:Author: Matthieu Sozeau
+
+Generalized rewriting
+=====================
+
+
+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
+toolbox also extends the automatic rewriting capabilities of the
+system, allowing the specification of custom strategies for rewriting.
+
+This documentation is adapted from the previous setoid documentation
+by Claudio Sacerdoti Coen (based on previous work by Clément Renard).
+The new implementation is a drop-in replacement for the old one
+[#tabareau]_, hence most of the documentation still applies.
+
+The work is a complete rewrite of the previous implementation, based
+on the type class infrastructure. It also improves on and generalizes
+the previous implementation in several ways:
+
+
++ User-extensible algorithm. The algorithm is separated in two parts:
+  generations of the rewriting constraints (done in ML) and solving of
+  these constraints using type class resolution. As type class
+  resolution is extensible using tactics, this allows users to define
+  general ways to solve morphism constraints.
++ Sub-relations. An example extension to the base algorithm is the
+  ability to define one relation as a subrelation of another so that
+  morphism declarations on one relation can be used automatically for
+  the other. This is done purely using tactics and type class search.
++ Rewriting under binders. It is possible to rewrite under binders in
+  the new implementation, if one provides the proper morphisms. Again,
+  most of the work is handled in the tactics.
++ First-class morphisms and signatures. Signatures and morphisms are
+  ordinary Coq terms, hence they can be manipulated inside Coq, put
+  inside structures and lemmas about them can be proved inside the
+  system. Higher-order morphisms are also allowed.
++ Performance. The implementation is based on a depth-first search for
+  the first solution to a set of constraints which can be as fast as
+  linear in the size of the term, and the size of the proof term is
+  linear in the size of the original term. Besides, the extensibility
+  allows the user to customize the proof search if necessary.
+
+.. [#tabareau] Nicolas Tabareau helped with the gluing.
+
+Introduction to generalized rewriting
+-------------------------------------
+
+
+Relations and morphisms
+~~~~~~~~~~~~~~~~~~~~~~~
+
+A parametric *relation* ``R`` is any term of type
+``forall (x1 :T1 ) ... (xn :Tn ), relation A``.
+The expression ``A``, which depends on ``x1 ... xn`` , is called the *carrier*
+of the relation and ``R`` is said to be a relation over ``A``; the list
+``x1,...,xn`` is the (possibly empty) list of parameters of the relation.
+
+**Example 1 (Parametric relation):**
+
+It is possible to implement finite sets of elements of type ``A`` as
+unordered list of elements of type ``A``.
+The function ``set_eq: forall (A: Type), relation (list A)``
+satisfied by two lists with the same elements is a parametric relation
+over ``(list A)`` with one parameter ``A``. The type of ``set_eq``
+is convertible with ``forall (A: Type), list A -> list A -> Prop.``
+
+An *instance* of a parametric relation ``R`` with n parameters is any term
+``(R t1 ... tn )``.
+
+Let ``R`` be a relation over ``A`` with ``n`` parameters. A term is a parametric
+proof of reflexivity for ``R`` if it has type
+``forall (x1 :T1 ) ... (xn :Tn), reflexive (R x1 ... xn )``.
+Similar definitions are given for parametric proofs of symmetry and transitivity.
+
+**Example 2 (Parametric relation (cont.)):**
+
+The ``set_eq`` relation of the previous example can be proved to be
+reflexive, symmetric and transitive. A parametric unary function ``f`` of type
+``forall (x1 :T1 ) ... (xn :Tn ), A1 -> A2`` covariantly respects two parametric relation instances
+``R1`` and ``R2`` if, whenever ``x``, ``y`` satisfy ``R1 x y``, their images (``f x``) and (``f y``)
+satisfy ``R2 (f x) (f y)``. An ``f`` that respects its input and output
+relations will be called a unary covariant *morphism*. We can also say
+that ``f`` is a monotone function with respect to ``R1`` and ``R2`` . The
+sequence ``x1 ... xn`` represents the parameters of the morphism.
+
+Let ``R1`` and ``R2`` be two parametric relations. The *signature* of a
+parametric morphism of type ``forall (x1 :T1 ) ... (xn :Tn ), A1 -> A2``
+that covariantly respects two instances :math:`I_{R_1}` and :math:`I_{R_2}` of ``R1`` and ``R2``
+is written :math:`I_{R_1} ++> I_{R_2}`. Notice that the special arrow ++>, which
+reminds the reader of covariance, is placed between the two relation
+instances, not between the two carriers. The signature relation
+instances and morphism will be typed in a context introducing
+variables for the parameters.
+
+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 :math`R` if it is covariant on the same argument when the inverse
+relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->``
+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 ``==>`` is used in signatures for morphisms that are both
+covariant and contravariant.
+
+An instance of a parametric morphism :math:`f` with :math:`n`
+parameters is any term :math:`f \, t_1 \ldots t_n`.
+
+**Example 3 (Morphisms):**
+
+Continuing the previous example, let ``union: forall (A: Type), list A -> list A -> list A``
+perform the union of two sets by appending one list to the other. ``union` is a binary
+morphism parametric over ``A`` that respects the relation instance
+``(set_eq A)``. The latter condition is proved by showing:
+
+.. coqtop:: in
+
+  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 ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A``
+for all ``A``.
+
+**Example 4 (Contravariant morphism):**
+
+The division function ``Rdiv: R -> R -> R`` is a morphism of signature
+``le ++> le --> le`` where ``le`` is the usual order relation over
+real numbers. Notice that division is covariant in its first argument
+and contravariant in its second argument.
+
+Leibniz equality is a relation and 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 :ref:`in this section <tactics-enabled-on-user-provided-relations>`.
+For instance, the tactic 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.
+
+
+**Example 5 (Rewriting):**
+
+Continuing the previous examples, suppose that the user must prove
+``set_eq int (union int (union int S1 S2) S2) (f S1 S2)`` under the
+hypothesis ``H: set_eq int S2 (@nil int)``. It
+is possible to use the ``rewrite`` tactic to replace the first two
+occurrences of ``S2`` with ``@nil int`` in the goal since the
+context ``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 ``S2``  unless ``f``
+has also been declared as a morphism.
+
+
+Adding new relations and morphisms
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm )`,
+:g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)` can be
+declared with the following command:
+
+.. cmd::  Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m ) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident.
+
+after having required the ``Setoid`` module with the ``Require Setoid``
+command.
+
+The :g:`@ident` 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 the carrier and relation parameters may refer to the
+context of variables introduced at the beginning of the declaration,
+but the instances need not be made only of variables. Also notice that
+``A`` is *not* required to be a term having the same parameters as ``Aeq``,
+although that is often the case in practice (this departs from the
+previous implementation).
+
+
+.. cmd:: Add Relation
+
+In case the carrier and relations are not parametric, one can use this command
+instead, whose syntax is the same except there is no local context.
+
+The proofs of reflexivity, symmetry and transitivity can be omitted if
+the relation is not an equivalence relation. The proofs must be
+instances of the corresponding relation definitions: e.g. the proof of
+reflexivity must have a type convertible to
+:g:`reflexive (A t1 ... tn) (Aeq t′ 1 …t′ n )`.
+Each proof may refer to the introduced variables as well.
+
+**Example 6 (Parametric relation):**
+
+For Leibniz equality, we may declare:
+
+.. coqtop:: in
+
+  Add Parametric Relation (A : Type) : A (@eq A)
+    [reflexivity proved by @refl_equal A]
+  ...
+
+Some tactics (``reflexivity``, ``symmetry``, ``transitivity``) work only on
+relations that respect the expected properties. The remaining tactics
+(``replace``, ``rewrite`` and derived tactics such as ``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.
+
+.. cmd:: Add Parametric Morphism (x1 : T1 ) ... (xk : Tk ) : (f t1 ... tn ) with signature sig as @ident.
+
+The command declares ``f`` as a parametric morphism of signature ``sig``. The
+identifier ``id`` gives a unique name to the morphism and it is used as
+the base name of the type class instance definition and as the name of
+the lemma that proves the well-definedness of the morphism. The
+parameters of the morphism as well as the signature may refer to the
+context of variables. The command asks the user to prove interactively
+that ``f`` respects the relations identified from the signature.
+
+**Example 7:**
+
+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.
+
+.. coqtop:: in
+
+   Require Export Setoid.
+   Require Export Relation_Definitions.
+
+   Set Implicit Arguments.
+
+   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 A)) 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 Parametric Relation A : (set A) (@eq_set A)
+            reflexivity proved by (eq_set_refl (A:=A))
+            symmetry proved by (eq_set_sym (A:=A))
+            transitivity proved by (eq_set_trans (A:=A))
+            as eq_set_rel.
+
+   Add Parametric Morphism A : (@union A) with
+            signature (@eq_set A) ==> (@eq_set A) ==> (@eq_set A) as union_mor.
+   Proof.
+     exact (@union_compat A).
+   Qed.
+
+It is possible to reduce the burden of specifying parameters using
+(maximally inserted) implicit arguments. If ``A`` is always set as
+maximally implicit in the previous example, one can write:
+
+.. coqtop:: in
+
+   Add Parametric Relation A : (set A) eq_set
+     reflexivity proved by eq_set_refl
+     symmetry proved by eq_set_sym
+     transitivity proved by eq_set_trans
+     as eq_set_rel.
+
+.. coqtop:: in
+
+   Add Parametric Morphism A : (@union A) with
+     signature eq_set ==> eq_set ==> eq_set as union_mor.
+
+.. coqtop:: in
+
+   Proof. exact (@union_compat A). Qed.
+
+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 ``eq_set`` and ``union`` can be established from the two
+declarations above.
+
+.. coqtop:: in
+
+   Goal forall (S: set nat),
+     eq_set (union (union S empty) S) (union S S).
+
+.. coqtop:: in
+
+   Proof. intros. rewrite empty_neutral. reflexivity. Qed.
+
+The tables of relations and morphisms are managed by the type class
+instance mechanism. The behavior on section close is to generalize the
+instances by the variables of the section (and possibly hypotheses
+used in the proofs of instance declarations) but not to export them in
+the rest of the development for proof search. One can use the
+``Existing Instance`` command to do so outside the section, using the name of the
+declared morphism suffixed by ``_Morphism``, or use the ``Global`` modifier
+for the corresponding class instance declaration
+(see :ref:`First Class Setoids and Morphisms <first-class-setoids-and-morphisms>`) at
+definition time. When loading a compiled file or importing a module,
+all the declarations of this module will be loaded.
+
+
+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.
+
+**Example 8:**
+
+To replace ``(union S empty)`` with ``S`` in ``(union (union S empty) S) (union S S)``
+the rewrite tactic must exploit the monotony of ``union`` (axiom ``union_compat``
+in the previous example). Applying ``union_compat`` by hand we are left with the
+goal ``eq_set (union S S) (union S S)``.
+
+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 ``R`` be a PER. We say that an
+element ``x`` is defined if ``R x x``. A partial function whose domain
+comprises all the defined elements only is declared as a morphism that
+respects ``R``. Every time a rewriting step is performed the user must
+prove that the argument of the morphism is defined.
+
+**Example 9:**
+
+Let ``eqO`` be ``fun x y => x = y /\ x <> 0`` (the
+smaller PER over non zero elements). Division can be declared as a
+morphism of signature ``eq ==> eq0 ==> eq``. Replace ``x`` with
+``y`` in ``div x n = div y n`` opens the additional goal ``eq0 n n``
+that is equivalent to ``n = n /\ n <> 0``.
+
+
+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.
+
+**Example 10 (Covariance and contravariance):**
+
+Suppose that division over real numbers has been defined as a morphism of signature
+``Z.div: Z.lt ++> Z.lt --> Z.lt`` (i.e. ``Z.div`` is increasing in
+its first argument, but decreasing on the second one). Let ``<``
+denotes ``Z.lt``. Under the hypothesis ``H: x < y`` we have
+``k < x / y -> k < x / x``, but not ``k < y / x -> k < x / x``. Dually,
+under the same hypothesis ``k < x / y -> k < y / y`` holds, but
+``k < y / x -> k < y / y`` does not. Thus, if the current goal is
+``k < x / x``, it is possible to replace only the second occurrence of
+``x`` (in contravariant position) with ``y`` since the obtained goal
+must imply the current one. On the contrary, if ``k < x / x`` is an
+hypothesis, it is possible to replace only the first occurrence of
+``x`` (in covariant position) with ``y`` since the current
+hypothesis must imply the obtained one.
+
+Contrary to the previous implementation, no specific error message
+will be raised when trying to replace a term that occurs in the wrong
+position. It will only fail because the rewriting constraints are not
+satisfiable. However it is possible to use the at modifier to specify
+which occurrences should be rewritten.
+
+As expected, composing morphisms together propagates the variance
+annotations by switching the variance every time a contravariant
+position is traversed.
+
+**Example 11:**
+
+Let us continue the previous example and let us consider
+the goal ``x / (x / x) < k``. The first and third occurrences of
+``x`` are in a contravariant position, while the second one is in
+covariant position. More in detail, the second occurrence of ``x``
+occurs covariantly in ``(x / x)`` (since division is covariant in
+its first argument), and thus contravariantly in ``x / (x / x)``
+(since division is contravariant in its second argument), and finally
+covariantly in ``x / (x / x) < k`` (since ``<``, as every
+transitive relation, is contravariant in its first argument with
+respect to the relation itself).
+
+
+Rewriting in ambiguous setoid contexts
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+One function can respect several different relations and thus it can
+be declared as a morphism having multiple signatures.
+
+**Example 12:**
+
+
+Union over homogeneous lists can be given all the
+following signatures: ``eq ==> eq ==> eq`` (``eq`` being the
+equality over ordered lists) ``set_eq ==> set_eq ==> set_eq``
+(``set_eq`` being the equality over unordered lists up to duplicates),
+``multiset_eq ==> multiset_eq ==> multiset_eq`` (``multiset_eq``
+being the equality over unordered lists).
+
+To declare multiple signatures for a morphism, repeat the ``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. Contrary to the previous
+implementation, the tactic will always choose the first possible
+solution to the set of constraints generated by a rewrite and will not
+try to find *all* possible solutions to warn the user about.
+
+
+Commands and tactics
+--------------------
+
+
+.. _first-class-setoids-and-morphisms:
+
+First class setoids and morphisms
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+
+
+The implementation is based on a first-class representation of
+properties of relations and morphisms as type classes. That is, the
+various combinations of properties on relations and morphisms are
+represented as records and instances of theses classes are put in a
+hint database. For example, the declaration:
+
+.. coqtop:: in
+
+   Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m)
+     [reflexivity proved by refl]
+     [symmetry proved by sym]
+     [transitivity proved by trans]
+     as id.
+
+
+is equivalent to an instance declaration:
+
+.. coqtop:: in
+
+   Instance (x1 : T1) ... (xn : Tk) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) :=
+     [Equivalence_Reflexive := refl]
+     [Equivalence_Symmetric := sym]
+     [Equivalence_Transitive := trans].
+
+The declaration itself amounts to the definition of an object of the
+record type ``Coq.Classes.RelationClasses.Equivalence`` and a hint added
+to the ``typeclass_instances`` hint database. Morphism declarations are
+also instances of a type class defined in ``Classes.Morphisms``. See the
+documentation on type classes :ref:`TODO-chapter-20-type-classes`
+and the theories files in Classes for further explanations.
+
+One can inform the rewrite tactic about morphisms and relations just
+by using the typeclass mechanism to declare them using Instance and
+Context vernacular commands. Any object of type Proper (the type of
+morphism declarations) in the local context will also be automatically
+used by the rewriting tactic to solve constraints.
+
+Other representations of first class setoids and morphisms can also be
+handled by encoding them as records. In the following example, the
+projections of the setoid relation and of the morphism function can be
+registered as parametric relations and morphisms.
+
+**Example 13 (First class setoids):**
+
+.. coqtop:: in
+
+   Require Import Relation_Definitions Setoid.
+
+   Record Setoid: Type :=
+   { car: Type;
+     eq: car -> car -> Prop;
+     refl: reflexive _ eq;
+     sym: symmetric _ eq;
+     trans: transitive _ eq
+   }.
+
+   Add Parametric Relation (s : Setoid) : (@car s) (@eq s)
+     reflexivity proved by (refl s)
+     symmetry proved by (sym s)
+     transitivity proved by (trans s) as eq_rel.
+
+   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)
+   }.
+
+   Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) :
+     (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor.
+   Proof. 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.
+
+.. _tactics-enabled-on-user-provided-relations:
+
+Tactics enabled on user provided relations
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The following tactics, all prefixed by ``setoid_``, deal with arbitrary
+registered relations and morphisms. Moreover, all the corresponding
+unprefixed tactics (i.e. ``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 ``using relation``.
+
+.. tacv:: setoid_reflexivity
+
+.. tacv:: setoid_symmetry [in @ident]
+
+.. tacv:: setoid_transitivity
+
+.. tacv:: setoid_rewrite [@orientation] @term [at @occs] [in @ident]
+
+.. tacv:: setoid_replace @term with @term [in @ident] [using relation @term] [by @tactic]
+
+
+The ``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 the ``DefaultRelation`` instance on the type of
+the objects. By default, it means the most recent ``Equivalence`` instance
+in the environment, but it can be customized by declaring
+new ``DefaultRelation`` instances. As Leibniz equality is a declared
+equivalence, it will fall back to it if no other relation is declared
+on a given type.
+
+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 ``autorewrite`` that
+are not proof of Leibniz equalities. In particular it is possible to
+exploit ``autorewrite`` to simulate normalization in a term rewriting
+system up to user defined equalities.
+
+
+Printing relations and morphisms
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The ``Print Instances`` command can be used to show the list of currently
+registered ``Reflexive`` (using ``Print Instances Reflexive``), ``Symmetric``
+or ``Transitive`` relations, Equivalences, PreOrders, PERs, and Morphisms
+(implemented as ``Proper`` instances). When the rewriting tactics refuse
+to replace a term in a context because the latter is not a composition
+of morphisms, the ``Print Instances`` commands can be useful to understand
+what additional morphisms should be registered.
+
+
+Deprecated syntax and backward incompatibilities
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Due to backward compatibility reasons, the following syntax for the
+declaration of setoids and morphisms is also accepted.
+
+.. tacv:: Add Setoid @A @Aeq @ST as @ident
+
+where ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier
+and ``ST`` is an object of type (``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.
+
+.. cmd:: Add Morphism f : @ident.
+
+The latter command also 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. As discussed in the next section, the semantics of the
+new ``setoid_rewrite`` command differs slightly from the old one and
+``rewrite``.
+
+
+Extensions
+----------
+
+
+Rewriting under binders
+~~~~~~~~~~~~~~~~~~~~~~~
+
+warning:: Due to compatibility issues, this feature is enabled only
+when calling the ``setoid_rewrite`` tactics directly and not ``rewrite``.
+
+To be able to rewrite under binding constructs, one must declare
+morphisms with respect to pointwise (setoid) equivalence of functions.
+Example of such morphisms are the standard ``all`` and ``ex`` combinators for
+universal and existential quantification respectively. They are
+declared as morphisms in the ``Classes.Morphisms_Prop`` module. For
+example, to declare that universal quantification is a morphism for
+logical equivalence:
+
+.. coqtop:: in
+
+   Instance all_iff_morphism (A : Type) :
+            Proper (pointwise_relation A iff ==> iff) (@all A).
+
+.. coqtop:: all
+
+   Proof. simpl_relation.
+
+One then has to show that if two predicates are equivalent at every
+point, their universal quantifications are equivalent. Once we have
+declared such a morphism, it will be used by the setoid rewriting
+tactic each time we try to rewrite under an ``all`` application (products
+in ``Prop`` are implicitly translated to such applications).
+
+Indeed, when rewriting under a lambda, binding variable ``x``, say from ``P x``
+to ``Q x`` using the relation iff, the tactic will generate a proof of
+``pointwise_relation A iff (fun x => P x) (fun x => Q x)`` from the proof
+of ``iff (P x) (Q x)`` and a constraint of the form Proper
+``(pointwise_relation A iff ==> ?) m`` will be generated for the
+surrounding morphism ``m``.
+
+Hence, one can add higher-order combinators as morphisms by providing
+signatures using pointwise extension for the relations on the
+functional arguments (or whatever subrelation of the pointwise
+extension). For example, one could declare the ``map`` combinator on lists
+as a morphism:
+
+.. coqtop:: in
+
+   Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} :
+            Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B).
+
+where ``list_equiv`` implements an equivalence on lists parameterized by
+an equivalence on the elements.
+
+Note that when one does rewriting with a lemma under a binder using
+``setoid_rewrite``, the application of the lemma may capture the bound
+variable, as the semantics are different from rewrite where the lemma
+is first matched on the whole term. With the new ``setoid_rewrite``,
+matching is done on each subterm separately and in its local
+environment, and all matches are rewritten *simultaneously* by
+default. The semantics of the previous ``setoid_rewrite`` implementation
+can almost be recovered using the ``at 1`` modifier.
+
+
+Sub-relations
+~~~~~~~~~~~~~
+
+Sub-relations can be used to specify that one relation is included in
+another, so that morphisms signatures for one can be used for the
+other. If a signature mentions a relation ``R`` on the left of an
+arrow ``==>``, then the signature also applies for any relation ``S`` that is
+smaller than ``R``, and the inverse applies on the right of an arrow. One
+can then declare only a few morphisms instances that generate the
+complete set of signatures for a particular constant. By default, the
+only declared subrelation is ``iff``, which is a subrelation of ``impl`` and
+``inverse impl`` (the dual of implication). That’s why we can declare only
+two morphisms for conjunction: ``Proper (impl ==> impl ==> impl) and`` and
+``Proper (iff ==> iff ==> iff) and``. This is sufficient to satisfy any
+rewriting constraints arising from a rewrite using ``iff``, ``impl`` or
+``inverse impl`` through ``and``.
+
+Sub-relations are implemented in ``Classes.Morphisms`` and are a prime
+example of a mostly user-space extension of the algorithm.
+
+
+Constant unfolding
+~~~~~~~~~~~~~~~~~~
+
+The resolution tactic is based on type classes and hence regards user-
+defined constants as transparent by default. This may slow down the
+resolution due to a lot of unifications (all the declared ``Proper``
+instances are tried at each node of the search tree). To speed it up,
+declare your constant as rigid for proof search using the command
+``Typeclasses Opaque`` (see :ref:`TODO-20.6.7-typeclasses-transparency`).
+
+
+Strategies for rewriting
+------------------------
+
+
+Definitions
+~~~~~~~~~~~
+
+The generalized rewriting tactic is based on a set of strategies that
+can be combined to obtain custom rewriting procedures. Its set of
+strategies is based on Elan’s rewriting strategies :ref:`TODO-102-biblio`. Rewriting
+strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a
+strategy expression. Strategies are defined inductively as described
+by the following grammar:
+
+.. productionlist:: rewriting
+   s, t, u : `strategy`
+           : | `lemma`
+           : | `lemma_right_to_left`
+           : | `failure`
+           : | `identity`
+           : | `reflexivity`
+           : | `progress`
+           : | `failure_catch`
+           : | `composition`
+           : | `left_biased_choice`
+           : | `iteration_one_or_more`
+           : | `iteration_zero_or_more`
+           : | `one_subterm`
+           : | `all_subterms`
+           : | `innermost_first`
+           : | `outermost_first`
+           : | `bottom_up`
+           : | `top_down`
+           : | `apply_hint`
+           : | `any_of_the_terms`
+           : | `apply_reduction`
+           : | `fold_expression`
+
+.. productionlist:: rewriting
+   strategy : "(" `s` ")"
+   lemma : `c`
+   lemma_right_to_left : "<-" `c`
+   failure : `fail`
+   identity : `id`
+   reflexivity : `refl`
+   progress : `progress` `s`
+   failure_catch : `try` `s`
+   composition : `s` ";" `u`
+   left_biased_choice : choice `s` `t`
+   iteration_one_or_more : `repeat` `s`
+   iteration_zero_or_more : `any` `s`
+   one_subterm : subterm `s`
+   all_subterms : subterms `s`
+   innermost_first : `innermost` `s`
+   outermost_first : `outermost` `s`
+   bottom_up : `bottomup` `s`
+   top_down : `topdown` `s`
+   apply_hint : hints `hintdb`
+   any_of_the_terms : terms (`c`)+
+   apply_reduction : eval `redexpr`
+   fold_expression : fold `c`
+
+
+Actually a few of these are defined in term of the others using a
+primitive fixpoint operator:
+
+.. productionlist:: rewriting
+   try `s` : choice `s` `id`
+   any `s` : fix `u`. try (`s` ; `u`)
+   repeat `s` : `s` ; `any` `s`
+   bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu
+   topdown s : fix `td`. (choice s (progress (subterms td))) ; try td
+   innermost s : fix `i`. (choice (subterm i) s)
+   outermost s : fix `o`. (choice s (subterm o))
+
+The basic control strategy semantics are straightforward: strategies
+are applied to subterms of the term to rewrite, starting from the root
+of the term. The lemma strategies unify the left-hand-side of the
+lemma with the current subterm and on success rewrite it to the right-
+hand-side. Composition can be used to continue rewriting on the
+current subterm. The fail strategy always fails while the identity
+strategy succeeds without making progress. The reflexivity strategy
+succeeds, making progress using a reflexivity proof of rewriting.
+Progress tests progress of the argument strategy and fails if no
+progress was made, while ``try`` always succeeds, catching failures.
+Choice is left-biased: it will launch the first strategy and fall back
+on the second one in case of failure. One can iterate a strategy at
+least 1 time using ``repeat`` and at least 0 times using ``any``.
+
+The ``subterm`` and ``subterms`` strategies apply their argument strategy ``s`` to
+respectively one or all subterms of the current term under
+consideration, left-to-right. ``subterm`` stops at the first subterm for
+which ``s`` made progress. The composite strategies ``innermost`` and ``outermost``
+perform a single innermost or outermost rewrite using their argument
+strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many
+rewritings as possible, starting from the bottom or the top of the
+term.
+
+Hint databases created for ``autorewrite`` can also be used
+by ``rewrite_strat`` using the ``hints`` strategy that applies any of the
+lemmas at the current subterm. The ``terms`` strategy takes the lemma
+names directly as arguments. The ``eval`` strategy expects a reduction
+expression (see :ref:`TODO-8.7-performing-computations`) and succeeds
+if it reduces the subterm under consideration. The ``fold`` strategy takes
+a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c``
+on success, it is stronger than the tactic ``fold``.
+
+
+Usage
+~~~~~
+
+
+.. tacv:: rewrite_strat @s [in @ident]
+
+   Rewrite using the strategy s in hypothesis ident or the conclusion.
+
+   .. exn:: Nothing to rewrite.
+
+      If the strategy failed.
+
+   .. exn:: No progress made.
+
+      If the strategy succeeded but made no progress.
+
+   .. exn:: Unable to satisfy the rewriting constraints.
+
+      If the strategy succeeded and made progress but the
+      corresponding rewriting constraints are not satisfied.
+
+
+   The ``setoid_rewrite c`` tactic is basically equivalent to
+   ``rewrite_strat (outermost c)``.
+
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 0757e5095..75e955136 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -53,6 +53,7 @@ Table of contents
    addendum/program
    addendum/ring
    addendum/nsatz
+   addendum/generalized-rewriting
 
 .. toctree::
    :caption: Reference