Fix documentation.

1 files changed, 47 insertions, 47 deletions

diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index b1c278ced..a3372c296 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -41,25 +41,25 @@ End EQ.
 We use Coq modules as name spaces.  This allows us to follow the same pattern
 and naming convention for the rest of the chapter.  The base name space
 contains the definitions of the algebraic structure.  To keep the example
-small, the algebraic structure $EQ.type$ we are defining is very simplistic,
+small, the algebraic structure \texttt{EQ.type} we are defining is very simplistic,
 and characterizes terms on which a binary relation is defined, without
 requiring such relation to validate any property.
-The inner $theory$ module contains the overloaded notation $==$ and
+The inner \texttt{theory} module contains the overloaded notation \texttt{==} and
 will eventually contain lemmas holding on all the instances of the
 algebraic structure (in this case there are no lemmas).
 
-Note that in practice the user may want to declare $EQ.obj$ as a coercion,
+Note that in practice the user may want to declare \texttt{EQ.obj} as a coercion,
 but we will not do that here.
 
-The following line tests that, when we assume a type $e$ that is in the
-$EQ$ class, then we can relates two of its objects with $==$.
+The following line tests that, when we assume a type \texttt{e} that is in the
+\texttt{EQ} class, then we can relates two of its objects with \texttt{==}.
 
 \begin{coq_example}
 Import EQ.theory.
 Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
 \end{coq_example}
 
-Still, no concrete type is in the $EQ$ class.  We amend that by equipping $nat$
+Still, no concrete type is in the \texttt{EQ} class.  We amend that by equipping \texttt{nat}
 with a comparison relation.
 
 \begin{coq_example}
@@ -71,23 +71,23 @@ Check 3 == 3.
 Eval compute in 3 == 4.
 \end{coq_example}
 
-This last test shows that Coq is now not only able to typecheck $3==3$, but
-also that the infix relation was bound to the $nat\_eq$ relation.  This
-relation is selected whenever $==$ is used on terms of type $nat$.  This
-can be read in the line declaring the canonical structure $nat\_EQty$,
-where the first argument to $Pack$ is the key and its second argument
+This last test shows that Coq is now not only able to typecheck \texttt{3==3}, but
+also that the infix relation was bound to the \texttt{nat\_eq} relation.  This
+relation is selected whenever \texttt{==} is used on terms of type \texttt{nat}.  This
+can be read in the line declaring the canonical structure \texttt{nat\_EQty},
+where the first argument to \texttt{Pack} is the key and its second argument
 a group of canonical values associated to the key.  In this case we associate
-to $nat$ only one canonical value (since its class, $nat\_EQcl$ has just one
-member).  The use of the projection $op$ requires its argument to be in
-the class $EQ$, and uses such a member (function) to actually compare
+to \texttt{nat} only one canonical value (since its class, \texttt{nat\_EQcl} has just one
+member).  The use of the projection \texttt{op} requires its argument to be in
+the class \texttt{EQ}, and uses such a member (function) to actually compare
 its arguments.
 
 Similarly, we could equip any other type with a comparison relation, and
-use the $==$ notation on terms of this type.
+use the \texttt{==} notation on terms of this type.
 
 \subsection{Derived Canonical Structures}
 
-We know how to use $==$ on base types, like $nat$, $bool$, $Z$.
+We know how to use \texttt{==} on base types, like \texttt{nat}, \texttt{bool}, \texttt{Z}.
 Here we show how to deal with type constructors, i.e. how to make the
 following example work:
 
@@ -109,18 +109,18 @@ Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b).
 Check forall n m : nat, (3,4) == (n,m).
 \end{coq_example}
 
-Thanks to the $pair\_EQty$ declaration, Coq is able to build a comparison
+Thanks to the \texttt{pair\_EQty} declaration, Coq is able to build a comparison
 relation for pairs whenever it is able to build a comparison relation
 for each component of the pair.  The declaration associates to the key
-$*$ (the type constructor of pairs) the canonical comparison relation
-$pair\_eq$ whenever the type constructor $*$ is applied to two types
-being themselves in the $EQ$ class.
+\texttt{*} (the type constructor of pairs) the canonical comparison relation
+\texttt{pair\_eq} whenever the type constructor \texttt{*} is applied to two types
+being themselves in the \texttt{EQ} class.
 
 \section{Hierarchy of structures}
 
 To get to an interesting example we need another base class to be available.
 We choose the class of types that are equipped with an order relation,
-to which we associate the infix $<=$ notation.
+to which we associate the infix \texttt{<=} notation.
 
 \begin{coq_example}
 Module LE.
@@ -136,7 +136,7 @@ Module LE.
 End LE.
 \end{coq_example}
 
-As before we register a canonical $LE$ class for $nat$.
+As before we register a canonical \texttt{LE} class for \texttt{nat}.
 
 \begin{coq_example}
 Import LE.theory.
@@ -145,7 +145,7 @@ Definition nat_LEcl : LE.class nat := LE.Class nat_le.
 Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
 \end{coq_example}
 
-And we enable Coq to relate pair of terms with $<=$.
+And we enable Coq to relate pair of terms with \texttt{<=}.
 
 \begin{coq_example}
 Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) :=
@@ -156,7 +156,7 @@ Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type :=
 Check (3,4,5) <= (3,4,5).
 \end{coq_example}
 
-At the current stage we can use $==$ and $<=$ on concrete types,
+At the current stage we can use \texttt{==} and \texttt{<=} on concrete types,
 like tuples of natural numbers, but we can't develop an algebraic
 theory over the types that are equipped with both relations.
 
@@ -166,7 +166,7 @@ Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
 Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
 \end{coq_example}
 
