Merge PR #8160: Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the Reference Manual.

2 files changed, 24 insertions, 24 deletions

diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index 6843e9eaa1..3af3115a59 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -6,14 +6,14 @@ Canonical Structures
 
 :Authors: Assia Mahboubi and Enrico Tassi
 
-This chapter explains the basics of Canonical Structure and how they can be used
+This chapter explains the basics of canonical structures and how they can be used
 to overload notations and build a hierarchy of algebraic structures. The
 examples are taken from :cite:`CSwcu`. We invite the interested reader to refer
 to this paper for all the details that are omitted here for brevity. The
 interested reader shall also find in :cite:`CSlessadhoc` a detailed description
-of another, complementary, use of Canonical Structures: advanced proof search.
+of another, complementary, use of canonical structures: advanced proof search.
 This latter papers also presents many techniques one can employ to tune the
-inference of Canonical Structures.
+inference of canonical structures.
 
 
 Notation overloading
@@ -38,21 +38,21 @@ of the terms that are compared.
     End theory.
   End EQ.
 
-We use Coq modules as name spaces. This allows us to follow the same
+We use Coq modules as namespaces. 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
+namespace contains the definitions of the algebraic structure. To
 keep the example small, the algebraic structure ``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 will eventually contain lemmas holding on all the instances of the
+and will eventually contain lemmas holding 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, but we will not do that here.
 
 The following line tests that, when we assume a type ``e`` that is in
-theEQ class, then we can relates two of its objects with ``==``.
+theEQ class, we can relate two of its objects with ``==``.
 
 .. coqtop:: all
   
@@ -312,7 +312,7 @@ The following script registers an ``LEQ`` class for ``nat`` and for the type
 constructor ``*``. 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.
+subsection we show how to make them more compact.
 
 .. coqtop:: all
 
@@ -385,7 +385,7 @@ with message "T is not an EQ.type"”.
 
 The other utilities are used to ask |Coq| to solve a specific unification
 problem, that will in turn require the inference of some canonical structures.
-They are explained in mode details in :cite:`CSwcu`.
+They are explained in more details in :cite:`CSwcu`.
 
 We now have all we need to create a compact “packager” to declare
 instances of the ``LEQ`` class.
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 09faa06765..f134022eb6 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -31,7 +31,7 @@ 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 :g:`C t₁ .. tₙ`.
-In addition to these user-classes, we have two abstract classes:
+In addition to these user-defined classes, we have two built-in classes:
 
 
   * ``Sortclass``, the class of sorts; its objects are the terms whose type is a
@@ -50,11 +50,11 @@ Formally, the syntax of a classes is defined as:
 Coercions
 ---------
 
-A name ``f`` can be declared as a coercion between a source user-class
+A name ``f`` can be declared as a coercion between a source user-defined class
 ``C`` with `n` parameters and a target class ``D`` if one of these
 conditions holds:
 
- * ``D`` is a user-class, then the type of ``f`` must have the form
+ * ``D`` is a user-defined 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
@@ -65,8 +65,8 @@ conditions holds:
 We then write :g:`f : C >-> D`. The restriction on the type
 of coercions is called *the uniform inheritance condition*.
 
-.. note:: The abstract class ``Sortclass`` can be used as a source class, but
-          the abstract class ``Funclass`` cannot.
+.. note:: The built-in class ``Sortclass`` can be used as a source class, but
+          the built-in 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
@@ -95,7 +95,7 @@ We can now declare ``f`` as coercion from ``C'`` to ``D``, since we can
 
 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``
+of ``C'`` towards ``C``, we do 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
@@ -121,7 +121,7 @@ by the coercions ``f₁..fₖ``.  The application of a coercion path to a
 term consists of the successive application of its coercions.
 
 
-Declaration of Coercions
+Declaring Coercions
 -------------------------
 
 .. cmd:: Coercion @qualid : @class >-> @class
@@ -140,8 +140,8 @@ Declaration of Coercions
 
   .. warn:: Ambiguous path.
 
-     When the coercion :token:`qualid` is added to the inheritance graph, non
-     valid coercion paths are ignored; they are signaled by a warning
+     When the coercion :token:`qualid` is added to the inheritance graph,
+     invalid 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
@@ -215,7 +215,7 @@ declaration, this constructor is declared as a coercion.
 
   .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident
 
-    Idem but locally to the current section.
+    Same as ``Identity Coercion`` but locally to the current section.
 
   .. cmdv:: SubClass @ident := @type
      :name: SubClass
@@ -319,7 +319,7 @@ Coercions and Modules
 
    Since |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
+   were activated as soon as the module was required, whether it was
    imported or not.
 
    This option makes it possible to recover the behavior of the versions of
@@ -387,8 +387,8 @@ We give now an example using identity 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``
+sub-typing. To coerce :g:`t : forall x : A, B` towards
+:g:`forall x : A', B'`, we have to coerce ``A'`` towards ``A`` and ``B``
 towards ``B'``. An example is given below:
 
 .. coqtop:: all
@@ -424,8 +424,8 @@ replaced by ``x:A'`` where ``A'`` is the result of the application to
 ``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.
+functions. In :g:`forall x:A,B`, such a coercion path may also be applied
+to ``B`` if necessary.
 
 .. coqtop:: all