[Sphinx] Add chapter 18

Thanks to Pierre Letouzey for porting this chapter.

1 files changed, 416 insertions, 510 deletions

diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 9862a9b30..f5ca5be44 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -1,563 +1,469 @@
-\achapter{Implicit Coercions}
-%HEVEA\cutname{coercions.html}
-\aauthor{Amokrane Saïbi}
+.. _implicitcoercions:
 
-\label{Coercions-full}
-\index{Coercions!presentation}
+.. include:: ../replaces.rst
 
-\asection{General Presentation}
+Implicit Coercions
+====================
 
-This section describes the inheritance mechanism of {\Coq}. In {\Coq} with
+:Author: Amokrane Saïbi
+
+General Presentation
+---------------------
+
+This section describes the inheritance mechanism of |Coq|. In |Coq| with
 inheritance, we are not interested in adding any expressive power to
 our theory, but only convenience. Given a term, possibly not typable,
 we are interested in the problem of determining if it can be well
-typed modulo insertion of appropriate coercions.  We allow to write:
-
-\begin{itemize}
-\item $f~a$ where $f:forall~ x:A, B$ and $a:A'$ when $A'$ can 
-      be seen in some sense as a subtype of $A$.
-\item $x:A$ when $A$ is not a type, but can be seen in 
-      a certain sense as a type: set, group, category etc.
-\item $f~a$ when $f$ is not a function, but can be seen in a certain sense
-      as a function: bijection, functor, any structure morphism etc.
-\end{itemize}
-
-\asection{Classes}
-\index{Coercions!classes}
- A class with $n$ parameters is any defined name with a type
-$forall~ (x_1:A_1)..(x_n:A_n), s$ where $s$ is a sort.  Thus a class with
+typed modulo insertion of appropriate coercions. We allow to write:
+
+ * :g:`f a` where :g:`f:(forall x:A,B)` and :g:`a:A'` when ``A'`` can
+   be seen in some sense as a subtype of ``A``.
+ * :g:`x:A` when ``A`` is not a type, but can be seen in
+   a certain sense as a type: set, group, category etc.
+ * :g:`f a` when ``f`` is not a function, but can be seen in a certain sense
+   as a function: bijection, functor, any structure morphism etc.
+
+
+Classes
+-------
+
+A class with `n` parameters is any defined name with a type
+:g:`forall (x₁:A₁)..(xₙ:Aₙ),s` where ``s`` is a sort.  Thus a class with
 parameters is considered as a single class and not as a family of
-classes.  An object of a class $C$ is any term of type $C~t_1
-.. t_n$.  In addition to these user-classes, we have two abstract
-classes:
-
-\begin{itemize}
-\item {\tt Sortclass}, the class of sorts; 
-  its objects are the terms whose type is a sort (e.g., \texttt{Prop}
-  or \texttt{Type}).
-\item {\tt Funclass}, the class of functions; 
-  its objects are all the terms with a functional 
-  type, i.e. of form $forall~ x:A, B$.
-\end{itemize}
-
-Formally, the syntax of a classes is defined on Figure~\ref{fig:classes}.
-\begin{figure}
-\begin{centerframe}
-\begin{tabular}{lcl}
-{\class} & ::= & {\qualid} \\
-  & $|$ & {\tt Sortclass} \\
-  & $|$ & {\tt Funclass} 
-\end{tabular}
-\end{centerframe}
-\caption{Syntax of classes}
-\label{fig:classes}
-\end{figure}
-
-\asection{Coercions}
-\index{Coercions!Funclass}
-\index{Coercions!Sortclass}
-  A name $f$ can be declared as a coercion between a source user-class
-$C$ with $n$ parameters and a target class $D$ if one of these
+classes.  An object of a class ``C`` is any term of type :g:`C t₁ .. tₙ`.
+In addition to these user-classes, we have two abstract classes:
+
+
+  * ``Sortclass``, the class of sorts; its objects are the terms whose type is a
+    sort (e.g. :g:`Prop` or :g:`Type`).
+  * ``Funclass``, the class of functions; its objects are all the terms with a functional
+    type, i.e. of form :g:`forall x:A,B`.
+
+Formally, the syntax of a classes is defined as:
+
+.. productionlist::
+   class: qualid
+        : | `Sortclass`
+        : | `Funclass`
+
+
+Coercions
+---------
+
+A name ``f`` can be declared as a coercion between a source user-class
+``C`` with `n` parameters and a target class ``D`` if one of these
 conditions holds:
 
