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.

6 files changed, 99 insertions, 93 deletions

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: