Add some missing smallcaps.

6 files changed, 100 insertions, 100 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index f18569c7fd..37d12e8ce5 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -8,7 +8,7 @@ This chapter documents the tactic language |Ltac|.
 We start by giving the syntax followed by the informal
 semantics. To learn more about the language and
 especially about its foundations, please refer to :cite:`Del00`.
-(Note the examples in the paper won't work as-is; Coq has evolved
+(Note the examples in the paper won't work as-is; |Coq| has evolved
 since the paper was written.)
 
 .. example:: Basic tactic macros
@@ -41,7 +41,7 @@ higher precedence than `+`.  Usually `a/b/c` is given the :gdef:`left associativ
 interpretation `(a/b)/c` rather than the :gdef:`right associative` interpretation
 `a/(b/c)`.
 
-In Coq, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4`
+In |Coq|, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4`
 is interpreted as :n:`(try (repeat (@tactic__1 || @tactic__2)); @tactic__3); @tactic__4`
 because `||` is part of :token:`ltac_expr2`, which has higher precedence than
 :tacn:`try` and :tacn:`repeat` (at the level of :token:`ltac_expr3`), which
@@ -784,7 +784,7 @@ single success:
 Checking for a single success: exactly_once
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Coq provides an experimental way to check that a tactic has *exactly
+|Coq| provides an experimental way to check that a tactic has *exactly
 one* success:
 
 .. tacn:: exactly_once @ltac_expr3
@@ -813,7 +813,7 @@ one* success:
 Checking for failure: assert_fails
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*:
+|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*:
 
 .. tacn:: assert_fails @ltac_expr3
    :name: assert_fails
@@ -859,7 +859,7 @@ Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*:
 Checking for success: assert_succeeds
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one*
+|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one*
 success:
 
 .. tacn:: assert_succeeds @ltac_expr3
@@ -904,7 +904,7 @@ Failing
 
    See the example for a comparison of the two constructs.
 
-   Note that if Coq terms have to be
+   Note that if |Coq| terms have to be
    printed as part of the failure, term construction always forces the
    tactic into the goals, meaning that if there are no goals when it is
    evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed.
@@ -989,7 +989,7 @@ amount of time:
       timeout with some other tacticals. This tactical is hence proposed only
       for convenience during debugging or other development phases, we strongly
       advise you to not leave any timeout in final scripts. Note also that
-      this tactical isn’t available on the native Windows port of Coq.
+      this tactical isn’t available on the native Windows port of |Coq|.
 
 Timing a tactic
 ~~~~~~~~~~~~~~~
@@ -1884,7 +1884,7 @@ Proving that a list is a permutation of a second list
    From Section :ref:`ltac-syntax` we know that Ltac has a primitive
    notion of integers, but they are only used as arguments for
    primitive tactics and we cannot make computations with them. Thus,
-   instead, we use Coq's natural number type :g:`nat`.
+   instead, we use |Coq|'s natural number type :g:`nat`.
 
    .. coqtop:: in
 
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 773e393eb6..64fc1133f0 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -3,8 +3,8 @@
 Ltac2
 =====
 
-The Ltac tactic language is probably one of the ingredients of the success of
-Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac:
+The |Ltac| tactic language is probably one of the ingredients of the success of
+|Coq|, yet it is at the same time its Achilles' heel. Indeed, |Ltac|:
 
 - has often unclear semantics
 - is very non-uniform due to organic growth
@@ -30,7 +30,7 @@ as Ltac1.
 Current limitations include:
 
 - There are a number of tactics that are not yet supported in Ltac2 because
-  the interface OCaml and/or Ltac2 notations haven't been written.  See
+  the interface |OCaml| and/or Ltac2 notations haven't been written.  See
   :ref:`defining_tactics`.
 
 - Missing usability features such as:
@@ -90,7 +90,7 @@ In particular, Ltac2 is:
   * together with the Hindley-Milner type system
 
 - a language featuring meta-programming facilities for the manipulation of
-  Coq-side terms
+  |Coq|-side terms
 - a language featuring notation facilities to help write palatable scripts
 
 We describe these in more detail in the remainder of this document.
@@ -108,14 +108,14 @@ that ML constitutes a sweet spot in PL design, as it is relatively expressive
 while not being either too lax (unlike dynamic typing) nor too strict
 (unlike, say, dependent types).
 
-The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it
+The main goal of Ltac2 is to serve as a meta-language for |Coq|. As such, it
 naturally fits in the ML lineage, just as the historical ML was designed as
 the tactic language for the LCF prover. It can also be seen as a general-purpose
-language, by simply forgetting about the Coq-specific features.
+language, by simply forgetting about the |Coq|-specific features.
 
 Sticking to a standard ML type system can be considered somewhat weak for a
-meta-language designed to manipulate Coq terms. In particular, there is no
-way to statically guarantee that a Coq term resulting from an Ltac2
+meta-language designed to manipulate |Coq| terms. In particular, there is no
+way to statically guarantee that a |Coq| term resulting from an Ltac2
 computation will be well-typed. This is actually a design choice, motivated
 by backward compatibility with Ltac1. Instead, well-typedness is deferred to
 dynamic checks, allowing many primitive functions to fail whenever they are
@@ -138,7 +138,7 @@ Type Syntax
 ~~~~~~~~~~~
 
 At the level of terms, we simply elaborate on Ltac1 syntax, which is quite
-close to OCaml. Types follow the simply-typed syntax of OCaml.
+close to |OCaml|. Types follow the simply-typed syntax of |OCaml|.
 
 .. insertprodn ltac2_type ltac2_typevar
 
@@ -160,7 +160,7 @@ declarations such as algebraic datatypes and records.
 
 Built-in types include:
 
-- ``int``, machine integers (size not specified, in practice inherited from OCaml)
+- ``int``, machine integers (size not specified, in practice inherited from |OCaml|)
 - ``string``, mutable strings
 - ``'a array``, mutable arrays
 - ``exn``, exceptions
@@ -201,7 +201,7 @@ One can define new types with the following commands.
      :token:`tac2typ_knd` should be in the form :n:`[ {? {? %| } {+| @tac2alg_constructor } } ]`.
 
    Without :n:`{| := | ::= }`
-     Defines an abstract type for use representing data from OCaml.  Not for
+     Defines an abstract type for use representing data from |OCaml|.  Not for
      end users.
 
    :n:`with @tac2typ_def`
@@ -227,9 +227,9 @@ One can define new types with the following commands.
 .. cmd:: Ltac2 @ external @ident : @ltac2_type := @string @string
    :name: Ltac2 external
 
-   Declares abstract terms.  Frequently, these declare OCaml functions
+   Declares abstract terms.  Frequently, these declare |OCaml| functions
    defined in |Coq| and give their type information.  They can also declare
-   data structures from OCaml.  This command has no use for the end user.
+   data structures from |OCaml|.  This command has no use for the end user.
 
 APIs
 ~~~~
@@ -363,7 +363,7 @@ Reduction
 ~~~~~~~~~
 
 We use the usual ML call-by-value reduction, with an otherwise unspecified
-evaluation order. This is a design choice making it compatible with OCaml,
+evaluation order. This is a design choice making it compatible with |OCaml|,
 if ever we implement native compilation. The expected equations are as follows::
 
   (fun x => t) V ≡ t{x := V} (βv)
@@ -407,7 +407,7 @@ standard IO monad as the ambient effectful world, Ltac2 is has a
 tactic monad.
 
 Note that the order of evaluation of application is *not* specified and is
-implementation-dependent, as in OCaml.
+implementation-dependent, as in |OCaml|.
 
 We recall that the `Proofview.tactic` monad is essentially a IO monad together
 with backtracking state representing the proof state.
@@ -537,8 +537,8 @@ aware of bound variables and must use heuristics to decide whether a variable
 is a proper one or referring to something in the Ltac context.
 
 Likewise, in Ltac1, constr parsing is implicit, so that ``foo 0`` is
-not ``foo`` applied to the Ltac integer expression ``0`` (Ltac does have a
-notion of integers, though it is not first-class), but rather the Coq term
+not ``foo`` applied to the Ltac integer expression ``0`` (|Ltac| does have a
+notion of integers, though it is not first-class), but rather the |Coq| term
 :g:`Datatypes.O`.
 
 The implicit parsing is confusing to users and often gives unexpected results.
@@ -570,11 +570,11 @@ Built-in quotations
 The current implementation recognizes the following built-in quotations:
 
 - ``ident``, which parses identifiers (type ``Init.ident``).
-- ``constr``, which parses Coq terms and produces an-evar free term at runtime
+- ``constr``, which parses |Coq| terms and produces an-evar free term at runtime
   (type ``Init.constr``).
-- ``open_constr``, which parses Coq terms and produces a term potentially with
+- ``open_constr``, which parses |Coq| terms and produces a term potentially with
   holes at runtime (type ``Init.constr`` as well).
-- ``pattern``, which parses Coq patterns and produces a pattern used for term
+- ``pattern``, which parses |Coq| patterns and produces a pattern used for term
   matching (type ``Init.pattern``).
 - ``reference``  Qualified names
   are globalized at internalization into the corresponding global reference,
@@ -617,7 +617,7 @@ Term Antiquotations
 Syntax
 ++++++
 
-One can also insert Ltac2 code into Coq terms, similar to what is possible in
+One can also insert Ltac2 code into |Coq| terms, similar to what is possible in
 Ltac1.
 
 .. prodn::
@@ -629,7 +629,7 @@ for their side-effects.
 Semantics
 +++++++++
 
-A quoted Coq term is interpreted in two phases, internalization and
+A quoted |Coq| term is interpreted in two phases, internalization and
 evaluation.
 
 - Internalization is part of the static semantics, that is, it is done at Ltac2
@@ -637,17 +637,17 @@ evaluation.
 - Evaluation is part of the dynamic semantics, that is, it is done when
   a term gets effectively computed by Ltac2.
 
-Note that typing of Coq terms is a *dynamic* process occurring at Ltac2
+Note that typing of |Coq| terms is a *dynamic* process occurring at Ltac2
 evaluation time, and not at Ltac2 typing time.
 
 Static semantics
 ****************
 
-During internalization, Coq variables are resolved and antiquotations are
-type checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq
+During internalization, |Coq| variables are resolved and antiquotations are
+type checked as Ltac2 terms, effectively producing a ``glob_constr`` in |Coq|
 implementation terminology. Note that although it went through the
 type checking of **Ltac2**, the resulting term has not been fully computed and
-is potentially ill-typed as a runtime **Coq** term.
+is potentially ill-typed as a runtime **|Coq|** term.
 
 .. example::
 
@@ -669,7 +669,7 @@ of the corresponding term expression.
       let x := '0 in constr:(1 + ltac2:(exact x))
 
 Beware that the typing environment of antiquotations is **not**
-expanded by the Coq binders from the term.
+expanded by the |Coq| binders from the term.
 
   .. example::
 
@@ -692,17 +692,17 @@ as follows.
 
 `constr:(fun x : nat => ltac2:(exact (hyp @x)))`
 
-This pattern is so common that we provide dedicated Ltac2 and Coq term notations
+This pattern is so common that we provide dedicated Ltac2 and |Coq| term notations
 for it.
 
 - `&x` as an Ltac2 expression expands to `hyp @x`.
-- `&x` as a Coq constr expression expands to
+- `&x` as a |Coq| constr expression expands to
   `ltac2:(Control.refine (fun () => hyp @x))`.
 
-In the special case where Ltac2 antiquotations appear inside a Coq term
+In the special case where Ltac2 antiquotations appear inside a |Coq| term
 notation, the notation variables are systematically bound in the body
 of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents
-untyped syntactic Coq expressions, which can by typed in the
+untyped syntactic |Coq| expressions, which can by typed in the
 current context using the `Ltac2.Constr.pretype` function.
 
 .. example::
@@ -748,9 +748,9 @@ the notation section.
 
 .. prodn:: term += $@lident
 
-In a Coq term, writing :g:`$x` is semantically equivalent to
+In a |Coq| term, writing :g:`$x` is semantically equivalent to
 :g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to
-insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term.
+insert in a concise way an Ltac2 variable of type :n:`constr` into a |Coq| term.
 
 Match over terms
 ~~~~~~~~~~~~~~~~
@@ -1129,7 +1129,7 @@ Match on values
 .. tacn:: match @ltac2_expr5 with {? @ltac2_branches } end
    :name: match (Ltac2)
 
-   Matches a value, akin to the OCaml `match` construct.  By itself, it doesn't cause backtracking
+   Matches a value, akin to the |OCaml| `match` construct.  By itself, it doesn't cause backtracking
    as do the `*match*!` and `*match*! goal` constructs.
 
    .. insertprodn ltac2_branches atomic_tac2pat
@@ -1254,7 +1254,7 @@ Abbreviations
 
    Introduces a special kind of notation, called an abbreviation,
    that does not add any parsing rules. It is similar in
-   spirit to Coq abbreviations (see :cmd:`Notation (abbreviation)`,
+   spirit to |Coq| abbreviations (see :cmd:`Notation (abbreviation)`,
    insofar as its main purpose is to give an
    absolute name to a piece of pure syntax, which can be transparently referred to
    by this name as if it were a proper definition.
@@ -1281,7 +1281,7 @@ Abbreviations
 Defining tactics
 ~~~~~~~~~~~~~~~~
 
-Built-in tactics (those defined in OCaml code in the |Coq| executable) and Ltac1 tactics,
+Built-in tactics (those defined in |OCaml| code in the |Coq| executable) and Ltac1 tactics,
 which are defined in `.v` files, must be defined through notations.  (Ltac2 tactics can be
 defined with :cmd:`Ltac2`.
 
@@ -1795,7 +1795,7 @@ Transition from Ltac1
 Owing to the use of a lot of notations, the transition should not be too
 difficult. In particular, it should be possible to do it incrementally. That
 said, we do *not* guarantee it will be a blissful walk either.
-Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq
+Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with |Coq|
 will help you.
 
 We list the major changes and the transition strategies hereafter.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index edd93f2266..449fc96b5a 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -11,7 +11,7 @@ section. They can also use some other specialized commands called
 *tactics*. They are the very tools allowing the user to deal with
 logical reasoning. They are documented in Chapter :ref:`tactics`.
 
-Coq user interfaces usually have a way of marking whether the user has
+|Coq| user interfaces usually have a way of marking whether the user has
 switched to proof editing mode. For instance, in coqtop the prompt ``Coq <``   is changed into
 :n:`@ident <`   where :token:`ident` is the declared name of the theorem currently edited.
 
@@ -36,7 +36,7 @@ terms are called *proof terms*.
 
 .. exn:: No focused proof.
 
-   Coq raises this error message when one attempts to use a proof editing command
+   |Coq| raises this error message when one attempts to use a proof editing command
    out of the proof editing mode.
 
 .. _proof-editing-mode:
@@ -62,7 +62,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
 
    This command is available in interactive editing proof mode when the
    proof is completed. Then :cmd:`Qed` extracts a proof term from the proof
-   script, switches back to Coq top-level and attaches the extracted
+   script, switches back to |Coq| top-level and attaches the extracted
    proof term to the declared name of the original goal. This name is
    added to the environment as an opaque constant.
 
@@ -675,10 +675,10 @@ Requesting information
 Showing differences between proof steps
 ---------------------------------------
 
-Coq can automatically highlight the differences between successive proof steps
-and between values in some error messages.  Coq can also highlight differences
+|Coq| can automatically highlight the differences between successive proof steps
+and between values in some error messages.  |Coq| can also highlight differences
 in the proof term.
-For example, the following screenshots of CoqIDE and coqtop show the application
+For example, the following screenshots of |CoqIDE| and coqtop show the application
 of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
 The conclusion is entirely in pale green because although it’s changed, no tokens were added
 to it.  The second screenshot uses the "removed" option, so it shows the conclusion a
@@ -714,7 +714,7 @@ new, no line of old text is shown for them.
   .. image:: ../_static/diffs-coqtop-on3.png
      :alt: coqtop with Set Diffs on
 
-This image shows an error message with diff highlighting in CoqIDE:
+This image shows an error message with diff highlighting in |CoqIDE|:
 
 ..
 
@@ -735,21 +735,21 @@ How to enable diffs
 
 For coqtop, showing diffs can be enabled when starting coqtop with the
 ``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option
-within Coq.  You will need to provide the ``-color on|auto`` command-line option when
+within |Coq|.  You will need to provide the ``-color on|auto`` command-line option when
 you start coqtop in either case.
 
 Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment
 variable.  See section :ref:`customization-by-environment-variables`.  Diffs
 use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``.
 
-In CoqIDE, diffs should be enabled from the ``View`` menu.  Don’t use the ``Set Diffs``
-command in CoqIDE.  You can change the background colors shown for diffs from the
+In |CoqIDE|, diffs should be enabled from the ``View`` menu.  Don’t use the ``Set Diffs``
+command in |CoqIDE|.  You can change the background colors shown for diffs from the
 ``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``,
 ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags.  This panel also
 lets you control other attributes of the highlights, such as the foreground
 color, bold, italic, underline and strikeout.
 
-As of June 2019, Proof General can also display Coq-generated proof diffs automatically.
+As of June 2019, Proof General can also display |Coq|-generated proof diffs automatically.
 Please see the PG documentation section
 "`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_)
 for details.
