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.

24 files changed, 250 insertions, 228 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}`.
 
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index 2988b194e2..be0b5d5f12 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -60,7 +60,7 @@ the language ML.
 
 Automated theorem-proving was pioneered in the 1960’s by Davis and
 Putnam in propositional calculus. A complete mechanization (in the sense
-of a semi-decision procedure) of classical first-order logic was
+of a semidecision procedure) of classical first-order logic was
 proposed in 1965 by J.A. Robinson, with a single uniform inference rule
 called *resolution*. Resolution relies on solving equations in free
 algebras (i.e. term structures), using the *unification algorithm*. Many
@@ -320,7 +320,7 @@ in March 2001, version 7.1 in September 2001, version 7.2 in January
 
 Jean-Christophe Filliâtre designed the architecture of the new system.
 He introduced a new representation for environments and wrote a new
-kernel for type-checking terms. His approach was to use functional
+kernel for type checking terms. His approach was to use functional
 data-structures in order to get more sharing, to prepare the addition of
 modules and also to get closer to a certified kernel.
 
@@ -352,7 +352,7 @@ sensible. Jean-Christophe Filliâtre wrote ``coqdoc``, a documentation
 tool for |Coq| libraries usable from version 7.2.
 
 Bruno Barras improved the efficiency of the reduction algorithm and the
-confidence level in the correctness of |Coq| critical type-checking
+confidence level in the correctness of |Coq| critical type checking
 algorithm.
 
 Yves Bertot designed the ``SearchPattern`` and ``SearchRewrite`` tools
@@ -506,7 +506,7 @@ Credits: version 8.1
 Coq version 8.1 adds various new functionalities.
 
 Benjamin Grégoire implemented an alternative algorithm to check the
-convertibility of terms in the |Coq| type-checker. This alternative
+convertibility of terms in the |Coq| type checker. This alternative
 algorithm works by compilation to an efficient bytecode that is
 interpreted in an abstract machine similar to Xavier Leroy’s ZINC
 machine. Convertibility is performed by comparing the normal forms. This
@@ -526,7 +526,7 @@ Claudio Sacerdoti Coen added new features to the module system.
 
 Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new, more
 efficient and more general simplification algorithm for rings and
-semi-rings.
+semirings.
 
 Laurent Théry and Bruno Barras developed a new, significantly more
 efficient simplification algorithm for fields.
@@ -586,11 +586,11 @@ Coq version 8.2 adds new features, new libraries and improves on many
 various aspects.
 
 Regarding the language of |Coq|, the main novelty is the introduction by
-Matthieu Sozeau of a package of commands providing Haskell-style type
-classes. Type classes, that come with a few convenient features such as
+Matthieu Sozeau of a package of commands providing Haskell-style typeclasses.
+Typeclasses, which come with a few convenient features such as
 type-based resolution of implicit arguments, play a new landmark role
 in the architecture of |Coq| with respect to automation. For
-instance, thanks to type classes support, Matthieu Sozeau could
+instance, thanks to typeclass support, Matthieu Sozeau could
 implement a new resolution-based version of the tactics dedicated to
 rewriting on arbitrary transitive relations.
 
@@ -648,7 +648,7 @@ maintenance and coqdoc support, Vincent Siles contributed extensions of
 the Scheme command and of injection.
 
 Bruno Barras implemented the `coqchk` tool: this is a stand-alone
-type-checker that can be used to certify .vo files. Especially, as this
+type checker that can be used to certify .vo files. Especially, as this
 verifier runs in a separate process, it is granted not to be “hijacked”
 by virtually malicious extensions added to |Coq|.
 
@@ -712,7 +712,7 @@ The new tactic nsatz is due to Loïc Pottier. It works by computing
 Gröbner bases. Regarding the existing tactics, various improvements have
 been done by Matthieu Sozeau, Hugo Herbelin and Pierre Letouzey.
 
-Matthieu Sozeau extended and refined the type classes and Program
+Matthieu Sozeau extended and refined the typeclasses and Program
 features (the Russell language). Pierre Letouzey maintained and improved
 the extraction mechanism. Bruno Barras and Élie Soubiran maintained the
 Coq checker, Julien Forest maintained the Function mechanism for
@@ -810,7 +810,7 @@ Regarding the high-level specification language, Pierre Boutillier
 introduced the ability to give implicit arguments to anonymous
 functions, Hugo Herbelin introduced the ability to define notations with
 several binders (e.g. ``exists x y z, P``), Matthieu Sozeau made the
-type classes inference mechanism more robust and predictable, Enrico
+typeclass inference mechanism more robust and predictable, Enrico
 Tassi introduced a command Arguments that generalizes Implicit Arguments
 and Arguments Scope for assigning various properties to arguments of
 constants. Various improvements in the type inference algorithm were
@@ -831,7 +831,7 @@ vm\_compute. Bug fixes and miscellaneous improvements of the tactic
 language came from Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau.
 
 Regarding decision tactics, Loïc Pottier maintained nsatz, moving in
-particular to a type-class based reification of goals while Frédéric
+particular to a typeclass based reification of goals while Frédéric
 Besson maintained Micromega, adding in particular support for division.
 
 Regarding vernacular commands, Stéphane Glondu provided new commands to
@@ -1074,7 +1074,7 @@ over 100 contributions integrated. The main user visible changes are:
    document.
 
 -  More access to the proof engine features from Ltac: goal management
-   primitives, range selectors and a typeclasses eauto engine handling
+   primitives, range selectors and a ``typeclasses eauto`` engine handling
    multiple goals and multiple successes, by Cyprien Mangin, Matthieu
    Sozeau and Arnaud Spiwack.
 
@@ -1234,7 +1234,7 @@ The efficiency of the whole system has been significantly improved thanks to
 contributions from Pierre-Marie Pédrot, Maxime Dénès and Matthieu Sozeau and
 performance issue tracking by Jason Gross and Paul Steckler.
 
-Thomas Sibut-Pinote and Hugo Herbelin added support for side effects hooks in
+Thomas Sibut-Pinote and Hugo Herbelin added support for side effect hooks in
 cbv, cbn and simpl. The side effects are provided via a plugin available at
 https://github.com/herbelin/reduction-effects/.
 
@@ -1292,7 +1292,7 @@ integration of new features, with an important focus given to compatibility and
 performance issues, resulting in a hopefully more robust release than |Coq| 8.6
 while maintaining compatibility.
 
-|Coq| Enhancement Proposals (CEPs for short) and open pull-requests discussions
+|Coq| Enhancement Proposals (CEPs for short) and open pull request discussions
 were used to discuss publicly the new features.
 
 The |Coq| consortium, an organization directed towards users and supporters of the
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 1a610396e5..b57e4b209c 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -7,8 +7,8 @@ Introduction
 This document is the Reference Manual of the |Coq| proof assistant.
 To start using Coq, it is advised to first read a tutorial.
 Links to several tutorials can be found at
-https://coq.inria.fr/documentation (see also
-https://github.com/coq/coq/wiki#coq-tutorials).
+https://coq.inria.fr/documentation and
+https://github.com/coq/coq/wiki#coq-tutorials
 
 The |Coq| system is designed to develop mathematical proofs, and
 especially to write formal specifications, programs and to verify that
@@ -20,7 +20,7 @@ properties and proofs are formalized in the same language called
 *Calculus of Inductive Constructions*, that is a
 :math:`\lambda`-calculus with a rich type system. All logical judgments
 in |Coq| are typing judgments. The very heart of the |Coq| system is the
-type-checking algorithm that checks the correctness of proofs, in other
+type checking algorithm that checks the correctness of proofs, in other
 words that checks that a program complies to its specification. |Coq| also
 provides an interactive proof assistant to build proofs using specific
 programs called *tactics*.
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index b0ba2bcc31..3d3a1b11b1 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -96,8 +96,9 @@ constraints between the universe variables is maintained globally. To
 ensure the existence of a mapping of the universes to the positive
 integers, the graph of constraints must remain acyclic. Typing
 expressions that violate the acyclicity of the graph of constraints
-results in a Universe inconsistency error (see also Section
-:ref:`printing-universes`).
+results in a Universe inconsistency error.
+
+.. seealso:: Section :ref:`printing-universes`.
 
 
 .. _Terms:
@@ -1252,7 +1253,7 @@ In this expression, if :math:`m` eventually happens to evaluate to
 and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are replaced by the
 :math:`u_1 … u_{p_i}` according to the ι-reduction.
 
-Actually, for type-checking a :math:`\Match…\with…\endkw` expression we also need
+Actually, for type checking a :math:`\Match…\with…\endkw` expression we also need
 to know the predicate P to be proved by case analysis. In the general
 case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate
 over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I`
@@ -1398,7 +1399,7 @@ arguments of this constructor have type :math:`\Prop`. In that case, there is a
 canonical way to interpret the informative extraction on an object in
 that type, such that the elimination on any sort :math:`s` is legal. Typical
 examples are the conjunction of non-informative propositions and the
-equality. If there is an hypothesis :math:`h:a=b` in the local context, it can
+equality. If there is a hypothesis :math:`h:a=b` in the local context, it can
 be used for rewriting not only in logical propositions but also in any
 type.
 
@@ -1821,7 +1822,7 @@ definitions can be found in :cite:`Gimenez95b,Gim98,GimCas05`.
 The Calculus of Inductive Constructions with impredicative Set
 -----------------------------------------------------------------
 
-|Coq| can be used as a type-checker for the Calculus of Inductive
+|Coq| can be used as a type checker for the Calculus of Inductive
 Constructions with an impredicative sort :math:`\Set` by using the compiler
 option ``-impredicative-set``. For example, using the ordinary `coqtop`
 command, the following is rejected,
@@ -1832,7 +1833,7 @@ command, the following is rejected,
 
       Fail Definition id: Set := forall X:Set,X->X.
 
-while it will type-check, if one uses instead the `coqtop`
+while it will type check, if one uses instead the `coqtop`
 ``-impredicative-set`` option..
 
 The major change in the theory concerns the rule for product formation
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 7dd0a6e383..0fbe7ac70b 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -212,7 +212,7 @@ During the definition of the one-constructor inductive definition, all
 the errors of inductive definitions, as described in Section
 :ref:`gallina-inductive-definitions`, may also occur.
 
-**See also** Coercions and records in Section :ref:`coercions-classes-as-records` of the chapter devoted to coercions.
+.. seealso:: Coercions and records in section :ref:`coercions-classes-as-records` of the chapter devoted to coercions.
 
 .. _primitive_projections:
 
@@ -229,7 +229,7 @@ term constructor `r.(p)` representing a primitive projection `p` applied
 to a record object `r` (i.e., primitive projections are always applied).
 Even if the record type has parameters, these do not appear at
 applications of the projection, considerably reducing the sizes of
-terms when manipulating parameterized records and typechecking time.
+terms when manipulating parameterized records and type checking time.
 On the user level, primitive projections can be used as a replacement
 for the usual defined ones, although there are a few notable differences.
 
@@ -328,7 +328,7 @@ into a sequence of match on simple patterns. Especially, a
 construction defined using the extended match is generally printed
 under its expanded form (see :opt:`Printing Matching`).
 
-See also: :ref:`extendedpatternmatching`.
+.. seealso:: :ref:`extendedpatternmatching`.
 
 .. _if-then-else:
 
@@ -711,7 +711,7 @@ terminating functions.
 
      `functional inversion` will not be available for the function.
 
-See also: :ref:`functional-scheme` and :tacn:`function induction`
+.. seealso:: :ref:`functional-scheme` and :tacn:`function induction`
 
 Depending on the ``{…}`` annotation, different definition mechanisms are
 used by ``Function``. A more precise description is given below.
@@ -1260,7 +1260,7 @@ identifiers qualid, i.e. as list of identifiers separated by dots (see
 |Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts
 the name of a library is called a *library root*. All library files of
 the standard library of |Coq| have the reserved root |Coq| but library
-file names based on other roots can be obtained by using |Coq| commands
+filenames based on other roots can be obtained by using |Coq| commands
 (coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`command-line-options`).
 Also, when an interactive |Coq| session starts, a library of root ``Top`` is
 started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-options`).
@@ -1294,7 +1294,7 @@ short name (or even same partially qualified names as soon as the full
 names are different).
 
 Notice that the notion of absolute, partially qualified and short
-names also applies to library file names.
+names also applies to library filenames.
 
 **Visibility**
 
@@ -1328,7 +1328,7 @@ accessible, absolute names can never be hidden.
 
        Locate nat.
 
-See also: Commands :cmd:`Locate` and :cmd:`Locate Library`.
+.. seealso:: Commands :cmd:`Locate` and :cmd:`Locate Library`.
 
 .. _libraries-and-filesystem:
 
@@ -1514,7 +1514,8 @@ says that the implicit argument is maximally inserted.
 Each implicit argument can be declared to have to be inserted maximally or non
 maximally. This can be governed argument per argument by the command
 :cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option.
-See also :ref:`displaying-implicit-args`.
+
+.. seealso:: :ref:`displaying-implicit-args`.
 
 
 Casual use of implicit arguments
@@ -1887,7 +1888,7 @@ arguments that are not detected as strict implicit arguments. This
 “defensive” mode can quickly make the display cumbersome so this can
 be deactivated by turning this option off.
 
-See also: :opt:`Printing All`.
+.. seealso:: :opt:`Printing All`.
 
 Interaction with subtyping
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1937,7 +1938,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
    Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
    structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
    Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
-   solved during the type-checking process, :token:`qualid` is used as a solution.
+   solved during the type checking process, :token:`qualid` is used as a solution.
    Otherwise said, :token:`qualid` is canonically used to extend the field |c_i|
    into a complete structure built on |c_i|.
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index da5cd00d72..075235a8e2 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -920,7 +920,7 @@ Parametrized inductive types
 
      When this option is set (it is off by default),
      inductive definitions are abstracted over their parameters
-     before typechecking constructors, allowing to write:
+     before type checking constructors, allowing to write:
 
      .. coqtop:: all undo
 
@@ -1124,7 +1124,7 @@ constructions.
         arguments, and this choice influences the reduction of the fixpoint.
         Hence an explicit annotation must be used if the leftmost decreasing
         argument is not the desired one. Writing explicit annotations can also
-        speed up type-checking of large mutual fixpoints.
+        speed up type checking of large mutual fixpoints.
 
       + In order to keep the strong normalization property, the fixed point
         reduction will only be performed when the argument in position of the
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 4e42bddee2..9498f37c7e 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -104,8 +104,12 @@ The following command-line options are recognized by the commands ``coqc``
 and ``coqtop``, unless stated otherwise:
 
 :-I *directory*, -include *directory*: Add physical path *directory*
-  to the OCaml loadpath. See also: :ref:`names-of-libraries` and the
-  command Declare ML Module Section :ref:`compiled-files`.
+  to the OCaml loadpath.
+
+  .. seealso::
+
+     :ref:`names-of-libraries` and the
+     command Declare ML Module Section :ref:`compiled-files`.
 :-Q *directory* dirpath: Add physical path *directory* to the list of
   directories where |Coq| looks for a file and bind it to the logical
   directory *dirpath*. The subdirectory structure of *directory* is
@@ -115,14 +119,17 @@ and ``coqtop``, unless stated otherwise:
   an :n:`@ident` are taken into account. Conversely, the
   underlying file systems or operating systems may be more restrictive
   than |Coq|. While Linux’s ext4 file system supports any |Coq| recursive
-  layout (within the limit of 255 bytes per file name), the default on
+  layout (within the limit of 255 bytes per filename), the default on
   NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to
   disallow two files differing only in the case in the same directory.
-  See also: Section :ref:`names-of-libraries`.
+
+  .. seealso:: Section :ref:`names-of-libraries`.
 :-R *directory* dirpath: Do as -Q *directory* dirpath but make the
   subdirectory structure of *directory* recursively visible so that the
   recursive contents of physical *directory* is available from |Coq| using
-  short or partially qualified names. See also: Section :ref:`names-of-libraries`.
+  short or partially qualified names.
+
+  .. seealso:: Section :ref:`names-of-libraries`.
 :-top dirpath: Set the toplevel module name to dirpath instead of Top.
   Not valid for `coqc` as the toplevel module name is inferred from the
   name of the output file.
@@ -168,11 +175,16 @@ and ``coqtop``, unless stated otherwise:
 :-emacs, -ide-slave: Start a special toplevel to communicate with a
   specific IDE.
 :-impredicative-set: Change the logical theory of |Coq| by declaring the
-   sort Set impredicative. Warning: This is known to be inconsistent with some
-   standard axioms of classical mathematics such as the functional
-   axiom of choice or the principle of description.
-:-type-in-type: Collapse the universe hierarchy of |Coq|. Warning: This makes the logic
-   inconsistent.
+   sort Set impredicative.
+
+   .. warning::
+
+      This is known to be inconsistent with some
+      standard axioms of classical mathematics such as the functional
+      axiom of choice or the principle of description.
+:-type-in-type: Collapse the universe hierarchy of |Coq|.
+
+  .. warning:: This makes the logic inconsistent.
 :-mangle-names *ident*: Experimental: Do not depend on this option. Replace
   Coq's auto-generated name scheme with names of the form *ident0*, *ident1*,
   etc. The command ``Set Mangle Names`` turns the behavior on in a document,
@@ -208,7 +220,7 @@ The ``coqchk`` command takes a list of library paths as argument, described eith
 by their logical name or by their physical filename, hich must end in ``.vo``. The
 corresponding compiled libraries (``.vo`` files) are searched in the path,
 recursively processing the libraries they depend on. The content of all these
-libraries is then type-checked. The effect of ``coqchk`` is only to return with
+libraries is then type checked. The effect of ``coqchk`` is only to return with
 normal exit code in case of success, and with positive exit code if an error has
 been found. Error messages are not deemed to help the user understand what is
 wrong. In the current version, it does not modify the compiled libraries to mark
@@ -248,15 +260,15 @@ the following: assuming that ``coqchk`` is called with argument ``M``, option
 ``-norec N``, and ``-admit A``. Let us write :math:`\overline{S}` for the
 set of reflexive transitive dependencies of set :math:`S`. Then:
 
-+ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type-checked before being added
++ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type checked before being added
   to the context.
 + And :math:`M \cup N \backslash C` is the set of modules that are loaded and added to the
-  context without type-checking. Basic integrity checks (checksums) are
+  context without type checking. Basic integrity checks (checksums) are
   nonetheless performed.
 
 As a rule of thumb, -admit can be used to tell Coq that some libraries
 have already been checked. So ``coqchk A B`` can be split in ``coqchk A`` &&
-``coqchk B -admit A`` without type-checking any definition twice. Of
+``coqchk B -admit A`` without type checking any definition twice. Of
 course, the latter is slightly slower since it makes more disk access.
 It is also less secure since an attacker might have replaced the
 compiled library ``A`` after it has been read by the first command, but
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index f7f442092f..bc6a074a27 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -12,7 +12,7 @@ file, executing corresponding commands or undoing them respectively.
 
 |CoqIDE| is run by typing the command `coqide` on the command line.
 Without argument, the main screen is displayed with an “unnamed
-buffer”, and with a file name as argument, another buffer displaying
+buffer”, and with a filename as argument, another buffer displaying
 the contents of that file. Additionally, `coqide` accepts the same
 options as `coqtop`, given in :ref:`thecoqcommands`, the ones having obviously
 no meaning for |CoqIDE| being ignored.
@@ -92,7 +92,7 @@ buffers (left and right arrows); an "information" button; and a "gears" button.
 
 The "information" button is described in Section :ref:`try-tactics-automatically`.
 
-The "gears" button submits proof terms to the |Coq| kernel for type-checking.
+The "gears" button submits proof terms to the |Coq| kernel for type checking.
 When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`),
 proofs may have been completed without kernel-checking of generated proof terms.
 The presence of unchecked proof terms is indicated by ``Qed`` statements that
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index e779515a00..218a19c2e5 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -43,7 +43,7 @@ Building a |Coq| project with coq_makefile
 The majority of |Coq| projects are very similar: a collection of ``.v``
 files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of
 metadata needed in order to build the project are the command line
-options to ``coqc`` (e.g. ``-R``, ``-I``, see also: Section
+options to ``coqc`` (e.g. ``-R``, ``-I``, see also: section
 :ref:`command-line-options`). Collecting the list of files and options is the job
 of the ``_CoqProject`` file.
 
@@ -107,7 +107,7 @@ decide how to build them. In particular:
 
 The use of ``.mlpack`` files has to be preferred over ``.mllib`` files,
 since it results in a “packed” plugin: All auxiliary modules (as
-``Baz`` and ``Bazaux``) are hidden inside the plugin’s “name space”
+``Baz`` and ``Bazaux``) are hidden inside the plugin’s "namespace"
 (``Qux_plugin``). This reduces the chances of begin unable to load two
 distinct plugins because of a clash in their auxiliary module names.
 
@@ -773,7 +773,7 @@ Command line options
     preamble, right before ``\begin{document}`` (meaningless with ``-html``).
   :--vernac-file file,--tex-file file: Considers the file ‘file’
     respectively as a ``.v`` (or ``.g``) file or a ``.tex`` file.
-  :--files-from file: Read file names to be processed from the file ‘file’ as if
+  :--files-from file: Read filenames to be processed from the file ‘file’ as if
     they were given on the command line. Useful for program sources split
     up into several directories.
   :-q, --quiet: Be quiet. Do not print anything except errors.
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 225df8d54c..344134b6f9 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -21,7 +21,7 @@ applied to the abstracted instance and after simplification of the
 equalities we get the expected goals.
 
 The abstracting tactic is called generalize_eqs and it takes as
-argument an hypothesis to generalize. It uses the JMeq datatype
+argument a hypothesis to generalize. It uses the JMeq datatype
 defined in Coq.Logic.JMeq, hence we need to require it before. For
 example, revisiting the first example of the inversion documentation:
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 0310dbead5..7608ea7245 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -556,9 +556,9 @@ Failing
       The number is the failure level. If no level is specified, it defaults to 0.
       The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching
       tacticals. If 0, it makes :tacn:`match goal` consider the next clause
-      (backtracking). If non zero, the current :tacn:`match goal` block, :tacn:`try`,
+      (backtracking). If nonzero, the current :tacn:`match goal` block, :tacn:`try`,
       :tacn:`repeat`, or branching command is aborted and the level is decremented. In
-      the case of :n:`+`, a non-zero level skips the first backtrack point, even if
+      the case of :n:`+`, a nonzero level skips the first backtrack point, even if
       the call to :n:`fail @num` is not enclosed in a :n:`+` command,
       respecting the algebraic identity.
 
@@ -863,7 +863,7 @@ We can perform pattern matching on goals using the following expression:
    :name: match goal
 
    If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is
-   matched (non-linear first-order unification) by an hypothesis of the
+   matched (non-linear first-order unification) by a hypothesis of the
    goal and if :n:`cpattern_1` is matched by the conclusion of the goal,
    then :n:`@expr__1` is evaluated to :n:`v__1` by substituting the
    pattern matching to the metavariables and the real hypothesis names
@@ -989,7 +989,7 @@ Manipulating untyped terms
 
    An untyped term, in |Ltac|, can contain references to hypotheses or to
    |Ltac| variables containing typed or untyped terms. An untyped term can be
-   type-checked using the function type_term whose argument is parsed as an
+   type checked using the function type_term whose argument is parsed as an
    untyped term and returns a well-typed term which can be used in tactics.
 
 Untyped terms built using :n:`uconstr :` can also be used as arguments to the
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index fe2124502a..b1e769c571 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -84,7 +84,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
       :name: Defined
 
       Same as :cmd:`Qed` but the proof is then declared transparent, which means
-      that its content can be explicitly used for type-checking and that it can be
+      that its content can be explicitly used for type checking and that it can be
       unfolded in conversion tactics (see :ref:`performingcomputations`,
       :cmd:`Opaque`, :cmd:`Transparent`).
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index be30f69704..7c3ea1a28c 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -37,7 +37,7 @@ bookkeeping is performed on the conclusion of the goal, using for that
 purpose a couple of syntactic constructions behaving similar to tacticals
 (and often named as such in this chapter). The ``:`` tactical moves hypotheses
 from the context to the conclusion, while ``=>`` moves hypotheses from the
-conclusion to the context, and ``in`` moves back and forth an hypothesis from the
+conclusion to the context, and ``in`` moves back and forth a hypothesis from the
 context to the conclusion for the time of applying an action to it.
 
 While naming hypotheses is commonly done by means of an ``as`` clause in the
@@ -303,7 +303,7 @@ the ``if`` construct to all binary data types; compare
 
 The latter appears to be marginally shorter, but it is quite
 ambiguous, and indeed often requires an explicit annotation
-``(term : {_} + {_})`` to type-check, which evens the character count.
+``(term : {_} + {_})`` to type check, which evens the character count.
 
 Therefore, |SSR| restricts by default the condition of a plain if
 construct to the standard ``bool`` type; this avoids spurious type
@@ -385,7 +385,7 @@ expressions such as
 
 Unfortunately, such higher-order expressions are quite frequent in
 representation functions, especially those which use |Coq|'s
-``Structures`` to emulate Haskell type classes.
+``Structures`` to emulate Haskell typeclasses.
 
 Therefore, |SSR| provides a variant of |Coq|’s implicit argument
 declaration, which causes |Coq| to fill in some implicit parameters at
@@ -1285,7 +1285,7 @@ catch the appropriate number of wildcards to be inserted. Note that
 this use of the refine tactic implies that the tactic tries to match
 the goal up to expansion of constants and evaluation of subterms.
 
-|SSR|’s apply has a special behaviour on goals containing
+|SSR|’s apply has a special behavior on goals containing
 existential metavariables of sort Prop.
 
 .. example::
@@ -2064,26 +2064,27 @@ is equivalent to:
 
 (see section :ref:`discharge_ssr` for the documentation of the apply: combination).
 
-Warning The list of tactics, possibly chained by semicolons, that
-follows a by keyword is considered as a parenthesized block applied to
-the current goal. Hence for example if the tactic:
+.. warning::
 
-.. coqtop:: in
+   The list of tactics (possibly chained by semicolons) that
+   follows the ``by`` keyword is considered to be a parenthesized block applied to
+   the current goal. Hence for example if the tactic:
 
-   by rewrite my_lemma1.
+   .. coqtop:: in
 
-succeeds, then the tactic:
+      by rewrite my_lemma1.
 
-.. coqtop:: in
+   succeeds, then the tactic:
 
-   by rewrite my_lemma1; apply my_lemma2.
+   .. coqtop:: in
 
-usually fails since it is equivalent to:
+      by rewrite my_lemma1; apply my_lemma2.
 
-.. coqtop:: in
+   usually fails since it is equivalent to:
 
-   by (rewrite my_lemma1; apply my_lemma2).
+   .. coqtop:: in
 
+      by (rewrite my_lemma1; apply my_lemma2).
 
 
 .. _selectors_ssr:
@@ -2653,11 +2654,11 @@ Last, notice that the use of intro patterns for abstract constants is
 orthogonal to the transparent flag ``@`` for have.
 
 
-The have tactic and type classes resolution
+The have tactic and typeclass resolution
 ```````````````````````````````````````````
 
-Since |SSR| 1.5 the have tactic behaves as follows with respect to
-type classes inference.
+Since |SSR| 1.5 the ``have`` tactic behaves as follows with respect to
+typeclass inference.
 
   .. coqtop:: none
 
@@ -2699,7 +2700,7 @@ type classes inference.
 
 .. opt:: SsrHave NoTCResolution
 
-   This option restores the behavior of |SSR| 1.4 and below (never resolve type classes).
+   This option restores the behavior of |SSR| 1.4 and below (never resolve typeclasses).
 
 Variants: the suff and wlog tactics
 ```````````````````````````````````
@@ -3009,6 +3010,15 @@ An :token:`r_item` can be:
   is equivalent to: ``change term1 with term2.`` If ``term2`` is a
   single constant and ``term1`` head symbol is not ``term2``, then the head
   symbol of ``term1`` is repeatedly unfolded until ``term2`` appears.
++ A :token:`term`, which can be:
+    + A term whose type has the form:
+      ``forall (x1 : A1 )…(xn : An ), eq term1 term2`` where
+      ``eq`` is the Leibniz equality or a registered setoid
+      equality.
+    + A list of terms ``(t1 ,…,tn)``, each ``ti`` having a type above.
+      The tactic: ``rewrite r_prefix (t1 ,…,tn ).``
+      is equivalent to: ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].``
+    + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above.  tactic: ``rewrite (_ : term)`` is in fact synonym of: ``cutrewrite (term).``.
 
   .. example::
 
@@ -3026,9 +3036,10 @@ An :token:`r_item` can be:
         Lemma test x : ddouble x = 4 * x.
         rewrite [ddouble _]/double.
 
-     *Warning* The |SSR|
-     terms containing holes are *not* typed as abstractions in this
-     context. Hence the following script fails.
+  .. warning::
+
+     The |SSR| terms containing holes are *not* typed as
+     abstractions in this context. Hence the following script fails.
 
      .. coqtop:: none
 