-We need to define a new class that inherits from both $EQ$ and $LE$.
+We need to define a new class that inherits from both \texttt{EQ} and \texttt{LE}.
 
 \begin{coq_example}
 Module LEQ.
@@ -181,8 +181,8 @@ Module LEQ.
   Arguments Class {T} _ _ _.
 \end{coq_example}
 
-The $mixin$ component of the $LEQ$ class contains all the extra content
-we are adding to $EQ$ and $LE$.  In particular it contains the requirement
+The \texttt{mixin} component of the \texttt{LEQ} class contains all the extra content
+we are adding to \texttt{EQ} and \texttt{LE}.  In particular it contains the requirement
 that the two relations we are combining are compatible.
 
 Unfortunately there is still an obstacle to developing the algebraic theory
@@ -193,12 +193,12 @@ of this new class.
   Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
 \end{coq_example}
 
-The problem is that the two classes $LE$ and $LEQ$ are not yet related by
+The problem is that the two classes \texttt{LE} and \texttt{LEQ} are not yet related by
 a subclass relation.  In other words Coq does not see that an object
-of the $LEQ$ class is also an object of the $LE$ class.
+of the \texttt{LEQ} class is also an object of the \texttt{LE} class.
 
 The following two constructions tell Coq how to canonically build
-the $LE.type$ and $EQ.type$ structure given an $LEQ.type$ structure
+the \texttt{LE.type} and \texttt{EQ.type} structure given an \texttt{LEQ.type} structure
 on the same type.
 
 \begin{coq_example}
@@ -209,7 +209,7 @@ on the same type.
     LE.Pack (obj e) (LE_class _ (class_of e)).
   Canonical Structure to_LE.
 \end{coq_example}
-We can now formulate out first theorem on the objects of the $LEQ$ structure.
+We can now formulate out first theorem on the objects of the \texttt{LEQ} structure.
 \begin{coq_example}
   Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
    now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. Qed.
@@ -231,8 +231,8 @@ Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
  Fail apply (lele_eq n m). Abort.
 \end{coq_example}
 
-Again one has to tell Coq that the type $nat$ is in the $LEQ$ class, and how
-the type constructor $*$ interacts with the $LEQ$ class.  In the following
+Again one has to tell Coq that the type \texttt{nat} is in the \texttt{LEQ} class, and how
+the type constructor \texttt{*} interacts with the \texttt{LEQ} class.  In the following
 proofs are omitted for brevity.
 
 \begin{coq_example}
@@ -271,8 +271,8 @@ Qed.
 Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
 \end{coq_example}
 
-The following script registers an $LEQ$ class for $nat$ and for the
-type constructor $*$.  It also tests that they work as expected.
+The following script registers an \texttt{LEQ} class for \texttt{nat} and for the
+type constructor \texttt{*}.  It also tests that they work as expected.
 
 Unfortunately, these declarations are very verbose.  In the following
 subsection we show how to make these declaration more compact.
@@ -294,9 +294,9 @@ Module Add_instance_attempt.
 End Add_instance_attempt.
 \end{coq_example}
 
-Note that no direct proof of $n <= m -> m <= n -> n == m$ is provided by the
-user for $n$ and $m$ of type $nat * nat$.  What the user provides is a proof of
-this statement for $n$ and $m$ of type $nat$ and a proof that the pair
+Note that no direct proof of \texttt{n <= m -> m <= n -> n == m} is provided by the
+user for \texttt{n} and \texttt{m} of type \texttt{nat * nat}.  What the user provides is a proof of
+this statement for \texttt{n} and \texttt{m} of type \texttt{nat} and a proof that the pair
 constructor preserves this property.  The combination of these two facts is a
 simple form of proof search that Coq performs automatically while inferring
 canonical structures.
@@ -334,7 +334,7 @@ problem, that will in turn require the inference of some canonical
 structures.  They are explained in mode details in~\cite{CSwcu}.
 
 We now have all we need to create a compact ``packager'' to declare
-instances of the $LEQ$ class.
+instances of the \texttt{LEQ} class.
 
 \begin{coq_example}
 Import infrastructure.
@@ -348,17 +348,17 @@ Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=
 Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).
 \end{coq_example}
 
-The object $Pack$ takes a type $T$ (the key) and a mixin $m$.  It infers all
-the other pieces of the class $LEQ$ and declares them as canonical values
-associated to the $T$ key.  All in all, the only new piece of information
-we add in the $LEQ$ class is the mixin, all the rest is already canonical
-for $T$ and hence can be inferred by Coq.
+The object \texttt{Pack} takes a type \texttt{T} (the key) and a mixin \texttt{m}.  It infers all
+the other pieces of the class \texttt{LEQ} and declares them as canonical values
+associated to the \texttt{T} key.  All in all, the only new piece of information
+we add in the \texttt{LEQ} class is the mixin, all the rest is already canonical
+for \texttt{T} and hence can be inferred by Coq.
 
-$Pack$ is a notation, hence it is not type checked at the time of its
+\texttt{Pack} is a notation, hence it is not type checked at the time of its
 declaration.  It will be type checked when it is used, an in that case
-$T$ is going to be a concrete type.  The odd arguments $\_$ and $id$ we
+\texttt{T} is going to be a concrete type.  The odd arguments \texttt{\_} and \texttt{id} we
 pass to the 
-packager represent respectively the classes to be inferred (like $e$, $o$, etc) and a token ($id$) to force their inference.  Again, for all the details the
+packager represent respectively the classes to be inferred (like \texttt{e}, \texttt{o}, etc) and a token (\texttt{id}) to force their inference.  Again, for all the details the
 reader can refer to~\cite{CSwcu}. 
 
 The declaration of canonical instances can now be way more compact: