Uniformized many spelling variants. Added .. warning:: and .. seealso:: directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.

9 files changed, 75 insertions, 73 deletions

diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index 3af3115a59..2cc1f95c08 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -75,7 +75,7 @@ We amend that by equipping ``nat`` with a comparison relation.
    Check 3 == 3.
    Eval compute in 3 == 4.
 
-This last test shows that |Coq| is now not only able to typecheck ``3 == 3``,
+This last test shows that |Coq| is now not only able to type check ``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
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 8c1eacf085..e3d25cf5cf 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -423,7 +423,7 @@ a generic type ``'a`` to any term.
 First, if some part of the program is *very* polymorphic, there
 may be no ML type for it. In that case the extraction to ML works
 alright but the generated code may be refused by the ML
-type-checker. A very well known example is the ``distr-pair``
+type checker. A very well known example is the ``distr-pair``
 function:
 
 .. coqtop:: in
@@ -458,7 +458,7 @@ In |OCaml|, we must cast any argument of the constructor dummy
 
 Even with those unsafe castings, you should never get error like
 ``segmentation fault``. In fact even if your program may seem
-ill-typed to the |OCaml| type-checker, it can't go wrong : it comes
+ill-typed to the |OCaml| type checker, it can't go wrong : it comes
 from a Coq well-typed terms, so for example inductive types will always 
 have the correct number of arguments, etc. Of course, when launching
 manually some extracted function, you should apply it to arguments
@@ -469,7 +469,7 @@ found in :cite:`Let02`.
 
 We have to say, though, that in most "realistic" programs, these problems do not
 occur. For example all the programs of Coq library are accepted by the |OCaml|
-type-checker without any ``Obj.magic`` (see examples below).
+type checker without any ``Obj.magic`` (see examples below).
 
 Some examples
 -------------
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index c7df250672..e0babb6c4e 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -22,18 +22,18 @@ 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
+on the typeclass infrastructure. It also improves on and generalizes
 the previous implementation in several ways:
 
 + User-extensible algorithm. The algorithm is separated into two parts:
   generation of the rewriting constraints (written in ML) and solving
-  these constraints using type class resolution. As type class
+  these constraints using typeclass resolution. As typeclass
   resolution is extensible using tactics, this allows users to define
   general ways to solve morphism constraints.
 + Subrelations. 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.
+  the other. This is done purely using tactics and typeclass 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.
@@ -226,7 +226,7 @@ following command.
 
    This command declares ``f`` as a parametric morphism of signature ``sig``. The
    identifier :token:`ident` 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 base name of the typeclass 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
@@ -309,7 +309,7 @@ following command.
 
       Proof. intros. rewrite empty_neutral. reflexivity. Qed.
 
-   The tables of relations and morphisms are managed by the type class
+   The tables of relations and morphisms are managed by the typeclass
    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
@@ -350,7 +350,7 @@ prove that the argument of the morphism is defined.
 .. example::
 
    Let ``eqO`` be ``fun x y => x = y /\ x <> 0`` (the
-   smallest PER over non zero elements). Division can be declared as a
+   smallest PER over nonzero elements). Division can be declared as a
    morphism of signature ``eq ==> eq0 ==> eq``. Replacing ``x`` with
    ``y`` in ``div x n = div y n`` opens an additional goal ``eq0 n n``
    which is equivalent to ``n = n /\ n <> 0``.
@@ -446,7 +446,7 @@ 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
+properties of relations and morphisms as typeclasses. 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:
@@ -472,9 +472,9 @@ is equivalent to an instance declaration:
 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:`typeclasses`
-and the theories files in Classes for further explanations.
+also instances of a typeclass defined in ``Classes.Morphisms``. See the
+documentation on :ref:`typeclasses` 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
@@ -703,7 +703,7 @@ example of a mostly user-space extension of the algorithm.
 Constant unfolding
 ~~~~~~~~~~~~~~~~~~
 
-The resolution tactic is based on type classes and hence regards user-
+The resolution tactic is based on typeclasses 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,
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index f134022eb6..c0c4539564 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -352,7 +352,7 @@ We first give an example of coercion between atomic inductive types
 
 .. warning::
 
-  Note that ``Check true=O`` would fail. This is "normal" behaviour of
+  Note that ``Check true=O`` would fail. This is "normal" behavior of
   coercions. To validate ``true=O``, the coercion is searched from
   ``nat`` to ``bool``. There is none.
 
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 1ed3bffd2c..1e92d01125 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -11,7 +11,7 @@ Description of ``omega``
 .. tacn:: omega
 
    :tacn:`omega` is a tactic for solving goals in Presburger arithmetic,