@@ -840,7 +840,7 @@ To show differences in the proof term:
 
 - In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command.
 
-- In CoqIDE, position the cursor on or just after a tactic to compare the proof term
+- In |CoqIDE|, position the cursor on or just after a tactic to compare the proof term
   after the tactic with the proof term before the tactic, then select
   `View / Show Proof` from the menu or enter the associated key binding.
   Differences will be shown applying the current `Show Diffs` setting
@@ -872,10 +872,10 @@ Controlling the effect of proof editing commands
 
    When turned on (it is off by default), this flag enables support for nested
    proofs: a new assertion command can be inserted before the current proof is
-   finished, in which case Coq will temporarily switch to the proof of this
+   finished, in which case |Coq| will temporarily switch to the proof of this
    *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed`
    or :cmd:`Defined`), its statement will be made available (as if it had been
-   proved before starting the previous proof) and Coq will switch back to the
+   proved before starting the previous proof) and |Coq| will switch back to the
    proof of the previous assertion.
 
 .. flag:: Printing Goal Names
@@ -892,7 +892,7 @@ Controlling memory usage
    Prints heap usage statistics, which are values from the `stat` type of the `Gc` module
    described
    `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_
-   in the OCaml documentation.
+   in the |OCaml| documentation.
    The `live_words`, `heap_words` and `top_heap_words` values give the basic information.
    Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables.
 