-\newcommand{\oftype}{\!:\!}
-
-\begin{itemize}
-\item $D$ is a user-class, then the type of $f$ must have the form
-      $forall~ (x_1 \oftype A_1)..(x_n \oftype A_n)(y\oftype C~x_1..x_n), D~u_1..u_m$ where $m$
-      is the number of parameters of $D$.
-\item $D$ is {\tt Funclass}, then the type of $f$ must have the form
-      $forall~ (x_1\oftype A_1)..(x_n\oftype A_n)(y\oftype C~x_1..x_n)(x:A), B$. 
-\item $D$ is {\tt Sortclass}, then the type of $f$ must have the form
-      $forall~ (x_1\oftype A_1)..(x_n\oftype A_n)(y\oftype C~x_1..x_n), s$ with $s$ a sort. 
-\end{itemize}
-
-We then write $f:C \mbox{\texttt{>->}} D$. The restriction on the type
-of coercions is called {\em the uniform inheritance condition}.
-Remark: the abstract class {\tt Sortclass} can be used as source class,
-but the abstract class {\tt Funclass} cannot.
-
-To coerce an object $t:C~t_1..t_n$ of $C$ towards $D$, we have to
-apply the coercion $f$ to it; the obtained term $f~t_1..t_n~t$ is
-then an object of $D$.
-
-\asection{Identity Coercions}
-\index{Coercions!identity}
-
-  Identity coercions are special cases of coercions used to go around
-the uniform inheritance condition.  Let $C$ and $D$ be two classes
-with respectively $n$ and $m$ parameters and
-$f:forall~(x_1:T_1)..(x_k:T_k)(y:C~u_1..u_n), D~v_1..v_m$ a function which
-does not verify the uniform inheritance condition. To declare $f$ as
-coercion, one has first to declare a subclass $C'$ of $C$:
-
-$$C' := fun~ (x_1:T_1)..(x_k:T_k) => C~u_1..u_n$$
-
-\noindent We then define an {\em identity coercion} between $C'$ and $C$:
-\begin{eqnarray*}
-Id\_C'\_C  & := & fun~ (x_1:T_1)..(x_k:T_k)(y:C'~x_1..x_k) => (y:C~u_1..u_n)\\
-\end{eqnarray*}
-
-We can now declare $f$ as coercion from $C'$ to $D$, since we can
-``cast'' its type as
-$forall~ (x_1:T_1)..(x_k:T_k)(y:C'~x_1..x_k),D~v_1..v_m$.\\ The identity
-coercions have a special status: to coerce an object $t:C'~t_1..t_k$
-of $C'$ towards $C$, we does not have to insert explicitly $Id\_C'\_C$
-since $Id\_C'\_C~t_1..t_k~t$ is convertible with $t$.  However we
-``rewrite'' the type of $t$ to become an object of $C$; in this case,
-it becomes $C~u_1^*..u_k^*$ where each $u_i^*$ is the result of the
-substitution in $u_i$ of the variables $x_j$ by $t_j$.
-
-
-\asection{Inheritance Graph}
-\index{Coercions!inheritance graph}
+ * ``D`` is a user-class, then the type of ``f`` must have the form
+   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where `m`
+   is the number of parameters of ``D``.
+ * ``D`` is ``Funclass``, then the type of ``f`` must have the form
+   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ)(x:A), B`.
+ * ``D`` is ``Sortclass``, then the type of ``f`` must have the form
+   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), s` with ``s`` a sort.
+
+We then write :g:`f : C >-> D`. The restriction on the type
+of coercions is called *the uniform inheritance condition*.
+
+.. note:: The abstract classe ``Sortclass`` can be used as a source class, but
+          the abstract class ``Funclass`` cannot.
+
+To coerce an object :g:`t:C t₁..tₙ` of ``C`` towards ``D``, we have to
+apply the coercion ``f`` to it; the obtained term :g:`f t₁..tₙ t` is
+then an object of ``D``.
+
+
+Identity Coercions
+-------------------
+
+Identity coercions are special cases of coercions used to go around
+the uniform inheritance condition. Let ``C`` and ``D`` be two classes
+with respectively `n` and `m` parameters and
+:g:`f:forall (x₁:T₁)..(xₖ:Tₖ)(y:C u₁..uₙ), D v₁..vₘ` a function which
+does not verify the uniform inheritance condition. To declare ``f`` as
+coercion, one has first to declare a subclass ``C'`` of ``C``:
+
+  :g:`C' := fun (x₁:T₁)..(xₖ:Tₖ) => C u₁..uₙ`
+
+We then define an *identity coercion* between ``C'`` and ``C``:
+
+  :g:`Id_C'_C  := fun (x₁:T₁)..(xₖ:Tₖ)(y:C' x₁..xₖ) => (y:C u₁..uₙ)`
+
+We can now declare ``f`` as coercion from ``C'`` to ``D``, since we can
+"cast" its type as
+:g:`forall (x₁:T₁)..(xₖ:Tₖ)(y:C' x₁..xₖ),D v₁..vₘ`.
+
+The identity coercions have a special status: to coerce an object
+:g:`t:C' t₁..tₖ`
+of ``C'`` towards ``C``, we does not have to insert explicitly ``Id_C'_C``
+since :g:`Id_C'_C t₁..tₖ t` is convertible with ``t``.  However we
+"rewrite" the type of ``t`` to become an object of ``C``; in this case,
+it becomes :g:`C uₙ'..uₖ'` where each ``uᵢ'`` is the result of the
+substitution in ``uᵢ`` of the variables ``xⱼ`` by ``tⱼ``.
+
+Inheritance Graph
+------------------
+
 Coercions form an inheritance graph with classes as nodes.  We call