-   i.e. for proving formulas made of equations and inequations over the
+   i.e. for proving formulas made of equations and inequalities over the
    type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers.
    Formulas on ``nat`` are automatically injected into ``Z``. The procedure
    may use any hypothesis of the current proof session to solve the goal.
@@ -140,12 +140,12 @@ Technical data
 Overview of the tactic
 ~~~~~~~~~~~~~~~~~~~~~~
 
- * The goal is negated twice and the first negation is introduced as an hypothesis.
- * Hypotheses are decomposed in simple equations or inequations. Multiple
+ * The goal is negated twice and the first negation is introduced as a hypothesis.
+ * Hypotheses are decomposed in simple equations or inequalities. Multiple
    goals may result from this phase.
- * Equations and inequations over ``nat`` are translated over
+ * Equations and inequalities over ``nat`` are translated over
    ``Z``, multiple goals may result from the translation of subtraction.
- * Equations and inequations are normalized.
+ * Equations and inequalities are normalized.
  * Goals are solved by the OMEGA decision procedure.
  * The script of the solution is replayed.
 
@@ -156,17 +156,17 @@ The OMEGA decision procedure involved in the :tacn:`omega` tactic uses
 a small subset of the decision procedure presented in :cite:`TheOmegaPaper`
 Here is an overview, refer to the original paper for more information.
 
- * Equations and inequations are normalized by division by the GCD of their
+ * Equations and inequalities are normalized by division by the GCD of their
    coefficients.
  * Equations are eliminated, using the Banerjee test to get a coefficient
    equal to one.
- * Note that each inequation cuts the Euclidean space in half.
- * Inequations are solved by projecting on the hyperspace
+ * Note that each inequality cuts the Euclidean space in half.
+ * Inequalities are solved by projecting on the hyperspace
    defined by cancelling one of the variables. They are partitioned
    according to the sign of the coefficient of the eliminated
-   variable. Pairs of inequations from different classes define a
+   variable. Pairs of inequalities from different classes define a
    new edge in the projection.
- * Redundant inequations are eliminated or merged in new
+ * Redundant inequalities are eliminated or merged in new
    equations that can be eliminated by the Banerjee test.
  * The last two steps are iterated until a contradiction is reached
    (success) or there is no more variable to eliminate (failure).
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 28fe68d78d..d6895f5fe5 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -18,7 +18,7 @@ program as in a regular functional programming language whilst using
 as rich a specification as desired and proving that the code meets the
 specification using the whole |Coq| proof apparatus. This is done using
 a technique originating from the “Predicate subtyping” mechanism of
-PVS :cite:`Rushby98`, which generates type-checking conditions while typing a
+PVS :cite:`Rushby98`, which generates type checking conditions while typing a
 term constrained to a particular type. Here we insert existential
 variables in the term, which must be filled with proofs to get a
 complete |Coq| term. |Program| replaces the |Program| tactic by Catherine
@@ -72,8 +72,8 @@ operation (see :ref:`extendedpatternmatching`).
   This permits to get the proper equalities in the context of proof
   obligations inside clauses, without which reasoning is very limited.
 
-+ Generation of inequalities. If a pattern intersects with a previous
-  one, an inequality is added in the context of the second branch. See
++ Generation of disequalities. If a pattern intersects with a previous
+  one, a disequality is added in the context of the second branch. See
   for example the definition of div2 below, where the second branch is
   typed in a context where :g:`∀ p, _ <> S (S p)`.
 + Coercion. If the object being matched is coercible to an inductive
@@ -87,7 +87,7 @@ coercions.
 .. opt:: Program Cases
 
    This controls the special treatment of pattern-matching generating equalities
-   and inequalities when using |Program| (it is on by default). All
+   and disequalities when using |Program| (it is on by default). All
    pattern-matches and let-patterns are handled using the standard algorithm
    of |Coq| (see :ref:`extendedpatternmatching`) when this option is
    deactivated.
@@ -104,7 +104,7 @@ Syntactic control over equalities
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 To give more control over the generation of equalities, the
-typechecker will fall back directly to |Coq|’s usual typing of dependent
+type checker will fall back directly to |Coq|’s usual typing of dependent
 pattern-matching if a return or in clause is specified. Likewise, the
 if construct is not treated specially by |Program| so boolean tests in
 the code are not automatically reflected in the obligations. One can
@@ -175,7 +175,7 @@ Program Definition
 
       .. TODO refer to production in alias
 
-See also: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold`
+.. seealso:: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold`
 
 .. _program_fixpoint:
 
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index d5c33dc1d4..8cb86e2267 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -19,7 +19,7 @@ field equations.
 What does this tactic do?
 ------------------------------
 
-``ring`` does associative-commutative rewriting in ring and semi-ring
+``ring`` does associative-commutative rewriting in ring and semiring
 structures. Assume you have two binary functions :math:`\oplus` and
 :math:`\otimes` that are associative and commutative, with :math:`\oplus`
 distributive on :math:`\otimes`, and two constants 0 and 1 that are unities for
@@ -37,7 +37,7 @@ order. It is an easy theorem to show that every polynomial is equivalent (modulo
 the ring properties) to exactly one canonical sum. This canonical sum is called
 the normal form of the polynomial. In fact, the actual representation shares
 monomials with same prefixes. So what does the ``ring`` tactic do? It normalizes polynomials over
-any ring or semi-ring structure. The basic use of ``ring`` is to simplify ring
+any ring or semiring structure. The basic use of ``ring`` is to simplify ring
 expressions, so that the user does not have to deal manually with the theorems
 of associativity and commutativity.
 
@@ -103,7 +103,7 @@ Concrete usage in Coq
 .. tacn:: ring
 
 The ``ring`` tactic solves equations upon polynomial expressions of a ring
-(or semi-ring) structure. It proceeds by normalizing both sides
+(or semiring) structure. It proceeds by normalizing both sides
 of the equation (w.r.t. associativity, commutativity and
 distributivity, constant propagation, rewriting of monomials) and
 comparing syntactically the results.
@@ -264,13 +264,13 @@ are the implementations of the ring operations, ``==`` is the equality of
 the coefficients, ``?+!`` is an implementation of this equality, and ``[x]``
 is a notation for the image of ``x`` by the ring morphism.
 
-Since |Z| is an initial ring (and |N| is an initial semi-ring), it can
+Since |Z| is an initial ring (and |N| is an initial semiring), it can
 always be considered as a set of coefficients. There are basically
 three kinds of (semi-)rings:
 
 abstract rings
   to be used when operations are not effective. The set
-  of coefficients is |Z| (or |N| for semi-rings).
+  of coefficients is |Z| (or |N| for semirings).
 
 computational rings
   to be used when operations are effective. The
@@ -505,10 +505,10 @@ expression `F` to a common denominator :math:`N/D = 0` where `N` and `D`
 are two ring expressions. For example, if we take :math:`F = (1 − 1/x) x − x + 1`, this
 gives :math:`N = (x − 1) x − x^2 + x` and :math:`D = x`. It then calls ring to solve 
 :math:`N = 0`.
-Note that ``field`` also generates non-zero conditions for all the
+Note that ``field`` also generates nonzero conditions for all the
 denominators it encounters in the reduction. In our example, it
 generates the condition :math:`x \neq 0`. These conditions appear as one subgoal
-which is a conjunction if there are several denominators. Non-zero
+which is a conjunction if there are several denominators. Nonzero
 conditions are always polynomial expressions. For example when
 reducing the expression :math:`1/(1 + 1/x)`, two side conditions are
 generated: :math:`x \neq 0` and :math:`x + 1 \neq 0`. Factorized expressions are broken since
@@ -616,7 +616,7 @@ carrier set, an equality, and field operations:
 satisfies the field axioms. Semi-fields (fields without + inverse) are
 also supported. The equality can be either Leibniz equality, or any
 relation declared as a setoid (see :ref:`tactics-enabled-on-user-provided-relations`). The definition of
-fields and semi-fields is:
+fields and semifields is:
 
 .. coqtop:: in
 
@@ -670,7 +670,7 @@ specific modifier:
 
 completeness :n:`@term`
   allows the field tactic to prove automatically
-  that the image of non-zero coefficients are mapped to non-zero
+  that the image of nonzero coefficients are mapped to nonzero
   elements of the field. :n:`@term` is a proof of
 
   ``forall x y, [x] == [y] ->  x ?=! y = true``, 
@@ -684,7 +684,7 @@ History of ring
 
 First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot
 of rewriting. But the proofs terms generated by rewriting were too big
-for |Coq|’s type-checker. Let us see why:
+for |Coq|’s type checker. Let us see why:
 
 .. coqtop:: all
 
@@ -707,7 +707,7 @@ interleaving of computation and reasoning (see :ref:`discussion_reflection`). He
 some |ML| code for the ``Add Ring`` command that allows registering new rings dynamically.
 
 Proofs terms generated by ring are quite small, they are linear in the
-number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type-checking
+number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type checking
 those terms requires some time because it makes a large use of the
 conversion rule, but memory requirements are much smaller.
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index b7946c6451..d26105b651 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -6,7 +6,7 @@ Type Classes
 ============
 
 This chapter presents a quick reference of the commands related to type
-classes. For an actual introduction to type classes, there is a
+classes. For an actual introduction to typeclasses, there is a
 description of the system :cite:`sozeau08` and the literature on type
 classes in Haskell which also applies.
 
@@ -76,7 +76,7 @@ for dealing with obligations.
 Binding classes
 ---------------
 
-Once a type class is declared, one can use it in class binders:
+Once a typeclass is declared, one can use it in class binders:
 
 .. coqtop:: all
 
@@ -92,7 +92,7 @@ found, an error is raised:
 
    Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
 
-The algorithm used to solve constraints is a variant of the eauto
+The algorithm used to solve constraints is a variant of the :tacn:`eauto`
 tactic that does proof search with a set of lemmas (the instances). It
 will use local hypotheses as well as declared lemmas in
 the ``typeclass_instances`` database. Hence the example can also be
@@ -103,13 +103,13 @@ written:
    Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y).
 
 However, the generalizing binders should be used instead as they have
-particular support for type classes:
+particular support for typeclasses:
 
-+ They automatically set the maximally implicit status for type class
++ They automatically set the maximally implicit status for typeclass
   arguments, making derived functions as easy to use as class methods.
   In the example above, ``A`` and ``eqa`` should be set maximally implicit.
 + They support implicit quantification on partially applied type
-  classes (:ref:`implicit-generalization`). Any argument not given as part of a type class
+  classes (:ref:`implicit-generalization`). Any argument not given as part of a typeclass
   binder will be automatically generalized.
 + They also support implicit quantification on :ref:`superclasses`.
 
@@ -148,7 +148,7 @@ database.
 Sections and contexts
 ---------------------
 
-To ease the parametrization of developments by type classes, we provide a new
+To ease the parametrization of developments by typeclasses, we provide a new
 way to introduce variables into section contexts, compatible with the implicit
 argument mechanism. The new command works similarly to the :cmd:`Variables`
 vernacular, except it accepts any binding context as argument. For example:
@@ -271,7 +271,7 @@ Summary of the commands
 
 .. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }
 
-   The :cmd:`Class` command is used to declare a type class with parameters
+   The :cmd:`Class` command is used to declare a typeclass with parameters
    ``binders`` and fields the declared record fields.
 
 Variants:
@@ -302,7 +302,7 @@ Variants:
 
 .. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
 
-The :cmd:`Instance` command is used to declare a type class instance named
+The :cmd:`Instance` command is used to declare a typeclass instance named
 ``ident`` of the class :cmd:`Class` with parameters ``t1`` to ``tn`` and
 fields ``b1`` to ``bi``, where each field must be a declared field of
 the class.  Missing fields must be filled in interactive proof mode.
@@ -310,7 +310,7 @@ the class.  Missing fields must be filled in interactive proof mode.
 An arbitrary context of ``binders`` can be put after the name of the
 instance and before the colon to declare a parameterized instance. An
 optional priority can be declared, 0 being the highest priority as for
-auto hints. If the priority is not specified, it defaults to the number
+:tacn:`auto` hints. If the priority is not specified, it defaults to the number
 of non-dependent binders of the instance.
 
 .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term
@@ -329,7 +329,7 @@ of non-dependent binders of the instance.
 .. cmdv:: Program Instance
    :name: Program Instance
 
-   Switches the type-checking to Program (chapter :ref:`programs`) and
+   Switches the type checking to Program (chapter :ref:`programs`) and
    uses the obligation mechanism to manage missing fields.
 
 .. cmdv:: Declare Instance
@@ -342,12 +342,12 @@ of non-dependent binders of the instance.
 
 
 Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
-few other commands related to type classes.
+few other commands related to typeclasses.
 
 .. cmd:: Existing Instance {+ @ident} [| priority]
 
    This command adds an arbitrary list of constants whose type ends with
-   an applied type class to the instance database with an optional
+   an applied typeclass to the instance database with an optional
    priority.  It can be used for redeclaring instances at the end of
    sections, or declaring structure projections as instances. This is
    equivalent to ``Hint Resolve ident : typeclass_instances``, except it
@@ -367,11 +367,11 @@ few other commands related to type classes.
    + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in
      the new proof engine (as of Coq 8.6), meaning that backtracking is
      available among dependent subgoals, and shelving goals is supported.