@@ -3050,17 +3061,6 @@ An :token:`r_item` can be:
 
         rewrite -[f y x]/(y + _).
 
-+ A :token:`term`, which can be:
-
-    + A term whose type has the form:
-      ``forall (x1 : A1 )…(xn : An ), eq term1 term2`` where
-      ``eq`` is the Leibniz equality or a registered setoid
-      equality.
-    + A list of terms ``(t1 ,…,tn)``, each ``ti`` having a type above.
-      The tactic: ``rewrite r_prefix (t1 ,…,tn ).``
-      is equivalent to: ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].``
-    + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above.  tactic: ``rewrite (_ : term)`` is in fact synonym of: ``cutrewrite (term).``.
-
 
 Remarks and examples
 ~~~~~~~~~~~~~~~~~~~~
@@ -3701,20 +3701,22 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to
 ``bar``; hence ``unfold foo`` will replace ``foo`` by ``bar``, and
 ``fold foo`` will replace ``bar`` by ``foo``.
 
-*Warning* The ``nosimpl`` trick only works if no reduction is apparent in
-``t``; in particular, the declaration:
+.. warning::
 
-.. coqtop:: in
+   The ``nosimpl`` trick only works if no reduction is apparent in
+   ``t``; in particular, the declaration:
 
-   Definition foo x := nosimpl (bar x).
+   .. coqtop:: in
 
-will usually not work. Anyway, the common practice is to tag only the
-function, and to use the following definition, which blocks the
-reduction as expected:
+      Definition foo x := nosimpl (bar x).
 
-.. coqtop:: in
+   will usually not work. Anyway, the common practice is to tag only the
+   function, and to use the following definition, which blocks the
+   reduction as expected:
+
+   .. coqtop:: in
 
-   Definition foo x := nosimpl bar x.
+      Definition foo x := nosimpl bar x.
 
 A standard example making this technique shine is the case of
 arithmetic operations. We define for instance:
@@ -4757,7 +4759,7 @@ equivalence property has been defined.
 
    Lemma andE (b1 b2 : bool) : (b1 /\ b2) <-> (b1 && b2).
 
-Let us compare the respective behaviours of ``andE`` and ``andP``.
+Let us compare the respective behaviors of ``andE`` and ``andP``.
 
 
 .. example::
@@ -4870,7 +4872,7 @@ The term , called the *view lemma* can be:
 
 Let ``top`` be the top assumption in the goal.
 
-There are three steps in the behaviour of an assumption view tactic:
+There are three steps in the behavior of an assumption view tactic:
 
 + It first introduces ``top``.
 + If the type of :token:`term` is neither a double implication nor an
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index fcb52cf275..854c3c919c 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -186,7 +186,7 @@ Applying theorems
 .. tacn:: assumption
    :name: assumption
 
-   This tactic looks in the local context for an hypothesis whose type is
+   This tactic looks in the local context for a hypothesis whose type is
    convertible to the goal. If it is the case, the subgoal is proved.
    Otherwise, it fails.
 
@@ -255,13 +255,13 @@ Applying theorems
    .. tacv:: notypeclasses refine @term
       :name: notypeclasses refine
 
-      This tactic behaves like :tacn:`refine` except it performs typechecking without
+      This tactic behaves like :tacn:`refine` except it performs type checking without
       resolution of typeclasses.
 
    .. tacv:: simple notypeclasses refine @term
       :name: simple notypeclasses refine
 
-      This tactic behaves like :tacn:`simple refine` except it performs typechecking
+      This tactic behaves like :tacn:`simple refine` except it performs type checking
       without resolution of typeclasses.
 
 .. tacn:: apply @term
@@ -797,7 +797,7 @@ Managing the local context
    Introduction via :n:`({+& p})` is a shortcut for introduction via
    :n:`(p,( ... ,( ..., p ) ... ))`; it expects the hypothesis to be a sequence of
    right-associative binary inductive constructors such as :g:`conj` or
-   :g:`ex_intro`; for instance, an hypothesis with type
+   :g:`ex_intro`; for instance, a hypothesis with type
    :g:`A /\(exists x, B /\ C /\ D)` can be introduced via pattern
    :n:`(a & x & b & c & d)`;
 
@@ -1384,7 +1384,7 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`.
    :name: contradiction
 
    This tactic applies to any goal. The contradiction tactic attempts to
-   find in the current context (after all intros) an hypothesis that is
+   find in the current context (after all intros) a hypothesis that is
    equivalent to an empty inductive type (e.g. :g:`False`), to the negation of
    a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory
    hypotheses.
@@ -1440,7 +1440,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       anymore dependent in the goal after application of :tacn:`destruct`, it
       is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`).
 
-      If :token:`ident` is an hypothesis of the context, and :token:`ident`
+      If :token:`ident` is a hypothesis of the context, and :token:`ident`
       is not anymore dependent in the goal after application
       of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as
       in :n:`destruct (@ident)`).
@@ -1477,7 +1477,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       enough names, :tacn:`destruct` invents names for the remaining variables
       to introduce. More generally, the :n:`pij` can be any introduction
       pattern (see :tacn:`intros`). This provides a concise notation for
-      chaining destruction of an hypothesis.
+      chaining destruction of a hypothesis.
 
    .. tacv:: destruct @term eqn:@naming_intro_pattern
       :name: destruct ... eqn:
@@ -1586,7 +1586,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
         For simple induction on a numeral, use syntax induction (num)
         (not very interesting anyway).
 
-   + In case term is an hypothesis :n:`@ident` of the context, and :n:`@ident`
+   + In case term is a hypothesis :n:`@ident` of the context, and :n:`@ident`
      is not anymore dependent in the goal after application of :n:`induction`,
      it is erased (to avoid erasure, use parentheses, as in
      :n:`induction (@ident)`).
@@ -1878,9 +1878,7 @@ and an explanation of the underlying technique.
    :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions`
    for details.
 
-See also: :ref:`advanced-recursive-functions`
-  :ref:`functional-scheme`
-  :tacn:`inversion`
+.. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion`
 
 .. exn:: Cannot find induction information on @qualid.
 .. exn:: Not the right number of induction arguments.
@@ -2041,7 +2039,7 @@ See also: :ref:`advanced-recursive-functions`
    the number of equalities newly generated. If it is smaller, fresh
    names are automatically generated to adjust the list of :n:`@intro_pattern`
    to the number of new equalities. The original equality is erased if it
-   corresponds to an hypothesis.
+   corresponds to a hypothesis.
 
    .. opt:: Structural Injection
 
@@ -2312,8 +2310,8 @@ See also: :ref:`advanced-recursive-functions`
 
    As H occurs in the goal, we may want to reason by cases on its
    structure and so, we would like inversion tactics to substitute H by
-   the corresponding @term in constructor form. Neither Inversion nor
-   Inversion_clear make such a substitution. To have such a behavior we
+   the corresponding @term in constructor form. Neither :tacn:`inversion` nor
+   :n:`inversion_clear` do such a substitution. To have such a behavior we
    use the dependent inversion tactics:
 
    .. coqtop:: all
@@ -3205,7 +3203,7 @@ the :tacn:`auto` and :tacn:`trivial` tactics:
 .. opt:: Info Trivial
 .. opt:: Debug Trivial
 
-See also: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
+.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
 
 .. tacn:: eauto
    :name: eauto
@@ -3236,7 +3234,7 @@ Note that ``ex_intro`` should be declared as a hint.
 .. opt:: Info Eauto
 .. opt:: Debug Eauto
 
-See also: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
+.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
 
 
 .. tacn:: autounfold with {+ @ident}
@@ -3293,10 +3291,10 @@ command.
   Performs all the rewriting in the clause :n:`@clause`. The clause argument
   must not contain any ``type of`` nor ``value of``.
 
-See also: :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by
-:tacn:`autorewrite`.
+.. seealso:
 
-See also: :tacn:`autorewrite` for examples showing the use of this tactic.
+   :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by
+   :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic.
 
 .. tacn:: easy
    :name: easy
@@ -3592,7 +3590,7 @@ At Coq startup, only the core database is nonempty and can be used.
 :zarith: contains lemmas about binary signed integers from the directories
          theories/ZArith. When required, the module Omega also extends the
          database zarith with a high-cost hint that calls ``omega`` on equations
-         and inequalities in nat or Z.
+         and inequalities in ``nat`` or ``Z``.
 
 :bool: contains lemmas about booleans, mostly from directory theories/Bool.
 
@@ -3602,7 +3600,7 @@ At Coq startup, only the core database is nonempty and can be used.
 :sets: contains lemmas about sets and relations from the directories Sets and
        Relations.
 
-:typeclass_instances: contains all the type class instances declared in the
+:typeclass_instances: contains all the typeclass instances declared in the
                       environment, including those used for ``setoid_rewrite``,
                       from the Classes directory.
 
@@ -3731,7 +3729,7 @@ Setting implicit automation tactics
    In this case the tactic command typed by the user is equivalent to
    ``tactic``:sub:`1` ``;tactic``.
 
-   See also: ``Proof.`` in :ref:`proof-editing-mode`.
+   .. seealso:: ``Proof`` in :ref:`proof-editing-mode`.
 
 
    .. cmdv:: Proof with tactic using {+ @ident}
@@ -4205,8 +4203,9 @@ available after a ``Require Import FunInd``.
 
 .. tacv:: functional inversion @num
 
-  This does the same thing as intros until num thenfunctional inversion ident
-  where ident is the identifier for the last introduced hypothesis.
+  This does the same thing as :n:`intros until @num` folowed by
+  :n:`functional inversion @ident` where :token:`ident` is the
+  identifier for the last introduced hypothesis.
 
 .. tacv:: functional inversion ident qualid
 .. tacv:: functional inversion num qualid
@@ -4313,7 +4312,7 @@ and :g:`Z` of binary integers. This tactic must be loaded by the command
    :name: ring_simplify
 
 The :n:`ring` tactic solves equations upon polynomial expressions of a ring
-(or semi-ring) structure. It proceeds by normalizing both hand sides
+(or semiring) structure. It proceeds by normalizing both hand sides
 of the equation (w.r.t. associativity, commutativity and
 distributivity, constant propagation) and comparing syntactically the
 results.
@@ -4366,8 +4365,10 @@ printed with the Print Fields command.
 
       intros; field.
 
-See also: file plugins/setoid_ring/RealField.v for an example of instantiation,
-theory theories/Reals for many examples of use of field.
+.. seealso::
+
+   File plugins/setoid_ring/RealField.v for an example of instantiation,
+   theory theories/Reals for many examples of use of field.
 
 Non-logical tactics
 ------------------------
@@ -4488,7 +4489,7 @@ user-defined tactics.
   other one can be automatically checked.
 .. [2] This corresponds to the cut rule of sequent calculus.
 .. [3] Reminder: opaque constants will not be expanded by δ reductions.
-.. [4] The behavior of this tactic has much changed compared to the
+.. [4] The behavior of this tactic has changed a lot compared to the
   versions available in the previous distributions (V6). This may cause
   significant changes in your theories to obtain the same result. As a
   drawback of the re-engineering of the code, this tactic has also been
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 0a517973c2..87131879e2 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -246,7 +246,7 @@ Requests to the environment
    hypothesis introduced in the first subgoal (if a proof is in
    progress).
 
-   See also: Section :ref:`performingcomputations`.
+   .. seealso:: Section :ref:`performingcomputations`.
 
 
 .. cmd:: Compute @term
@@ -255,7 +255,7 @@ Requests to the environment
    bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in``
    :n:`@term`.
 