-{\em coercion path} an ordered list of coercions between two nodes of
-the graph.  A class $C$ is said to be a subclass of $D$ if there is a
-coercion path in the graph from $C$ to $D$; we also say that $C$
-inherits from $D$. Our mechanism supports multiple inheritance since a
+*coercion path* an ordered list of coercions between two nodes of
+the graph.  A class ``C`` is said to be a subclass of ``D`` if there is a
+coercion path in the graph from ``C`` to ``D``; we also say that ``C``
+inherits from ``D``. Our mechanism supports multiple inheritance since a
 class may inherit from several classes, contrary to simple inheritance
 where a class inherits from at most one class.  However there must be
-at most one path between two classes.  If this is not the case, only
-the {\em oldest} one is valid and the others are ignored. So the order
+at most one path between two classes. If this is not the case, only
+the *oldest* one is valid and the others are ignored. So the order
 of declaration of coercions is important.
 
 We extend notations for coercions to coercion paths. For instance
-$[f_1;..;f_k]:C \mbox{\texttt{>->}} D$ is the coercion path composed
-by the coercions $f_1..f_k$.  The application of a coercion path to a
+:g:`[f₁;..;fₖ] : C >-> D` is the coercion path composed
+by the coercions ``f₁..fₖ``.  The application of a coercion path to a
 term consists of the successive application of its coercions.
 