-     typeclasses eauto is a multi-goal tactic. It analyses the dependencies
+     ``typeclasses eauto`` is a multi-goal tactic. It analyses the dependencies
      between subgoals to avoid backtracking on subgoals that are entirely
      independent.
 
-   + When called with no arguments, typeclasses eauto uses
+   + When called with no arguments, ``typeclasses eauto`` uses
      the ``typeclass_instances`` database by default (instead of core).
      Dependent subgoals are automatically shelved, and shelved goals can
      remain after resolution ends (following the behavior of Coq 8.5).
@@ -379,13 +379,13 @@ few other commands related to type classes.
      .. note::
         As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully
         mimicks what happens during typeclass resolution when it is called
-        during refinement/type-inference, except that *only* declared class
+        during refinement/type inference, except that *only* declared class
         subgoals are considered at the start of resolution during type
         inference, while ``all`` can select non-class subgoals as well. It might
         move to ``all:typeclasses eauto`` in future versions when the
         refinement engine will be able to backtrack.
 
-   + When called with specific databases (e.g. with), typeclasses eauto
+   + When called with specific databases (e.g. with), ``typeclasses eauto``
      allows shelved goals to remain at any point during search and treat
      typeclass goals like any other.
 
@@ -403,10 +403,10 @@ few other commands related to type classes.
 
       .. warning::
          The semantics for the limit :n:`@num`
-         is different than for auto. By default, if no limit is given the
-         search is unbounded. Contrary to auto, introduction steps (intro) are
+         is different than for auto. By default, if no limit is given, the
+         search is unbounded. Contrary to :tacn:`auto`, introduction steps are
          counted, which might result in larger limits being necessary when
-         searching with typeclasses eauto than auto.
+         searching with ``typeclasses eauto`` than with :tacn:`auto`.
 
    .. cmdv:: typeclasses eauto with {+ @ident}
 
@@ -417,11 +417,11 @@ few other commands related to type classes.
 .. tacn:: autoapply @term with @ident
    :name: autoapply
 
-   The tactic autoapply applies a term using the transparency information
+   The tactic ``autoapply`` applies a term using the transparency information
    of the hint database ident, and does *no* typeclass resolution. This can
    be used in :cmd:`Hint Extern`’s for typeclass instances (in the hint
    database ``typeclass_instances``) to allow backtracking on the typeclass
-   subgoals created by the lemma application, rather than doing type class
+   subgoals created by the lemma application, rather than doing typeclass
    resolution locally at the hint application time.
 
 .. _TypeclassesTransparent:
@@ -431,7 +431,7 @@ Typeclasses Transparent, Typclasses Opaque
 
 .. cmd:: Typeclasses Transparent {+ @ident}
 
-   This command defines makes the identifiers transparent during type class
+   This command defines makes the identifiers transparent during typeclass
    resolution.
 
 .. cmd:: Typeclasses Opaque {+ @ident}
@@ -487,16 +487,18 @@ Options
    avoiding (functional) eta-expansions in the generated proof term. It
    does so by allowing hints that conclude in a product to apply to a
    goal with a matching product directly, avoiding an introduction.
-   *Warning:* this can be expensive as it requires rebuilding hint
-   clauses dynamically, and does not benefit from the invertibility
-   status of the product introduction rule, resulting in potentially more
-   expensive proof-search (i.e. more useless backtracking).
 
+   .. warning::
+
+      This can be expensive as it requires rebuilding hint
+      clauses dynamically, and does not benefit from the invertibility
+      status of the product introduction rule, resulting in potentially more
+      expensive proof-search (i.e. more useless backtracking).
 
 .. opt:: Typeclass Resolution For Conversion
 
    This option (on by default) controls the use of typeclass resolution
-   when a unification problem cannot be solved during elaboration/type-
+   when a unification problem cannot be solved during elaboration/type
    inference. With this option on, when a unification fails, typeclass
    resolution is tried before launching unification once again.
 
@@ -548,7 +550,7 @@ Typeclasses eauto `:=`
 
 .. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth
 
-   This command allows more global customization of the type class
+   This command allows more global customization of the typeclass
    resolution tactic. The semantics of the options are:
 
    + ``debug`` In debug mode, the trace of successfully applied tactics is
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index f245fab5ca..7e77dea457 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -36,7 +36,7 @@ error:
    Fail Definition selfid := identity (@identity).
 
 Indeed, the global level ``Top.1`` would have to be strictly smaller than
-itself for this self-application to typecheck, as the type of
+itself for this self-application to type check, as the type of
 :g:`(@identity)` is :g:`forall (A : Type@{Top.1}), A -> A` whose type is itself
 :g:`Type@{Top.1+1}`.