-   See also: Section :ref:`performingcomputations`.
+   .. seealso:: Section :ref:`performingcomputations`.
 
 
 .. cmd:: Print Assumptions @qualid
@@ -521,7 +521,7 @@ Requests to the environment
    This command displays the full name of objects whose name is a prefix
    of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in
    which they are defined. It searches for objects from the different
-   qualified name spaces of |Coq|: terms, modules, Ltac, etc.
+   qualified namespaces of |Coq|: terms, modules, Ltac, etc.
 
    .. example::
 
@@ -549,7 +549,7 @@ Requests to the environment
 
       As Locate but restricted to tactics.
 
-See also: Section :ref:`locating-notations`
+.. seealso:: Section :ref:`locating-notations`
 
 
 .. _loading-files:
@@ -587,7 +587,9 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
 
       Display, while loading,
       the answers of |Coq| to each command (including tactics) contained in
-      the loaded file See also: Section :ref:`controlling-display`.
+      the loaded file.
+
+      .. seealso:: Section :ref:`controlling-display`.
 
    .. exn:: Can’t find file @ident on loadpath.
 
@@ -699,10 +701,7 @@ file is a particular case of module called *library file*.
       that the commands ``Import`` and ``Export`` alone can be used inside modules
       (see Section :ref:`Import <import_qualid>`).
 
-
-
-See also: Chapter :ref:`thecoqcommands`
-
+      .. seealso:: Chapter :ref:`thecoqcommands`
 
 .. cmd:: Print Libraries
 
@@ -930,7 +929,7 @@ Quitting and debugging
 
 .. cmd:: Drop
 
-   This is used mostly as a debug facility by |Coq|’s implementors and does
+   This is used mostly as a debug facility by |Coq|’s implementers and does
    not concern the casual user. This command permits to leave |Coq|
    temporarily and enter the OCaml toplevel. The OCaml
    command:
@@ -1097,8 +1096,10 @@ described first.
       The scope of :cmd:`Opaque` is limited to the current section, or current
       file, unless the variant :cmd:`Global Opaque` is used.
 
-   See also: sections :ref:`performingcomputations`, :ref:`tactics-automating`,
-   :ref:`proof-editing-mode`
+   .. seealso::
+
+      Sections :ref:`performingcomputations`, :ref:`tactics-automating`,
+      :ref:`proof-editing-mode`
 
    .. exn:: The reference @qualid was not found in the current environment.
 
@@ -1130,8 +1131,10 @@ described first.
 
       There is no constant referred by :n:`@qualid` in the environment.
 
-   See also: sections :ref:`performingcomputations`,
-   :ref:`tactics-automating`, :ref:`proof-editing-mode`
+      .. seealso:
+
+         Sections :ref:`performingcomputations`,
+         :ref:`tactics-automating`, :ref:`proof-editing-mode`
 
 .. _vernac-strategy:
 
@@ -1195,7 +1198,7 @@ described first.
    nothing prevents the user to also perform a
    ``Ltac`` `ident` ``:=`` `convtactic`.
 
-   See also: sections :ref:`performingcomputations`
+   .. seealso: :ref:`performingcomputations`
 
 
 .. _controlling-locality-of-commands:
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index d92b9a6794..5089a1b3e3 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -119,7 +119,7 @@ command understands. Here is how the previous examples refine.
    Notation "A /\ B" := (and A B) (at level 80, right associativity).
    Notation "A \/ B" := (or A B) (at level 85, right associativity).
 
-By default, a notation is considered non-associative, but the
+By default, a notation is considered nonassociative, but the
 precedence level is mandatory (except for special cases whose level is
 canonical). The level is either a number or the phrase ``next level``
 whose meaning is obvious.
@@ -139,7 +139,7 @@ instance define prefix notations.
    Notation "~ x" := (not x) (at level 75, right associativity).
 
 One can also define notations for incomplete terms, with the hole
-expected to be inferred during typechecking.
+expected to be inferred during type checking.
 
 .. coqtop:: in
 
@@ -296,7 +296,7 @@ the possible following elements delimited by single quotes:
   after the “``[``” is applied at the beginning of each newline
 
 Notations disappear when a section is closed. No typing of the denoted
-expression is performed at definition time. Type-checking is done only
+expression is performed at definition time. Type checking is done only
 at the time of use of the notation.
 
 .. note:: Sometimes, a notation is expected only for the parser. To do
@@ -899,7 +899,7 @@ notations are given below. The optional :production:`scope` is described in
                  : | as strict pattern
 
 .. note:: No typing of the denoted expression is performed at definition
-          time. Type-checking is done only at the time of use of the notation.
+          time. Type checking is done only at the time of use of the notation.
 
 .. note:: Some examples of Notation may be found in the files composing
           the initial state of Coq (see directory :file:`$COQLIB/theories/Init`).
@@ -1369,7 +1369,7 @@ Abbreviations
       Check (id 0).
 
    Abbreviations disappear when a section is closed. No typing of the
-   denoted expression is performed at definition time. Type-checking is
+   denoted expression is performed at definition time. Type checking is
    done only at the time of use of the abbreviation.
 
 .. _TacticNotation:
@@ -1431,7 +1431,7 @@ Tactic notations allow to customize the syntax of tactics. They have the followi
 
       * - ``hyp``
         - identifier
-        - an hypothesis defined in context
+        - a hypothesis defined in context
         - clear
 
       * - ``reference``
@@ -1503,7 +1503,7 @@ Tactic notations allow to customize the syntax of tactics. They have the followi
 .. [#and_or_levels] which are the levels effectively chosen in the current
    implementation of Coq
 
-.. [#no_associativity] Coq accepts notations declared as non-associative but the parser on
+.. [#no_associativity] Coq accepts notations declared as nonassociative but the parser on
    which Coq is built, namely Camlp5, currently does not implement ``no associativity`` and
    replaces it with ``left associativity``; hence it is the same for Coq: ``no associativity``
    is in fact ``left associativity`` for the purposes of parsing