-\asection{Declaration of Coercions}
-
-%%%%% "Class" is useless, since classes are implicitely defined via coercions.
-
-% \asubsection{\tt Class {\qualid}.}\comindex{Class}
-% Declares {\qualid} as a new class.
-
-% \begin{ErrMsgs}
-% \item {\qualid} \errindex{not declared}
-% \item {\qualid} \errindex{is already a class}
-% \item \errindex{Type of {\qualid} does not end with a sort}
-% \end{ErrMsgs}
-
-% \begin{Variant}
-% \item {\tt Class Local {\qualid}.} \\
-% Declares the construction denoted by {\qualid} as a new local class to 
-% the current section.
-% \end{Variant}
-
-% END "Class" is useless
-
-\asubsection{\tt Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.}
-\comindex{Coercion}
-
-Declares the construction denoted by {\qualid} as a coercion between
-{\class$_1$} and {\class$_2$}.
-
-% Useless information
-% The classes {\class$_1$} and {\class$_2$} are first declared if necessary.
-   
-\begin{ErrMsgs}
-\item {\qualid} \errindex{not declared}
-\item {\qualid} \errindex{is already a coercion}
-\item \errindex{Funclass cannot be a source class}
-\item {\qualid} \errindex{is not a function}
-\item \errindex{Cannot find the source class of {\qualid}}
-\item \errindex{Cannot recognize {\class$_1$} as a source class of {\qualid}}
-\item {\qualid} \errindex{does not respect the uniform inheritance condition}
-\item \errindex{Found target class {\class} instead of {\class$_2$}}
-
-\end{ErrMsgs}
-
-When the coercion {\qualid} is added to the inheritance graph, non
-valid coercion paths are ignored; they are signaled by a warning.
-\\[0.3cm]
-\noindent {\bf Warning :}
-\begin{enumerate}
-\item \begin{tabbing}
-{\tt Ambiguous paths: }\= $[f_1^1;..;f_{n_1}^1] : C_1\mbox{\tt >->}D_1$\\
-                       \> {\ldots} \\
-                       \>$[f_1^m;..;f_{n_m}^m] : C_m\mbox{\tt >->}D_m$
-      \end{tabbing}
-\end{enumerate}
-
-\begin{Variants}
-\item {\tt Local Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.}
-\comindex{Local Coercion}\\
-  Declares the construction denoted by {\qualid} as a coercion local to
-  the current section.
-
-\item {\tt Coercion {\ident} := {\term}}\comindex{Coercion}\\
-  This defines {\ident} just like \texttt{Definition {\ident} :=
-    {\term}}, and then declares {\ident} as a coercion between it
-  source and its target.
-
-\item {\tt Coercion {\ident} := {\term} : {\type}}\\
-  This defines {\ident} just like 
-  \texttt{Definition {\ident} : {\type} := {\term}}, and then
-  declares {\ident} as a coercion between it source and its target. 
-
-\item {\tt Local Coercion {\ident} := {\term}}\comindex{Local Coercion}\\
-  This defines {\ident} just like \texttt{Let {\ident} :=
-    {\term}}, and then declares {\ident} as a coercion between it
-  source and its target.
-
-\item Assumptions can be declared as coercions at declaration
-time. This extends the grammar of assumptions from 
-Figure~\ref{sentences-syntax} as follows:
-\comindex{Variable \mbox{\rm (and coercions)}}
-\comindex{Axiom \mbox{\rm (and coercions)}}
-\comindex{Parameter \mbox{\rm (and coercions)}}
-\comindex{Hypothesis \mbox{\rm (and coercions)}}
-
-\begin{tabular}{lcl}
-%% Declarations
-{\assumption} & ::= & {\assumptionkeyword} {\assums} {\tt .} \\
-&&\\
-{\assums} & ::= & {\simpleassums} \\
-          & $|$ & \nelist{{\tt (} \simpleassums {\tt )}}{} \\
-&&\\
-{\simpleassums} & ::= &  \nelist{\ident}{} {\tt :}\zeroone{{\tt >}} {\term}\\  
-\end{tabular}
-
-If the extra {\tt >} is present before the type of some assumptions, these
+
+Declaration of Coercions
+-------------------------
+
+.. cmd:: Coercion @qualid : @class >-> @class.
+
+  Declares the construction denoted by `qualid` as a coercion between
+  the two given classes.
+
+  .. exn:: @qualid not declared
+  .. exn:: @qualid is already a coercion
+  .. exn:: Funclass cannot be a source class
+  .. exn:: @qualid is not a function
+  .. exn:: Cannot find the source class of @qualid
+  .. exn:: Cannot recognize @class as a source class of @qualid
+  .. exn:: @qualid does not respect the uniform inheritance condition
+  .. exn:: Found target class ... instead of ...
+
+  .. warn:: Ambigous path:
+
+    When the coercion `qualid` is added to the inheritance graph, non
+    valid coercion paths are ignored; they are signaled by a warning
+    displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
+
+  .. cmdv:: Local Coercion @qualid : @class >-> @class.
+
+    Declares the construction denoted by `qualid` as a coercion local to
+    the current section.
+
+  .. cmdv:: Coercion @ident := @term.
+
+    This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
+    and then declares `ident` as a coercion between it source and its target.
+
+  .. cmdv:: Coercion @ident := @term : @type.
+
+    This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
+    and then declares `ident` as a coercion between it source and its target.
+
+  .. cmdv:: Local Coercion @ident := @term.
+
+    This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
+    and then declares `ident` as a coercion between it source and its target.
+
+Assumptions can be declared as coercions at declaration time.
+This extends the grammar of assumptions from
+Figure :ref:`TODO-1.3-sentences-syntax` as follows:
+
+..
+  FIXME:
+   \comindex{Variable \mbox{\rm (and coercions)}}
+   \comindex{Axiom \mbox{\rm (and coercions)}}
+   \comindex{Parameter \mbox{\rm (and coercions)}}
+   \comindex{Hypothesis \mbox{\rm (and coercions)}}
+
+.. productionlist::
+   assumption : assumption_keyword assums .
+   assums : simple_assums
+          : | (simple_assums) ... (simple_assums)
+   simple_assums : ident ... ident :[>] term
+
+If the extra ``>`` is present before the type of some assumptions, these
 assumptions are declared as coercions.
 
-\item Constructors of inductive types can be declared as coercions at
+Similarly, constructors of inductive types can be declared as coercions at
 definition time of the inductive type. This extends and modifies the
-grammar of inductive types from Figure \ref{sentences-syntax} as follows: 
-\comindex{Inductive \mbox{\rm (and coercions)}}
-\comindex{CoInductive \mbox{\rm (and coercions)}}
-
-\begin{center}
-\begin{tabular}{lcl}
-%% Inductives
-{\inductive} & ::= & 
-           {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\
- & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\
-           & & \\
-{\inductivebody} & ::= & 
-  {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\
-   && ~~~\zeroone{\zeroone{\tt |} \nelist{\constructor}{|}} \\
-           & & \\
-{\constructor} & ::= &  {\ident} \zeroone{\binders} \zeroone{{\tt :}\zeroone{\tt >} {\term}} \\
-\end{tabular}
-\end{center}
-
-Especially, if the extra {\tt >} is present in a constructor
+grammar of inductive types from Figure :ref:`TODO-1.3-sentences-syntax` as follows:
+
+..
+  FIXME:
+   \comindex{Inductive \mbox{\rm (and coercions)}}
+   \comindex{CoInductive \mbox{\rm (and coercions)}}
+
+.. productionlist::
+   inductive : `Inductive` ind_body `with` ... `with` ind_body
+             : | `CoInductive` ind_body `with` ... `with` ind_body
+   ind_body : ident [binders] : term := [[|] constructor | ... | constructor]
+   constructor : ident [binders] [:[>] term]
+
+Especially, if the extra ``>`` is present in a constructor
 declaration, this constructor is declared as a coercion.
-\end{Variants}
-
-\asubsection{\tt Identity Coercion {\ident}:{\class$_1$} >-> {\class$_2$}.} 
-\comindex{Identity Coercion}
-
-We check that {\class$_1$} is a constant with a value of the form
-$fun~ (x_1:T_1)..(x_n:T_n) => (\mbox{\class}_2~t_1..t_m)$ where $m$ is the
-number of parameters of \class$_2$.  Then we define an identity
-function with the type
-$forall~ (x_1:T_1)..(x_n:T_n)(y:\mbox{\class}_1~x_1..x_n),
-{\mbox{\class}_2}~t_1..t_m$, and we declare it as an identity
-coercion between {\class$_1$} and {\class$_2$}.
-
-\begin{ErrMsgs}
-\item {\class$_1$} \errindex{must be a transparent constant} 
-\end{ErrMsgs}
-
-\begin{Variants}
-\item {\tt Local Identity Coercion {\ident}:{\ident$_1$} >-> {\ident$_2$}.} \\
-Idem but locally to the current section.
-
-\item {\tt SubClass {\ident} := {\type}.} \\
-\comindex{SubClass}
- If {\type} is a class
-{\ident'} applied to some arguments then {\ident} is defined and an
-identity coercion of name {\tt Id\_{\ident}\_{\ident'}} is
-declared. Otherwise said, this is an abbreviation for 
-
-{\tt Definition {\ident} := {\type}.} 
-
- followed by
-
-{\tt Identity Coercion Id\_{\ident}\_{\ident'}:{\ident} >-> {\ident'}}.
-
-\item {\tt Local SubClass {\ident} := {\type}.} \\
-Same as before but locally to the current section.
-
-\end{Variants}
-
-\asection{Displaying Available Coercions}
-
-\asubsection{\tt Print Classes.} 
-\comindex{Print Classes}
-Print the list of declared classes in the current context.
-
-\asubsection{\tt Print Coercions.}
-\comindex{Print Coercions}
-Print the list of declared coercions in the current context.
-
-\asubsection{\tt Print Graph.} 
-\comindex{Print Graph}
-Print the list of valid coercion paths in the current context.
-
-\asubsection{\tt Print Coercion Paths {\class$_1$} {\class$_2$}.} 
-\comindex{Print Coercion Paths}
-Print the list of valid coercion paths from {\class$_1$} to {\class$_2$}.
-
-\asection{Activating the Printing of Coercions}
-
-\asubsection{\tt Set Printing Coercions.}
-\optindex{Printing Coercions}
-
-This command forces all the coercions to be printed.
-Conversely, to skip the printing of coercions, use
- {\tt Unset Printing Coercions}.
-By default, coercions are not printed.
-
-\asubsection{\tt Add Printing Coercion {\qualid}.}
-\comindex{Add Printing Coercion}
-\comindex{Remove Printing Coercion}
-
-This command forces coercion denoted by {\qualid} to be printed.
-To skip the printing of coercion {\qualid}, use
- {\tt Remove Printing Coercion {\qualid}}.
-By default, a coercion is never printed.
- 
-\asection{Classes as Records}
-\label{Coercions-and-records}
-\index{Coercions!and records}
-We allow the definition of {\em Structures with Inheritance} (or
-classes as records) by extending the existing {\tt Record} macro
-(see Section~\ref{Record}). Its new syntax is:
-
-\begin{center}
-\begin{tabular}{l}
-{\tt Record \zeroone{>}~{\ident} \zeroone{\binders} : {\sort} := \zeroone{\ident$_0$} \verb+{+} \\
-~~~~\begin{tabular}{l}
-        {\tt \ident$_1$ $[$:$|$:>$]$ \term$_1$ ;} \\
-        ... \\
-        {\tt \ident$_n$ $[$:$|$:>$]$ \term$_n$ \verb+}+. }
-    \end{tabular}
-\end{tabular}
-\end{center}
-The identifier {\ident} is the name of the defined record and {\sort}
-is its type. The identifier {\ident$_0$} is the name of its
-constructor. The identifiers {\ident$_1$}, .., {\ident$_n$} are the
-names of its fields and {\term$_1$}, .., {\term$_n$} their respective
-types. The alternative {\tt $[$:$|$:>$]$} is ``{\tt :}'' or ``{\tt
-:>}''. If {\tt {\ident$_i$}:>{\term$_i$}}, then {\ident$_i$} is
-automatically declared as coercion from {\ident} to the class of
-{\term$_i$}.  Remark that {\ident$_i$} always verifies the uniform
-inheritance condition.  If the optional ``{\tt >}'' before {\ident} is
-present, then {\ident$_0$} (or the default name {\tt Build\_{\ident}}
-if {\ident$_0$} is omitted) is automatically declared as a coercion
-from the class of {\term$_n$} to {\ident} (this may fail if the
-uniform inheritance condition is not satisfied).
-
-\Rem The keyword {\tt Structure}\comindex{Structure} is a synonym of {\tt
-Record}.
-
-\asection{Coercions and Sections}
-\index{Coercions!and sections}
-  The inheritance mechanism is compatible with the section
+
+.. cmd:: Identity Coercion @ident : @class >-> @class.
+
+  If ``C`` is the source `class` and ``D`` the destination, we check
+  that ``C`` is a constant with a body of the form
+  :g:`fun (x₁:T₁)..(xₙ:Tₙ) => D t₁..tₘ` where `m` is the
+  number of parameters of ``D``.  Then we define an identity
+  function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`,
+  and we declare it as an identity coercion between ``C`` and ``D``.
+
+  .. exn:: @class must be a transparent constant
+
+  .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident.
+
+    Idem but locally to the current section.
+
+  .. cmdv:: SubClass @ident := @type.
+
+    If `type` is a class `ident'` applied to some arguments then
+    `ident` is defined and an identity coercion of name
+    `Id_ident_ident'` is
+    declared. Otherwise said, this is an abbreviation for
+
+      ``Definition`` `ident` ``:=`` `type`.
+
+      ``Identity Coercion`` `Id_ident_ident'` : `ident` ``>->`` `ident'`.
+
+  .. cmdv:: Local SubClass @ident := @type.
+
+    Same as before but locally to the current section.
+
+
+Displaying Available Coercions
+-------------------------------
+
+.. cmd:: Print Classes.
+
+  Print the list of declared classes in the current context.
+
+.. cmd:: Print Coercions.
+
+  Print the list of declared coercions in the current context.
+
+.. cmd:: Print Graph.
+
+  Print the list of valid coercion paths in the current context.
+
+.. cmd:: Print Coercion Paths @class @class.
+
+  Print the list of valid coercion paths between the two given classes.
+
+Activating the Printing of Coercions
+-------------------------------------
+
+.. cmd:: Set Printing Coercions.
+
+  This command forces all the coercions to be printed.
+  Conversely, to skip the printing of coercions, use
+  ``Unset Printing Coercions``. By default, coercions are not printed.
+
+.. cmd:: Add Printing Coercion @qualid.
+
+  This command forces coercion denoted by `qualid` to be printed.
+  To skip the printing of coercion `qualid`, use
+  ``Remove Printing Coercion`` `qualid`. By default, a coercion is never printed.
+
+
+Classes as Records
+------------------
+
+We allow the definition of *Structures with Inheritance* (or
+classes as records) by extending the existing ``Record`` macro
+(see Section :ref:`TODO-2.1-Record`). Its new syntax is:
+
+.. cmd:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }.
+
+  The first identifier `ident` is the name of the defined record and
+  `sort` is its type. The optional identifier after ``:=`` is the name
+  of the constuctor (it will be ``Build_``\ `ident` if not given).
+  The other identifiers are the names of the fields, and the `term`
+  are their respective types. If ``:>`` is used instead of ``:`` in
+  the declaration of a field, then the name of this field is automatically
+  declared as a coercion from the record name to the class of this
+  field type. Remark that the fields always verify the uniform
+  inheritance condition. If the optional ``>`` is given before the
+  record name, then the constructor name is automatically declared as
+  a coercion from the class of the last field type to the record name
+  (this may fail if the uniform inheritance condition is not
+  satisfied).
+
+.. note::
+
+  The keyword ``Structure`` is a synonym of ``Record``.
+
+..
+  FIXME: \comindex{Structure}
+
+
+Coercions and Sections
+----------------------
+
+The inheritance mechanism is compatible with the section
 mechanism. The global classes and coercions defined inside a section
 are redefined after its closing, using their new value and new
 type. The classes and coercions which are local to the section are
 simply forgotten.
-Coercions with a local source class or a local target class, and 
+Coercions with a local source class or a local target class, and
 coercions which do not verify the uniform inheritance condition any longer
 are also forgotten.
 
-\asection{Coercions and Modules}
-\index{Coercions!and modules}
+Coercions and Modules
+--------------------=
 
-From Coq version 8.3, the coercions present in a module are activated
+From |Coq| version 8.3, the coercions present in a module are activated
 only when the module is explicitly imported. Formerly, the coercions
 were activated as soon as the module was required, whatever it was
 imported or not.
 
-To recover the behavior of the versions of Coq prior to 8.3, use the
+To recover the behavior of the versions of |Coq| prior to 8.3, use the
 following command:
 
-\optindex{Automatic Coercions Import}
-\begin{verbatim}
-Set Automatic Coercions Import.
-\end{verbatim}
+.. cmd:: Set Automatic Coercions Import.
+
+To cancel the effect of the option, use instead ``Unset Automatic Coercions Import``.
 
-To cancel the effect of the option, use instead:
 
-\begin{verbatim}
-Unset Automatic Coercions Import.
-\end{verbatim}
+Examples
+--------
 
-\asection{Examples}
+There are three situations:
 
-  There are three situations:
+Coercion at function application
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-\begin{itemize}
-\item $f~a$ is ill-typed where $f:forall~x:A,B$ and $a:A'$. If there is a
-      coercion path between $A'$ and $A$, $f~a$ is transformed into
-      $f~a'$ where $a'$ is the result of the application of this
-      coercion path to $a$.
+:g:`f a` is ill-typed where :g:`f:forall x:A,B` and :g:`a:A'`. If there is a
+coercion path between ``A'`` and ``A``, then :g:`f a` is transformed into
+:g:`f a'` where ``a'`` is the result of the application of this
+coercion path to ``a``.
 
 We first give an example of coercion between atomic inductive types
 
-%\begin{\small}
-\begin{coq_example}
-Definition bool_in_nat (b:bool) := if b then 0 else 1.
-Coercion bool_in_nat : bool >-> nat.
-Check (0 = true).
-Set Printing Coercions.
-Check (0 = true).
-\end{coq_example}
-%\end{small}
+.. coqtop:: all
 
-\begin{coq_eval}
-Unset Printing Coercions.
-\end{coq_eval}
+  Definition bool_in_nat (b:bool) := if b then 0 else 1.
+  Coercion bool_in_nat : bool >-> nat.
+  Check (0 = true).
+  Set Printing Coercions.
+  Check (0 = true).
+  Unset Printing Coercions.
 
-\Warning ``\verb|Check true=O.|'' fails. This is ``normal'' behaviour of
-coercions. To validate \verb|true=O|, the coercion is searched from
-\verb=nat= to \verb=bool=. There is none.
+
+.. warning::
+
+  Note that ``Check true=O`` would fail. This is "normal" behaviour of
+  coercions. To validate ``true=O``, the coercion is searched from
+  ``nat`` to ``bool``. There is none.
 
 We give an example of coercion between classes with parameters.
 
-%\begin{\small}
-\begin{coq_example}
-Parameters
-   (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set).
-Parameter f : forall n:nat, C n -> D (S n) true.
-Coercion f : C >-> D.
-Parameter g : forall (n:nat) (b:bool), D n b -> E b.
-Coercion g : D >-> E.
-Parameter c : C 0.
-Parameter T : E true -> nat.
-Check (T c).
-Set Printing Coercions.
-Check (T c).
-\end{coq_example}
-%\end{small}
-
-\begin{coq_eval}
-Unset Printing Coercions.
-\end{coq_eval}
+.. coqtop:: all
+
+  Parameters (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set).
+  Parameter f : forall n:nat, C n -> D (S n) true.
+  Coercion f : C >-> D.
+  Parameter g : forall (n:nat) (b:bool), D n b -> E b.
+  Coercion g : D >-> E.
+  Parameter c : C 0.
+  Parameter T : E true -> nat.
+  Check (T c).
+  Set Printing Coercions.
+  Check (T c).
+  Unset Printing Coercions.
 
 We give now an example using identity coercions.
 
-%\begin{small}
-\begin{coq_example}
-Definition D' (b:bool) := D 1 b.
-Identity Coercion IdD'D : D' >-> D.
-Print IdD'D.
-Parameter d' : D' true.
-Check (T d').
-Set Printing Coercions.
-Check (T d').
-\end{coq_example}
-%\end{small}
-
-\begin{coq_eval}
-Unset Printing Coercions.
-\end{coq_eval}
-
-
-  In the case of functional arguments, we use the monotonic rule of
-sub-typing.  Approximatively, to coerce $t:forall~x:A, B$ towards
-$forall~x:A',B'$, one have to coerce $A'$ towards $A$ and $B$ towards
-$B'$. An example is given below:
-
-%\begin{small}
-\begin{coq_example}
-Parameters (A B : Set) (h : A -> B).
-Coercion h : A >-> B.
-Parameter U : (A -> E true) -> nat.
-Parameter t : B -> C 0.
-Check (U t).
-Set Printing Coercions.
-Check (U t).
-\end{coq_example}
-%\end{small}
-
-\begin{coq_eval}
-Unset Printing Coercions.
-\end{coq_eval}
-
-  Remark the changes in the result following the modification of the
+.. coqtop:: all
+
+  Definition D' (b:bool) := D 1 b.
+  Identity Coercion IdD'D : D' >-> D.
+  Print IdD'D.
+  Parameter d' : D' true.
+  Check (T d').
+  Set Printing Coercions.
+  Check (T d').
+  Unset Printing Coercions.
+
+
+In the case of functional arguments, we use the monotonic rule of
+sub-typing.  Approximatively, to coerce :g:`t:forall x:A,B` towards
+:g:`forall x:A',B'`, one have to coerce ``A'`` towards ``A`` and ``B``
+towards ``B'``. An example is given below:
+
+.. coqtop:: all
+
+  Parameters (A B : Set) (h : A -> B).
+  Coercion h : A >-> B.
+  Parameter U : (A -> E true) -> nat.
+  Parameter t : B -> C 0.
+  Check (U t).
+  Set Printing Coercions.
+  Check (U t).
+  Unset Printing Coercions.
+
+Remark the changes in the result following the modification of the
 previous example.
 
-%\begin{small}
-\begin{coq_example}
-Parameter U' : (C 0 -> B) -> nat.
-Parameter t' : E true -> A.
-Check (U' t').
-Set Printing Coercions.
-Check (U' t').
-\end{coq_example}
-%\end{small}
-
-\begin{coq_eval}
-Unset Printing Coercions.
-\end{coq_eval}
-
-\item An assumption $x:A$ when $A$ is not a type, is ill-typed.  It is
-      replaced by $x:A'$ where $A'$ is the result of the application
-      to $A$ of the coercion path between the class of $A$ and {\tt
-      Sortclass} if it exists.  This case occurs in the abstraction
-      $fun~ x:A => t$, universal quantification $forall~x:A, B$,
-      global variables and parameters of (co-)inductive definitions
-      and functions. In $forall~x:A, B$, such a coercion path may be
-      applied to $B$ also if necessary.
-
-%\begin{small}
-\begin{coq_example}
-Parameter Graph : Type.
-Parameter Node : Graph -> Type.
-Coercion Node : Graph >-> Sortclass.
-Parameter G : Graph.
-Parameter Arrows : G -> G -> Type.
-Check Arrows.
-Parameter fg : G -> G.
-Check fg.
-Set Printing Coercions.
-Check fg.
-\end{coq_example}
-%\end{small}
-
-\begin{coq_eval}
-Unset Printing Coercions.
-\end{coq_eval}
-
-\item $f~a$ is ill-typed because $f:A$ is not a function. The term
-      $f$ is replaced by the term obtained by applying to $f$ the
-      coercion path between $A$ and {\tt Funclass} if it exists.
-
-%\begin{small}
-\begin{coq_example}
-Parameter bij : Set -> Set -> Set.
-Parameter ap : forall A B:Set, bij A B -> A -> B.
-Coercion ap : bij >-> Funclass.
-Parameter b : bij nat nat.
-Check (b 0).
-Set Printing Coercions.
-Check (b 0).
-\end{coq_example}
-%\end{small}
-
-\begin{coq_eval}
-Unset Printing Coercions.
-\end{coq_eval}
-
-Let us see the resulting graph of this session.
-
-%\begin{small}
-\begin{coq_example}
-Print Graph.
-\end{coq_example}
-%\end{small}
-
-\end{itemize}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
+.. coqtop:: all
+
+  Parameter U' : (C 0 -> B) -> nat.
+  Parameter t' : E true -> A.
+  Check (U' t').
+  Set Printing Coercions.
+  Check (U' t').
+  Unset Printing Coercions.
+
+
+Coercion to a type
+~~~~~~~~~~~~~~~~~~
+
+An assumption ``x:A`` when ``A`` is not a type, is ill-typed.  It is
+replaced by ``x:A'`` where ``A'`` is the result of the application to
+``A`` of the coercion path between the class of ``A`` and
+``Sortclass`` if it exists.  This case occurs in the abstraction
+:g:`fun x:A => t`, universal quantification :g:`forall x:A,B`, global
+variables and parameters of (co-)inductive definitions and
+functions. In :g:`forall x:A,B`, such a coercion path may be applied
+to ``B`` also if necessary.
+
+.. coqtop:: all
+
+  Parameter Graph : Type.
+  Parameter Node : Graph -> Type.
+  Coercion Node : Graph >-> Sortclass.
+  Parameter G : Graph.
+  Parameter Arrows : G -> G -> Type.
+  Check Arrows.
+  Parameter fg : G -> G.
+  Check fg.
+  Set Printing Coercions.
+  Check fg.
+  Unset Printing Coercions.
+
+
+Coercion to a function
+~~~~~~~~~~~~~~~~~~~~~~
+
+``f a`` is ill-typed because ``f:A`` is not a function. The term
+``f`` is replaced by the term obtained by applying to ``f`` the
+coercion path between ``A`` and ``Funclass`` if it exists.
+
+.. coqtop:: all
+
+  Parameter bij : Set -> Set -> Set.
+  Parameter ap : forall A B:Set, bij A B -> A -> B.
+  Coercion ap : bij >-> Funclass.
+  Parameter b : bij nat nat.
+  Check (b 0).
+  Set Printing Coercions.
+  Check (b 0).
+  Unset Printing Coercions.
+
+Let us see the resulting graph after all these examples.
+
+.. coqtop:: all
+
+  Print Graph.