@@ -907,7 +907,7 @@ to force |Coq| to optimize some of its internal data structures.
 .. cmd:: Optimize Heap
 
    Perform a heap compaction.  This is generally an expensive operation.
-   See: `OCaml Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
+   See: `|OCaml| Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
    There is also an analogous tactic :tacn:`optimize_heap`.
 
 Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>`
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index ca50a02562..770de9a6c3 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -158,23 +158,23 @@ compatible with the rest of |Coq|, up to a few discrepancies:
   generalized form, turn off the |SSR| Boolean ``if`` notation using the command:
   ``Close Scope boolean_if_scope``.
 + The following flags can be unset to make |SSR| more compatible with
-  parts of Coq:
+  parts of |Coq|:
 
 .. flag:: SsrRewrite
 
    Controls whether the incompatible rewrite syntax is enabled (the default).
-   Disabling the flag makes the syntax compatible with other parts of Coq.
+   Disabling the flag makes the syntax compatible with other parts of |Coq|.
 
 .. flag:: SsrIdents
 
    Controls whether tactics can refer to |SSR|-generated variables that are
    in the form _xxx_.  Scripts with explicit references to such variables
    are fragile; they are prone to failure if the proof is later modified or
-   if the details of variable name generation change in future releases of Coq.
+   if the details of variable name generation change in future releases of |Coq|.
 
    The default is on, which gives an error message when the user tries to
    create such identifiers.  Disabling the flag generates a warning instead,
-   increasing compatibility with other parts of Coq.
+   increasing compatibility with other parts of |Coq|.
 
 |Gallina| extensions
 --------------------
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4b1f312105..e8938fdd47 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -173,11 +173,11 @@ The :n:`eqn:` construct in various tactics uses :n:`@naming_intropattern`.
 Use these elementary patterns to specify a name:
 
 * :n:`@ident` — use the specified name
-* :n:`?` — let Coq choose a name
+* :n:`?` — let |Coq| choose a name
 * :n:`?@ident` — generate a name that begins with :n:`@ident`
 * :n:`_` — discard the matched part (unless it is required for another
   hypothesis)
-* if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name
+* if a disjunction pattern omits a name, such as :g:`[|H2]`, |Coq| will choose a name
 
 **Splitting patterns**
 
@@ -849,7 +849,7 @@ Applying theorems
 
 .. flag:: Universal Lemma Under Conjunction
 
-   This flag, which preserves compatibility with versions of Coq prior to
+   This flag, which preserves compatibility with versions of |Coq| prior to
    8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply … in`).
 
 .. tacn:: apply @term in @ident
@@ -1299,7 +1299,7 @@ Managing the local context
    .. tacv:: set @term {? in @goal_occurrences }
 
       This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }`
-      but :token:`ident` is generated by Coq.
+      but :token:`ident` is generated by |Coq|.
 
    .. tacv:: eset (@ident {* @binder } := @term) {? in @goal_occurrences }
              eset @term {? in @goal_occurrences }
@@ -1344,7 +1344,7 @@ Managing the local context
    .. tacv:: pose @term
 
       This behaves as :n:`pose (@ident := @term)` but :token:`ident` is
-      generated by Coq.
+      generated by |Coq|.
 
    .. tacv:: epose (@ident {* @binder } := @term)
              epose @term
@@ -1406,7 +1406,7 @@ Controlling the proof flow
    .. tacv:: assert @type
 
       This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is
-      generated by Coq.
+      generated by |Coq|.
 
    .. tacv:: assert @type by @tactic
 
@@ -1486,7 +1486,7 @@ Controlling the proof flow
 .. tacv:: enough @type
 
    This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of
-   the hypothesis generated by Coq.
+   the hypothesis generated by |Coq|.
 
 .. tacv:: enough @type as @simple_intropattern
 
@@ -1611,7 +1611,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
              must have given the name explicitly (see :ref:`Existential-Variables`).
 
    .. note:: When you are referring to hypotheses which you did not name
-             explicitly, be aware that Coq may make a different decision on how to
+             explicitly, be aware that |Coq| may make a different decision on how to
              name the variable in the current goal and in the context of the
              existential variable. This can lead to surprising behaviors.
 
@@ -1765,7 +1765,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       between :token:`term` and the value that it takes in each of the
       possible cases. The name of the equation is specified
       by :token:`naming_intropattern` (see :tacn:`intros`),
-      in particular ``?`` can be used to let Coq generate a fresh name.
+      in particular ``?`` can be used to let |Coq| generate a fresh name.
 
    .. tacv:: destruct @term with @bindings_list
 
@@ -2359,7 +2359,7 @@ and an explanation of the underlying technique.
    ``inversion`` generally behaves in a slightly more expectable way than
    ``inversion`` (no artificial duplication of some hypotheses referring to
    other hypotheses). To take benefit of these improvements, it is enough to use
-   ``inversion ... as []``, letting the names being finally chosen by Coq.
+   ``inversion ... as []``, letting the names being finally chosen by |Coq|.
 
    .. example::
 
@@ -3029,7 +3029,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    These parameterized reduction tactics apply to any goal and perform
    the normalization of the goal according to the specified flags. In
-   correspondence with the kinds of reduction considered in Coq namely
+   correspondence with the kinds of reduction considered in |Coq| namely
    :math:`\beta` (reduction of functional application), :math:`\delta`
    (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`),
    :math:`\iota` (reduction of
@@ -3111,8 +3111,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
 .. tacv:: native_compute
    :name: native_compute
 
-   This tactic evaluates the goal by compilation to OCaml as described
-   in :cite:`FullReduction`. If Coq is running in native code, it can be
+   This tactic evaluates the goal by compilation to |OCaml| as described
+   in :cite:`FullReduction`. If |Coq| is running in native code, it can be
    typically two to five times faster than :tacn:`vm_compute`. Note however that the
    compilation cost is higher, so it is worth using only for intensive
    computations.
@@ -4024,14 +4024,14 @@ automatically created.
         ``typeclass_instances`` hint database.
 
 
-Hint databases defined in the Coq standard library
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Hint databases defined in the |Coq| standard library
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Several hint databases are defined in the Coq standard library. The
+Several hint databases are defined in the |Coq| standard library. The
 actual content of a database is the collection of hints declared
 to belong to this database in each of the various modules currently
 loaded. Especially, requiring new modules may extend the database.
-At Coq startup, only the core database is nonempty and can be used.
+At |Coq| startup, only the core database is nonempty and can be used.
 
 :core: This special database is automatically used by ``auto``, except when
        pseudo-database ``nocore`` is given to ``auto``. The core database
@@ -4152,7 +4152,7 @@ but this is a mere workaround and has some limitations (for instance, external
 hints cannot be removed).
 
 A proper way to fix this issue is to bind the hints to their module scope, as
-for most of the other objects Coq uses. Hints should only be made available when
+for most of the other objects |Coq| uses. Hints should only be made available when
 the module they are defined in is imported, not just required. It is very
 difficult to change the historical behavior, as it would break a lot of scripts.
 We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior`
@@ -4408,7 +4408,7 @@ some incompatibilities.
 .. exn:: I don’t know how to handle dependent equality.
 
   The decision procedure managed to find a proof of the goal or of a
-  discriminable equality but this proof could not be built in Coq because of
+  discriminable equality but this proof could not be built in |Coq| because of
   dependently-typed functions.
 
 .. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms.
@@ -4855,14 +4855,14 @@ Proof maintenance
 
 *Experimental.*  Many tactics, such as :tacn:`intros`, can automatically generate names, such
 as "H0" or "H1" for a new hypothesis introduced from a goal.  Subsequent proof steps
-may explicitly refer to these names.  However, future versions of Coq may not assign
+may explicitly refer to these names.  However, future versions of |Coq| may not assign
 names exactly the same way, which could cause the proof to fail because the
 new names don't match the explicit references in the proof.
 
 The following "Mangle Names" settings let users find all the
 places where proofs rely on automatically generated names, which can
 then be named explicitly to avoid any incompatibility.  These
-settings cause Coq to generate different names, producing errors for
+settings cause |Coq| to generate different names, producing errors for
 references to automatically generated names.
 
 .. flag:: Mangle Names
@@ -4884,7 +4884,7 @@ Performance-oriented tactic variants
    For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization,
    it skips checking that :n:`@term` is convertible to the goal.
 
-   Recall that the Coq kernel typechecks proofs again when they are concluded to
+   Recall that the |Coq| kernel typechecks proofs again when they are concluded to
    ensure safety. Hence, using :tacn:`change` checks convertibility twice
    overall, while :tacn:`change_no_check` can produce ill-typed terms,
    but checks convertibility only once.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 6c07253bce..a684afad09 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -637,10 +637,10 @@ file is a particular case of a module called a *library file*.
 
 .. cmd:: Declare ML Module {+ @string }
 
-   This commands dynamically loads OCaml compiled code from
+   This commands dynamically loads |OCaml| compiled code from
    a :n:`.mllib` file.
    It is used to load plugins dynamically.  The
-   files must be accessible in the current OCaml loadpath (see the
+   files must be accessible in the current |OCaml| loadpath (see the
    command :cmd:`Add ML Path`).  The :n:`.mllib` suffix may be omitted.
 
    This command is reserved for plugin developers, who should provide
@@ -656,7 +656,7 @@ file is a particular case of a module called a *library file*.
 
 .. cmd:: Print ML Modules
 
-   This prints the name of all OCaml modules loaded with :cmd:`Declare ML Module`.
+   This prints the name of all |OCaml| modules loaded with :cmd:`Declare ML Module`.
    To know from where these module were loaded, the user
    should use the command :cmd:`Locate File`.
 
@@ -719,13 +719,13 @@ the toplevel, and using them in source files is discouraged.
 
 .. cmd:: Add ML Path @string
 
-   This command adds the path :n:`@string` to the current OCaml
+   This command adds the path :n:`@string` to the current |OCaml|
    loadpath (cf. :cmd:`Declare ML Module`).
 
 
 .. cmd:: Print ML Path
 
-   This command displays the current OCaml loadpath. This
+   This command displays the current |OCaml| loadpath. This
    command makes sense only under the bytecode version of ``coqtop``, i.e.
    using option ``-byte``
    (cf. :cmd:`Declare ML Module`).
@@ -794,10 +794,10 @@ Quitting and debugging
 
 .. cmd:: Drop
 
-   This command temporarily enters the OCaml toplevel.
+   This command temporarily enters the |OCaml| toplevel.
    It is a debug facility used by |Coq|’s implementers.  Valid only in the
    bytecode version of coqtop.
-   The OCaml command:
+   The |OCaml| command:
 
    ::
 
@@ -1230,15 +1230,15 @@ in support libraries of plug-ins.
 
 .. _exposing-constants-to-ocaml-libraries:
 
-Exposing constants to OCaml libraries
-`````````````````````````````````````
+Exposing constants to |OCaml| libraries
+```````````````````````````````````````
 
 .. cmd:: Register @qualid__1 as @qualid__2
 
-   Makes the constant :n:`@qualid__1` accessible to OCaml libraries under
+   Makes the constant :n:`@qualid__1` accessible to |OCaml| libraries under
    the name :n:`@qualid__2`.  The constant can then be dynamically located
-   in OCaml code by
-   calling :n:`Coqlib.lib_ref "@qualid__2"`.  The OCaml code doesn't need
+   in |OCaml| code by
+   calling :n:`Coqlib.lib_ref "@qualid__2"`.  The |OCaml| code doesn't need
    to know where the constant is defined (what file, module, library, etc.).
 
    As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`,
@@ -1267,7 +1267,7 @@ Registering primitive operations
 
 .. cmd:: Primitive @ident_decl {? : @term } := #@ident
 
-   Makes the primitive type or primitive operator :n:`#@ident` defined in OCaml
+   Makes the primitive type or primitive operator :n:`#@ident` defined in |OCaml|
    accessible in |Coq| commands and tactics.
    For internal use by implementors of |Coq|'s standard library or standard library
    replacements.  No space is allowed after the `#`.  Invalid values give a syntax