Add some missing smallcaps.

43 files changed, 484 insertions, 484 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index c2249b8e57..1ca85e7e17 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -16,7 +16,7 @@ Before using any of the commands or options described in this chapter,
 the extraction framework should first be loaded explicitly
 via ``Require Extraction``, or via the more robust
 ``From Coq Require Extraction``.
-Note that in earlier versions of Coq, these commands and options were
+Note that in earlier versions of |Coq|, these commands and options were
 directly available without any preliminary ``Require``.
 
 .. coqtop:: in
@@ -72,10 +72,10 @@ produce one monolithic file or one file per |Coq| library.
    Recursive extraction of all the mentioned objects and all
    their dependencies, just as :n:`Extraction @string {+ @qualid }`,
    but instead of producing one monolithic file, this command splits
-   the produced code in separate ML files, one per corresponding Coq
+   the produced code in separate ML files, one per corresponding |Coq|
    ``.v`` file. This command is hence quite similar to
    :cmd:`Recursive Extraction Library`, except that only the needed
-   parts of Coq libraries are extracted instead of the whole.
+   parts of |Coq| libraries are extracted instead of the whole.
    The naming convention in case of name clash is the same one as
    :cmd:`Extraction Library`: identifiers are here renamed using prefixes
    ``coq_``  or ``Coq_``.
@@ -138,7 +138,7 @@ and commands:
    Default is on. This controls all type-preserving optimizations made on
    the ML terms (mostly reduction of dummy beta/iota redexes, but also
    simplifications on Cases, etc). Turn this flag off if you want a
-   ML term as close as possible to the Coq term.
+   ML term as close as possible to the |Coq| term.
 
 .. flag:: Extraction Conservative Types
 
@@ -434,7 +434,7 @@ Additional settings
 
    Controls which optimizations are used during extraction, providing a finer-grained
    control than :flag:`Extraction Optimize`.  The bits of :token:`natural` are used as a bit mask.
-   Keeping an option off keeps the extracted ML more similar to the Coq term.
+   Keeping an option off keeps the extracted ML more similar to the |Coq| term.
    Values are:
 
    +-----+-------+----------------------------------------------------------------+
@@ -465,7 +465,7 @@ Additional settings
 
 .. flag:: Extraction TypeExpand
 
-   If set, fully expand Coq types in ML.  See the Coq source code to learn more.
+   If set, fully expand |Coq| types in ML.  See the |Coq| source code to learn more.
 
 Differences between |Coq| and ML type systems
 ----------------------------------------------
@@ -515,7 +515,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
-from a Coq well-typed terms, so for example inductive types will always 
+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
 of the right shape (from the |Coq| point-of-view).
@@ -524,7 +524,7 @@ More details about the correctness of the extracted programs can be
 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|
+occur. For example all the programs of |Coq| library are accepted by the |OCaml|
 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 759f630b85..fdc349e0d8 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -35,7 +35,7 @@ the previous implementation in several ways:
   the new implementation, if one provides the proper morphisms. Again,
   most of the work is handled in the tactics.
 + First-class morphisms and signatures. Signatures and morphisms are
-  ordinary Coq terms, hence they can be manipulated inside Coq, put
+  ordinary |Coq| terms, hence they can be manipulated inside |Coq|, put
   inside structures and lemmas about them can be proved inside the
   system. Higher-order morphisms are also allowed.
 + Performance. The implementation is based on a depth-first search for
@@ -103,7 +103,7 @@ argument.
 Morphisms can also be contravariant in one or more of their arguments.
 A morphism is contravariant on an argument associated to the relation
 instance :math:`R` if it is covariant on the same argument when the inverse
-relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->``
+relation :math:`R^{−1}` (``inverse R`` in |Coq|) is considered. The special arrow ``-->``
 is used in signatures for contravariant morphisms.
 
 Functions having arguments related by symmetric relations instances
@@ -144,7 +144,7 @@ always the intended equality for a given structure.
 
 In the next section we will describe the commands to register terms as
 parametric relations and morphisms. Several tactics that deal with
-equality in Coq can also work with the registered relations. The exact
+equality in |Coq| can also work with the registered relations. The exact
 list of tactics will be given :ref:`in this section <tactics-enabled-on-user-provided-relations>`.
 For instance, the tactic reflexivity can be used to solve a goal ``R n n`` whenever ``R``
 is an instance of a registered reflexive relation. However, the
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index ba5bac6489..d184eafac9 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -260,7 +260,7 @@ proof by abstracting monomials by variables.
    that might miss a refutation.
 
    To illustrate the working of the tactic, consider we wish to prove the
-   following Coq goal:
+   following |Coq| goal:
 
 .. needs csdp
 .. coqdoc::
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index e1b1ee8e8d..35f087d47d 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -9,7 +9,7 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic
 
    The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia`
    tactic.  The goal is to consolidate the arithmetic solving
-   capabilities of Coq into a single engine; moreover, :tacn:`lia` is
+   capabilities of |Coq| into a single engine; moreover, :tacn:`lia` is
    in general more powerful than :tacn:`omega` (it is a complete
    Presburger arithmetic solver while :tacn:`omega` was known to be
    incomplete).
@@ -143,7 +143,7 @@ Options
 
    .. deprecated:: 8.5
 
-   This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It
+   This deprecated flag (on by default) is for compatibility with |Coq| pre 8.5. It
    resets internal name counters to make executions of :tacn:`omega` independent.
 
 .. flag:: Omega UseLocalDefs
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index c6a4b4fe1a..0fd66d07db 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -22,7 +22,7 @@ complete |Coq| term. |Program| replaces the |Program| tactic by Catherine
 Parent :cite:`Parent95b` which had a similar goal but is no longer maintained.
 
 The languages available as input are currently restricted to |Coq|’s
-term language, but may be extended to OCaml, Haskell and
+term language, but may be extended to |OCaml|, Haskell and
 others in the future. We use the same syntax as |Coq| and permit to use
 implicit arguments and the existing coercion mechanism. Input terms
 and types are typed in an extended system (Russell) and interpreted
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index cda8a1b679..9f839364b6 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -99,7 +99,7 @@ Yes, building the variables map and doing the substitution after
 normalizing is automatically done by the tactic. So you can just
 forget this paragraph and use the tactic according to your intuition.
 
-Concrete usage in Coq
+Concrete usage in |Coq|
 --------------------------
 
 .. tacn:: ring {? [ {+ @term } ] }
@@ -433,10 +433,10 @@ How does it work?
 
 The code of ``ring`` is a good example of a tactic written using *reflection*.
 What is reflection? Basically, using it means that a part of a tactic is written
-in Gallina, Coq's language of terms, rather than |Ltac| or |OCaml|. From the
+in Gallina, |Coq|'s language of terms, rather than |Ltac| or |OCaml|. From the
 philosophical point of view, reflection is using the ability of the Calculus of
 Constructions to speak and reason about itself. For the ``ring`` tactic we used
-Coq as a programming language and also as a proof environment to build a tactic
+|Coq| as a programming language and also as a proof environment to build a tactic
 and to prove its correctness.
 
 The interested reader is strongly advised to have a look at the
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index d533470f22..8cbc436ab7 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -13,7 +13,7 @@ Class and Instance declarations
 -------------------------------
 
 The syntax for class and instance declarations is the same as the record
-syntax of Coq:
+syntax of |Coq|:
 
 .. coqdoc::
 
@@ -61,7 +61,7 @@ Note that if you finish the proof with :cmd:`Qed` the entire instance
 will be opaque, including the fields given in the initial term.
 
 Alternatively, in :flag:`Program Mode` if one does not give all the
-members in the Instance declaration, Coq generates obligations for the
+members in the Instance declaration, |Coq| generates obligations for the
 remaining fields, e.g.:
 
 .. coqtop:: in
@@ -242,7 +242,7 @@ binders. For example:
    Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y).
 
 The ``!`` modifier switches the way a binder is parsed back to the usual
-interpretation of Coq. In particular, it uses the implicit arguments
+interpretation of |Coq|. In particular, it uses the implicit arguments
 mechanism if available, as shown in the example.
 
 Substructures
@@ -511,13 +511,13 @@ Settings
    This flag (off by default) respects the dependency order
    between subgoals, meaning that subgoals on which other subgoals depend
    come first, while the non-dependent subgoals were put before
-   the dependent ones previously (Coq 8.5 and below). This can result in
+   the dependent ones previously (|Coq| 8.5 and below). This can result in
    quite different performance behaviors of proof search.
 
 
 .. flag:: Typeclasses Filtered Unification
 
-   This flag, available since Coq 8.6 and off by default, switches the
+   This flag, available since |Coq| 8.6 and off by default, switches the
    hint application procedure to a filter-then-unify strategy. To apply a
    hint, we first check that the goal *matches* syntactically the
    inferred or specified pattern of the hint, and only then try to
diff --git a/doc/sphinx/appendix/history-and-changes/index.rst b/doc/sphinx/appendix/history-and-changes/index.rst
index 50ffec8e3f..b00a7cdb08 100644
--- a/doc/sphinx/appendix/history-and-changes/index.rst
+++ b/doc/sphinx/appendix/history-and-changes/index.rst
@@ -5,10 +5,10 @@ History and recent changes
 ==========================
 
 This chapter is divided in two parts.  The first one is about the
-:ref:`early history of Coq <history>` and is presented in
+:ref:`early history of |Coq| <history>` and is presented in
 chronological order.  The second one provides :ref:`release notes
-about recent versions of Coq <changes>` and is presented in reverse
-chronological order.  When updating your copy of Coq to a new version
+about recent versions of |Coq| <changes>` and is presented in reverse
+chronological order.  When updating your copy of |Coq| to a new version
 (especially a new major version), it is strongly recommended that you
 read the corresponding release notes.  They may contain advice that
 will help you understand the differences with the previous version and
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index af66efa95e..401c7d4381 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -34,10 +34,10 @@ The main changes include:
   this takes precedence over the now deprecated :ref:`ssreflect search<812SSRSearch>`.
 - Many additions and improvements of the :ref:`standard library<812Stdlib>`.
 - Improvements to the :ref:`reference manual<812Refman>` include a more logical organization
-  of chapters along with updated syntax descriptions that match Coq's grammar
+  of chapters along with updated syntax descriptions that match |Coq|'s grammar
   in most but not all chapters.
 
-Additionally, the :tacn:`omega` tactic is deprecated in this version of Coq,
+Additionally, the :tacn:`omega` tactic is deprecated in this version of |Coq|,
 and we recommend users to switch to :tacn:`lia` in new proof scripts (see
 also the warning message in the :ref:`corresponding chapter
 <omega_chapter>`).
@@ -46,7 +46,7 @@ See the `Changes in 8.12+beta1`_ section and following sections for the
 detailed list of changes, including potentially breaking changes marked
 with **Changed**.
 
-Coq's documentation is available at https://coq.github.io/doc/v8.12/refman (reference
+|Coq|'s documentation is available at https://coq.github.io/doc/v8.12/refman (reference
 manual), and https://coq.github.io/doc/v8.12/stdlib (documentation of
 the standard library). Developer documentation of the ML API is available
 at https://coq.github.io/doc/v8.12/api.
@@ -55,8 +55,8 @@ Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael
 Soegtrop and Théo Zimmermann worked on maintaining and improving the
 continuous integration system and package building infrastructure.
 
-Erik Martin-Dorel has maintained the `Coq Docker images
-<https://hub.docker.com/r/coqorg/coq>`_ that are used in many Coq
+Erik Martin-Dorel has maintained the `|Coq| Docker images
+<https://hub.docker.com/r/coqorg/coq>`_ that are used in many |Coq|
 projects for continuous integration.
 
 The OPAM repository for |Coq| packages has been maintained by
@@ -64,7 +64,7 @@ Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with
 contributions from many users. A list of packages is available at
 https://coq.inria.fr/opam/www/.
 
-Previously, most components of Coq had a single principal maintainer.
+Previously, most components of |Coq| had a single principal maintainer.
 This was changed in 8.12 (`#11295
 <https://github.com/coq/coq/pull/11295>`_) so that every component now has
 a team of maintainers, who are in charge of reviewing and
@@ -99,12 +99,12 @@ Nickolai Zeldovich and Théo Zimmermann.
 Many power users helped to improve the design of this new version via
 the GitHub issue and pull request system, the |Coq| development mailing list
 coqdev@inria.fr, the coq-club@inria.fr mailing list, the `Discourse forum
-<https://coq.discourse.group/>`_ and the new `Coq Zulip chat <http://coq.zulipchat.com>`_
+<https://coq.discourse.group/>`_ and the new `|Coq| Zulip chat <http://coq.zulipchat.com>`_
 (thanks to Cyril Cohen for organizing the move from Gitter).
 
 Version 8.12's development spanned 6 months from the release of
 |Coq| 8.11.0. Emilio Jesus Gallego Arias and Théo Zimmermann are
-the release managers of Coq 8.12. This release is the result of
+the release managers of |Coq| 8.12. This release is the result of
 ~500 PRs merged, closing ~100 issues.
 
 | Nantes, June 2020,
@@ -131,7 +131,7 @@ Specification language, type inference
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 - **Changed:**
-  The deprecation warning raised since Coq 8.10 when a trailing
+  The deprecation warning raised since |Coq| 8.10 when a trailing
   implicit is declared to be non-maximally inserted (with the command
   :cmd:`Arguments`) has been turned into an error
   (`#11368 <https://github.com/coq/coq/pull/11368>`_,
@@ -432,7 +432,7 @@ Tactics
   fixes `#12210 <https://github.com/coq/coq/issues/12210>`_).
 - **Fixed:**
   :tacn:`zify` now handles :g:`Z.pow_pos` by default.
-  In Coq 8.11, this was the case only when loading module
+  In |Coq| 8.11, this was the case only when loading module
   :g:`ZifyPow` because this triggered a regression of :tacn:`lia`.
   The regression is now fixed, and the module kept only for compatibility
   (`#11362 <https://github.com/coq/coq/pull/11362>`_,
@@ -532,7 +532,7 @@ Flags, options and attributes
   by Emilio Jesus Gallego Arias).
 - **Removed:**
   Unqualified ``polymorphic``, ``monomorphic``, ``template``,
-  ``notemplate`` attributes (they were deprecated since Coq 8.10).
+  ``notemplate`` attributes (they were deprecated since |Coq| 8.10).
   Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
   :attr:`universes(template)` and :attr:`universes(notemplate)` instead
   (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann).
@@ -676,7 +676,7 @@ Tools
   involving ``%``) (`#12126
   <https://github.com/coq/coq/pull/12126>`_, by Jason Gross).
 - **Changed:**
-  When passing ``TIMED=1`` to ``make`` with either Coq's own makefile
+  When passing ``TIMED=1`` to ``make`` with either |Coq|'s own makefile
   or a ``coq_makefile``\-made makefile, timing information is now
   printed for OCaml files as well (`#12211
   <https://github.com/coq/coq/pull/12211>`_, by Jason Gross).
@@ -701,7 +701,7 @@ Tools
   <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert).
 - **Added:**
   A new documentation environment ``details`` to make certain portion
-  of a Coq document foldable.  See :ref:`coqdoc-hide-show`
+  of a |Coq| document foldable.  See :ref:`coqdoc-hide-show`
   (`#10592 <https://github.com/coq/coq/pull/10592>`_,
   by Thomas Letan).
 - **Added:**
@@ -726,7 +726,7 @@ Tools
   ``--user``) to ``make`` (`#11302
   <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
 - **Added:**
-  Coq's build system now supports both ``TIMING_FUZZ``,
+  |Coq|'s build system now supports both ``TIMING_FUZZ``,
   ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile``
   made by ``coq_makefile`` (`#11302
   <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
@@ -742,7 +742,7 @@ Tools
   ``TIMING_SORT_BY_MEM=1`` (to pass ``--sort-by-mem``) to ``make``
   (`#11606 <https://github.com/coq/coq/pull/11606>`_, by Jason Gross).
 - **Added:**
-  Coq's build system now supports both ``TIMING_INCLUDE_MEM`` and
+  |Coq|'s build system now supports both ``TIMING_INCLUDE_MEM`` and
   ``TIMING_SORT_BY_MEM`` just like a ``Makefile`` made by
   ``coq_makefile`` (`#11606 <https://github.com/coq/coq/pull/11606>`_,
   by Jason Gross).
@@ -765,7 +765,7 @@ Tools
   (`#12091 <https://github.com/coq/coq/pull/12091>`_,
   by Hugo Herbelin).
 - **Fixed:**
-  The various timing targets for Coq's standard library now correctly
+  The various timing targets for |Coq|'s standard library now correctly
   display and label the "before" and "after" columns, rather than
   mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_
   fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason
@@ -799,15 +799,15 @@ Tools
   <https://github.com/coq/coq/pull/12388>`_, fixes `#12387
   <https://github.com/coq/coq/pull/12387>`_, by Jason Gross).
 
-CoqIDE
-^^^^^^
+|CoqIDE|
+^^^^^^^^
 
 - **Removed:**
-  "Tactic" menu from CoqIDE which had been unmaintained for a number of years
+  "Tactic" menu from |CoqIDE| which had been unmaintained for a number of years
   (`#11414 <https://github.com/coq/coq/pull/11414>`_,
   by Pierre-Marie Pédrot).
 - **Removed:**
-  "Revert all buffers" command from CoqIDE which had been broken for a long time
+  "Revert all buffers" command from |CoqIDE| which had been broken for a long time
   (`#11415 <https://github.com/coq/coq/pull/11415>`_,
   by Pierre-Marie Pédrot).
 
@@ -1038,7 +1038,7 @@ Extraction
 
 - **Added:**
   Support for better extraction of strings in OCaml and Haskell:
-  `ExtOcamlNativeString` provides bindings from the Coq `String` type to
+  `ExtOcamlNativeString` provides bindings from the |Coq| `String` type to
   the OCaml `string` type, and string literals can be extracted to literals,
   both in OCaml and Haskell (`#10486
   <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from
@@ -1063,7 +1063,7 @@ Reference manual
   organization.  In the new version, there are fewer top-level
   chapters, and, in the HTML format, chapters are split into smaller
   pages.  This is still a work in progress and further restructuring
-  is expected in the next versions of Coq
+  is expected in the next versions of |Coq|
   (`CEP#43 <https://github.com/coq/ceps/pull/43>`_, implemented in
   `#11601 <https://github.com/coq/coq/pull/11601>`_,
   `#11871 <https://github.com/coq/coq/pull/11871>`_,
@@ -1076,7 +1076,7 @@ Reference manual
   help and reviews of Jim Fehrle, Clément Pit-Claudel and others).
 - **Changed:**
   Most of the grammar is now presented using the notation mechanism
-  that has been used to present commands and tactics since Coq 8.8 and
+  that has been used to present commands and tactics since |Coq| 8.8 and
   which is documented in :ref:`syntax-conventions`
   (`#11183 <https://github.com/coq/coq/pull/11183>`_,
   `#11314 <https://github.com/coq/coq/pull/11314>`_,
@@ -1201,9 +1201,9 @@ Changes in 8.12.0
   fixes `#11970 <https://github.com/coq/coq/issues/11970>`_,
   by Pierre-Marie Pédrot).
 
-**CoqIDE**
+**|CoqIDE|**
 
-- **Fixed:** CoqIDE no longer exits when trying to open a file whose name is not a valid identifier
+- **Fixed:** |CoqIDE| no longer exits when trying to open a file whose name is not a valid identifier
   (`#12562 <https://github.com/coq/coq/pull/12562>`_,
   fixes `#10988 <https://github.com/coq/coq/issues/10988>`_,
   by Vincent Laporte).
@@ -1250,7 +1250,7 @@ The main changes brought by |Coq| version 8.11 are:
   instances of the constructive and classical real numbers.
 
 Additionally, while the :tacn:`omega` tactic is not yet deprecated in
-this version of Coq, it should soon be the case and we already
+this version of |Coq|, it should soon be the case and we already
 recommend users to switch to :tacn:`lia` in new proof scripts (see
 also the warning message in the :ref:`corresponding chapter
 <omega_chapter>`).
@@ -1260,7 +1260,7 @@ of |Coq| and affected releases. See the `Changes in 8.11+beta1`_
 section and following sections for the detailed list of changes,
 including potentially breaking changes marked with **Changed**.
 
-Coq's documentation is available at https://coq.github.io/doc/v8.11/api (documentation of
+|Coq|'s documentation is available at https://coq.github.io/doc/v8.11/api (documentation of
 the ML API), https://coq.github.io/doc/v8.11/refman (reference
 manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of
 the standard library).
@@ -1322,7 +1322,7 @@ Changes in 8.11+beta1
   computation. Primitive floats are added in the language of terms,
   following the binary64 format of the IEEE 754 standard, and the
   related operations are implemented for the different reduction
-  engines of Coq by using the corresponding processor operators in
+  engines of |Coq| by using the corresponding processor operators in
   rounding-to-nearest-even. The properties of these operators are
   axiomatized in the theory :g:`Coq.Floats.FloatAxioms` which is part
   of the library :g:`Coq.Floats.Floats`.
@@ -1415,7 +1415,7 @@ Changes in 8.11+beta1
   Output of the :cmd:`Print` and :cmd:`About` commands.
   Arguments meta-data is now displayed as the corresponding
   :cmd:`Arguments` command instead of the
-  human-targeted prose used in previous Coq versions. (`#10985
+  human-targeted prose used in previous |Coq| versions. (`#10985
   <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert).
 
   .. _811RefineInstance:
@@ -1514,7 +1514,7 @@ Changes in 8.11+beta1
 
 - **Added:**
   Ltac2, a new version of the tactic language Ltac, that doesn't
-  preserve backward compatibility, has been integrated in the main Coq
+  preserve backward compatibility, has been integrated in the main |Coq|
   distribution.  It is still experimental, but we already recommend
   users of advanced Ltac to start using it and report bugs or request
   enhancements.  See its documentation in the :ref:`dedicated chapter
@@ -1543,14 +1543,14 @@ Changes in 8.11+beta1
   Generalize tactics :tacn:`under` and :tacn:`over` for any registered
   relation. More precisely, assume the given context lemma has type
   `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`.  The
-  first step performed by :tacn:`under` (since Coq 8.10) amounts to
+  first step performed by :tacn:`under` (since |Coq| 8.10) amounts to
   calling the tactic :tacn:`rewrite <rewrite (ssreflect)>`, which
   itself relies on :tacn:`setoid_rewrite` if need be. So this step was
   already compatible with a double implication or setoid equality for
   the conclusion head symbol `R2`. But a further step consists in
   tagging the generated subgoal `R1 (f1 i) (?f2 i)` to protect it from
   unwanted evar instantiation, and get `Under_rel _ R1 (f1 i) (?f2 i)`
-  that is displayed as ``'Under[ f1 i ]``. In Coq 8.10, this second
+  that is displayed as ``'Under[ f1 i ]``. In |Coq| 8.10, this second
   (convenience) step was only performed when `R1` was Leibniz' `eq` or
   `iff`. Now, it is also performed for any relation `R1` which has a
   ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance
@@ -1612,7 +1612,7 @@ Changes in 8.11+beta1
   .. warning::
 
      This is a common source of incompatibilities in projects
-     migrating to Coq 8.11.
+     migrating to |Coq| 8.11.
 
 - **Changed:**
   Output generated by :flag:`Printing Dependent Evars Line` flag
@@ -1643,7 +1643,7 @@ Changes in 8.11+beta1
   `coqc` now provides the ability to generate compiled interfaces.
   Use `coqc -vos foo.v` to skip all opaque proofs during the
   compilation of `foo.v`, and output a file called `foo.vos`.
-  This feature is experimental. It enables working on a Coq file without the need to
+  This feature is experimental. It enables working on a |Coq| file without the need to
   first compile the proofs contained in its dependencies
   (`#8642 <https://github.com/coq/coq/pull/8642>`_ by Arthur Charguéraud, review by
   Maxime Dénès and Emilio Gallego).
@@ -1715,7 +1715,7 @@ Changes in 8.11+beta1
 **Infrastructure and dependencies**
 
 - **Changed:**
-  Coq now officially supports OCaml 4.08.
+  |Coq| now officially supports OCaml 4.08.
   See `INSTALL` file for details
   (`#10471 <https://github.com/coq/coq/pull/10471>`_,
   by Emilio Jesús Gallego Arias).
@@ -1793,7 +1793,7 @@ Changes in 8.11.0
 **Tactic language**
 
 - **Fixed:**
-  Syntax of tactic `cofix ... with ...` was broken since Coq 8.10
+  Syntax of tactic `cofix ... with ...` was broken since |Coq| 8.10
   (`#11241 <https://github.com/coq/coq/pull/11241>`_,
   by Hugo Herbelin).
 
@@ -1826,9 +1826,9 @@ Changes in 8.11.0
   fixes `#11353 <https://github.com/coq/coq/issues/11353>`_,
   by Karl Palmskog).
 
-**CoqIDE**
+**|CoqIDE|**
 
-- **Changed:** CoqIDE now uses the GtkSourceView native implementation
+- **Changed:** |CoqIDE| now uses the GtkSourceView native implementation
   of the autocomplete mechanism (`#11400
   <https://github.com/coq/coq/pull/11400>`_, by Pierre-Marie Pédrot).
 
@@ -1874,7 +1874,7 @@ Changes in 8.11.1
   (`#11859 <https://github.com/coq/coq/pull/11859>`_,
   by Pierre Roux).
 
-**CoqIDE**
+**|CoqIDE|**
 
 - **Fixed:**
   Compiling file paths containing spaces
@@ -1932,21 +1932,21 @@ Changes in 8.11.2
   (`#12070 <https://github.com/coq/coq/pull/12070>`_,
   by Pierre Roux).
 
-**CoqIDE**
+**|CoqIDE|**
 
 - **Changed:**
-  CoqIDE now uses native window frames by default on Windows.
+  |CoqIDE| now uses native window frames by default on Windows.
   The GTK window frames can be restored by setting the `GTK_CSD` environment variable to `1`
   (`#12060 <https://github.com/coq/coq/pull/12060>`_,
   fixes `#11080 <https://github.com/coq/coq/issues/11080>`_,
   by Attila Gáspár).
 - **Fixed:**
-  New patch presumably fixing the random Coq 8.11 segfault issue with CoqIDE completion
+  New patch presumably fixing the random |Coq| 8.11 segfault issue with |CoqIDE| completion
   (`#12068 <https://github.com/coq/coq/pull/12068>`_,
   by Hugo Herbelin, presumably fixing
   `#11943 <https://github.com/coq/coq/pull/11943>`_).
 - **Fixed:**
-  Highlighting style consistently applied to all three buffers of CoqIDE
+  Highlighting style consistently applied to all three buffers of |CoqIDE|
   (`#12106 <https://github.com/coq/coq/pull/12106>`_,
   by Hugo Herbelin; fixes
   `#11506 <https://github.com/coq/coq/pull/11506>`_).
@@ -2058,15 +2058,15 @@ reference manual. Here are the most important user-visible changes:
   :math:`\Type`. It used to be limited to sort `Prop`
   (`#7634 <https://github.com/coq/coq/pull/7634>`_, by Théo Winterhalter).
 
-- A new registration mechanism for reference from ML code to Coq
+- A new registration mechanism for reference from ML code to |Coq|
   constructs has been added
   (`#186 <https://github.com/coq/coq/pull/186>`_,
   by Emilio Jesús Gallego Arias, Maxime Dénès and Vincent Laporte).
 
-- CoqIDE:
+- |CoqIDE|:
 
-  - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2.
-    The INSTALL file available in the Coq sources has been updated to list
+  - |CoqIDE| now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2.
+    The INSTALL file available in the |Coq| sources has been updated to list
     the new dependencies
     (`#9279 <https://github.com/coq/coq/pull/9279>`_,
     by Hugo Herbelin, with help from Jacques Garrigue,
@@ -2081,15 +2081,15 @@ reference manual. Here are the most important user-visible changes:
 
 - Infrastructure and dependencies:
 
-  - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the
+  - |Coq| 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the
     `INSTALL` file for more information on dependencies
     (`#7522 <https://github.com/coq/coq/pull/7522>`_, by Emilio Jesús Gallego Arías).
 
-  - Coq 8.10 doesn't need Camlp5 to build anymore. It now includes a
-    fork of the core parsing library that Coq uses, which is a small
+  - |Coq| 8.10 doesn't need Camlp5 to build anymore. It now includes a
+    fork of the core parsing library that |Coq| uses, which is a small
     subset of the whole Camlp5 distribution. In particular, this subset
     doesn't depend on the OCaml AST, allowing easier compilation and
-    testing on experimental OCaml versions. Coq also ships a new parser
+    testing on experimental OCaml versions. |Coq| also ships a new parser
     `coqpp` that plugin authors must switch to
     (`#7902 <https://github.com/coq/coq/pull/7902>`_,
     `#7979 <https://github.com/coq/coq/pull/7979>`_,
@@ -2098,19 +2098,19 @@ reference manual. Here are the most important user-visible changes:
     and `#8945 <https://github.com/coq/coq/pull/8945>`_,
     by Pierre-Marie Pédrot and Emilio Jesús Gallego Arias).
 
-    The Coq developers would like to thank Daniel de Rauglaudre for many
+    The |Coq| developers would like to thank Daniel de Rauglaudre for many
     years of continued support.
 
-  - Coq now supports building with Dune, in addition to the traditional
+  - |Coq| now supports building with Dune, in addition to the traditional
     Makefile which is scheduled for deprecation
     (`#6857 <https://github.com/coq/coq/pull/6857>`_,
     by Emilio Jesús Gallego Arias, with help from Rudi Grinberg).
 
-    Experimental support for building Coq projects has been integrated
+    Experimental support for building |Coq| projects has been integrated
     in Dune at the same time, providing an `improved experience
     <https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/>`_
     for plugin developers. We thank the Dune team for their work
-    supporting Coq.
+    supporting |Coq|.
 
 Version 8.10 also comes with a bunch of smaller-scale changes and
 improvements regarding the different components of the system, including
@@ -2129,10 +2129,10 @@ contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès.
 Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael
 Soegtrop, Théo Zimmermann worked on maintaining and improving the
 continuous integration system and package building infrastructure.
-Coq is now continuously tested against OCaml trunk, in addition to the
+|Coq| is now continuously tested against the |OCaml| trunk, in addition to the
 oldest supported and latest OCaml releases.
 
-Coq's documentation for the development branch is now deployed
+|Coq|'s documentation for the development branch is now deployed
 continuously at https://coq.github.io/doc/master/api (documentation of
 the ML API), https://coq.github.io/doc/master/refman (reference
 manual), and https://coq.github.io/doc/master/stdlib (documentation of
@@ -2191,13 +2191,13 @@ Other changes in 8.10+beta1
     (*à la* ``-top``) based on the filename passed, taking into account the
     proper ``-R``/``-Q`` options. For example, given ``-R Foo foolib`` using
     ``-topfile foolib/bar.v`` will set the module name to ``Foo.Bar``.
-    CoqIDE now properly sets the module name for a given file based on
+    |CoqIDE| now properly sets the module name for a given file based on
     its path
     (`#8991 <https://github.com/coq/coq/pull/8991>`_,
     closes `#8989 <https://github.com/coq/coq/issues/8989>`_,
     by Gaëtan Gilbert).
 
-  - Experimental: Coq flags and options can now be set on the
+  - Experimental: |Coq| flags and options can now be set on the
     command-line, e.g. ``-set "Universe Polymorphism=true"``
     (`#9876 <https://github.com/coq/coq/pull/9876>`_, by Gaëtan Gilbert).
 
@@ -2295,7 +2295,7 @@ Other changes in 8.10+beta1
 
   - Deprecated compatibility notations have actually been
     removed. Uses of these notations are generally easy to fix thanks
-    to the hint contained in the deprecation warning emitted by Coq
+    to the hint contained in the deprecation warning emitted by |Coq|
     8.8 and 8.9.  For projects that require more than a handful of
     such fixes, there is `a script
     <https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py>`_
@@ -2310,7 +2310,7 @@ Other changes in 8.10+beta1
 - The `quote plugin
   <https://coq.inria.fr/distrib/V8.9.0/refman/proof-engine/detailed-tactic-examples.html#quote>`_
   was removed. If some users are interested in maintaining this plugin
-  externally, the Coq development team can provide assistance for
+  externally, the |Coq| development team can provide assistance for
   extracting the plugin and setting up a new repository
   (`#7894 <https://github.com/coq/coq/pull/7894>`_, by Maxime Dénès).
 
@@ -2537,7 +2537,7 @@ Other changes in 8.10+beta1
 - Changelog has been moved from a specific file `CHANGES.md` to the
   reference manual; former Credits chapter of the reference manual has
   been split in two parts: a History chapter which was enriched with
-  additional historical information about Coq versions 1 to 5, and a
+  additional historical information about |Coq| versions 1 to 5, and a
   Changes chapter which was enriched with the content formerly in
   `CHANGES.md` and `COMPATIBILITY`
   (`#9133 <https://github.com/coq/coq/pull/9133>`_,
@@ -2580,15 +2580,15 @@ Many bug fixes and documentation improvements, in particular:
   fixes `#9336 <https://github.com/coq/coq/issues/9336>`_,
   by Andreas Lynge, review by Enrico Tassi)
 
-**CoqIDE**
+**|CoqIDE|**
 
-- Fix CoqIDE instability on Windows after the update to gtk3
+- Fix |CoqIDE| instability on Windows after the update to gtk3
   (`#10360 <https://github.com/coq/coq/pull/10360>`_, by Michael Soegtrop,
   closes `#9885 <https://github.com/coq/coq/issues/9885>`_).
 
 **Miscellaneous**
 
-- Proof General can now display Coq-generated diffs between proof steps
+- Proof General can now display |Coq|-generated diffs between proof steps
   in color
   (`#10019 <https://github.com/coq/coq/pull/10019>`_ and
   (in Proof General) `#421 <https://github.com/ProofGeneral/PG/pull/421>`_,
@@ -2696,7 +2696,7 @@ A few bug fixes and documentation improvements, in particular:
   fixes `#10894 <https://github.com/coq/coq/issues/10894>`_,
   by Hugo Herbelin).
 
-**CoqIDE**
+**|CoqIDE|**
 
 - Fix handling of unicode input before space
   (`#10852 <https://github.com/coq/coq/pull/10852>`_,
@@ -2736,9 +2736,9 @@ Changes in 8.10.2
   (`#11090 <https://github.com/coq/coq/pull/11090>`_,
   fixes `#11033 <https://github.com/coq/coq/issues/11033>`_, by Hugo Herbelin).
 
-**CoqIDE**
+**|CoqIDE|**
 
-- Fixed uneven dimensions of CoqIDE panels when window has been resized
+- Fixed uneven dimensions of |CoqIDE| panels when window has been resized
   (`#11070 <https://github.com/coq/coq/pull/11070>`_,
   fixes 8.10-regression `#10956 <https://github.com/coq/coq/issues/10956>`_,
   by Guillaume Melquiond).
@@ -2853,7 +2853,7 @@ important ones are documented in the next subsection file.
 On the implementation side, the ``dev/doc/changes.md`` file documents
 the numerous changes to the implementation and improvements of
 interfaces. The file provides guidelines on porting a plugin to the new
-version and a plugin development tutorial kept in sync with Coq was
+version and a plugin development tutorial kept in sync with |Coq| was
 introduced by Yves Bertot http://github.com/ybertot/plugin_tutorials.
 The new ``dev/doc/critical-bugs`` file documents the known critical bugs
 of |Coq| and affected releases.
@@ -2917,7 +2917,7 @@ Notations
   entries" (see chapter "Syntax extensions" of the reference manual).
 
 - Deprecated compatibility notations will actually be removed in the
-  next version of Coq.  Uses of these notations are generally easy to
+  next version of |Coq|.  Uses of these notations are generally easy to
   fix thanks to the hint contained in the deprecation warnings. For
   projects that require more than a handful of such fixes, there is `a
   script
@@ -3018,7 +3018,7 @@ Standard Library
 
 - Numeral syntax for `nat` is no longer available without loading the
   entire prelude (`Require Import Coq.Init.Prelude`).  This only
-  impacts users running Coq without the init library (`-nois` or
+  impacts users running |Coq| without the init library (`-nois` or
   `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`.
 
 Tools
@@ -3028,10 +3028,10 @@ Tools
   `COQFLAGS` is now entirely separate from `COQLIBS`, so in custom Makefiles
   `$(COQFLAGS)` should be replaced by `$(COQFLAGS) $(COQLIBS)`.
 
-- Removed the `gallina` utility (extracts specification from Coq vernacular files).
+- Removed the `gallina` utility (extracts specification from |Coq| vernacular files).
   If you would like to maintain this tool externally, please contact us.
 
-- Removed the Emacs modes distributed with Coq. You are advised to
+- Removed the Emacs modes distributed with |Coq|. You are advised to
   use `Proof-General <https://proofgeneral.github.io/>`_ (and optionally
   `Company-Coq <https://github.com/cpitclaudel/company-coq>`_) instead.
   If your use case is not covered by these alternative Emacs modes,
@@ -3060,15 +3060,15 @@ Vernacular Commands
   NoTCResolution`.
 - Multiple sections with the same name are allowed.
 
-Coq binaries and process model
+|Coq| binaries and process model
 
-- Before 8.9, Coq distributed a single `coqtop` binary and a set of
+- Before 8.9, |Coq| distributed a single `coqtop` binary and a set of
   dynamically loadable plugins that used to take over the main loop
   for tasks such as IDE language server or parallel proof checking.
 
   These plugins have been turned into full-fledged binaries so each
   different process has associated a particular binary now, in
-  particular `coqidetop` is the CoqIDE language server, and
+  particular `coqidetop` is the |CoqIDE| language server, and
   `coq{proof,tactic,query}worker` are in charge of task-specific and
   parallel proof checking.
 
@@ -3126,7 +3126,7 @@ Changes in 8.8.1
 - Some quality-of-life fixes.
 - Numerous improvements to the documentation.
 - Fix a critical bug related to primitive projections and :tacn:`native_compute`.
-- Ship several additional Coq libraries with the Windows installer.
+- Ship several additional |Coq| libraries with the Windows installer.
 
 Version 8.8
 -----------
@@ -3232,7 +3232,7 @@ of everybody who to some extent influenced the development.
 
 The |Coq| consortium, an organization directed towards users and
 supporters of the system, is now running and employs Maxime Dénès.
-The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès.
+The contacts of the |Coq| Consortium are Yves Bertot and Maxime Dénès.
 
 | Santiago de Chile, March 2018,
 | Matthieu Sozeau for the |Coq| development team
@@ -3354,7 +3354,7 @@ Universes
 
 Tools
 
-- Coq can now be run with the option -mangle-names to change the auto-generated
+- |Coq| can now be run with the option -mangle-names to change the auto-generated
   name scheme. This is intended to function as a linter for developments that
   want to be robust to changes in auto-generated names. This feature is experimental,
   and may change or disappear without warning.
@@ -3364,7 +3364,7 @@ Checker
 
 - The checker now accepts filenames in addition to logical paths.
 
-CoqIDE
+|CoqIDE|
 
 - Find and Replace All report the number of occurrences found; Find indicates
   when it wraps.
@@ -3377,7 +3377,7 @@ coqdep
 
 Documentation
 
-- The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been
+- The |Coq| FAQ, formerly located at https://coq.inria.fr/faq, has been
   moved to the GitHub wiki section of this repository; the main entry
   page is https://github.com/coq/coq/wiki/The-Coq-FAQ.
 - Documentation: a large community effort resulted in the migration
@@ -3427,7 +3427,7 @@ Details of changes in 8.8.0
 Tools
 
 - Asynchronous proof delegation policy was fixed. Since version 8.7
-  Coq was ignoring previous runs and the `-async-proofs-delegation-threshold`
+  |Coq| was ignoring previous runs and the `-async-proofs-delegation-threshold`
   option did not have the expected behavior.
 
 Tactic language
@@ -3700,7 +3700,7 @@ Vernacular Commands
 - Possibility to unset the printing of notations in a more fine grained
   fashion than `Unset Printing Notations` is provided without any
   user-syntax. The goal is that someone creates a plugin to experiment
-  such a user-syntax, to be later integrated in Coq when stabilized.
+  such a user-syntax, to be later integrated in |Coq| when stabilized.
 - `About` now tells if a reference is a coercion.
 - The deprecated `Save` vernacular and its form `Save Theorem id` to
   close proofs have been removed from the syntax. Please use `Qed`.
@@ -3718,7 +3718,7 @@ Standard Library
 - New lemmas about iff and about orders on positive and Z.
 - New lemmas on powerRZ.
 - Strengthened statement of JMeq_eq_dep (closes bug #4912).
-- The BigN, BigZ, BigZ libraries are no longer part of the Coq standard
+- The BigN, BigZ, BigZ libraries are no longer part of the |Coq| standard
   library, they are now provided by a separate repository
   https://github.com/coq/bignums
   The split has been done just after the Int31 library.
@@ -3732,12 +3732,12 @@ Standard Library
 
 Plugins
 
-- The Ssreflect plugin is now distributed with Coq. Its documentation has
+- The Ssreflect plugin is now distributed with |Coq|. Its documentation has
   been integrated as a chapter of the reference manual. This chapter is
   work in progress so feedback is welcome.
 - The mathematical proof language (also known as declarative mode) was removed.
 - A new command Extraction TestCompile has been introduced, not meant
-  for the general user but instead for Coq's test-suite.
+  for the general user but instead for |Coq|'s test-suite.
 - The extraction plugin is no longer loaded by default. It must be
   explicitly loaded with [Require Extraction], which is backwards
   compatible.
@@ -3756,7 +3756,7 @@ Tools
   the extensibility of generated Makefiles, and to make _CoqProject files
   more palatable to IDEs.  Overview:
 
-  * _CoqProject files contain only Coq specific data (i.e. the list of
+  * _CoqProject files contain only |Coq| specific data (i.e. the list of
     files, -R options, ...)
   * coq_makefile translates _CoqProject to Makefile.conf and copies in the
     desired location a standard Makefile (that reads Makefile.conf)
@@ -3814,15 +3814,15 @@ Details of changes in 8.7+beta2
 
 Tools
 
-- In CoqIDE, the "Compile Buffer" command takes account of flags in
+- In |CoqIDE|, the "Compile Buffer" command takes account of flags in
   _CoqProject or other project file.
 
 Improvements around some error messages.
 
 Many bug fixes including two important ones:
 
-- Bug #5730: CoqIDE becomes unresponsive on file open.
-- coq_makefile: make sure compile flags for Coq and coq_makefile are in sync
+- Bug #5730: |CoqIDE| becomes unresponsive on file open.
+- coq_makefile: make sure compile flags for |Coq| and coq_makefile are in sync
   (in particular, make sure the `-safe-string` option is used to compile plugins).
 
 Details of changes in 8.7.0
@@ -3833,7 +3833,7 @@ OCaml
 - Users can pass specific flags to the OCaml optimizing compiler by
   -using the flambda-opts configure-time option.
 
-  Beware that compiling Coq with a flambda-enabled compiler is
+  Beware that compiling |Coq| with a flambda-enabled compiler is
   experimental and may require large amounts of RAM and CPU, see
   INSTALL for more details.
 
@@ -3863,7 +3863,7 @@ Version 8.6
 Summary of changes
 ~~~~~~~~~~~~~~~~~~
 
-Coq version 8.6 contains the result of refinements, stabilization of
+|Coq| version 8.6 contains the result of refinements, stabilization of
 8.5’s features and cleanups of the internals of the system. Over the
 year of (now time-based) development, about 450 bugs were resolved and
 over 100 contributions integrated. The main user visible changes are:
@@ -3897,7 +3897,7 @@ over 100 contributions integrated. The main user visible changes are:
 -  Integration of LtacProf, a profiler for Ltac by Jason Gross, Paul
    Steckler, Enrico Tassi and Tobias Tebbi.
 
-Coq 8.6 also comes with a bunch of smaller-scale changes and
+|Coq| 8.6 also comes with a bunch of smaller-scale changes and
 improvements regarding the different components of the system. We shall
 only list a few of them.
 
@@ -3983,13 +3983,13 @@ development.
 
 Version 8.6 is the first release of |Coq| developed on a time-based
 development cycle. Its development spanned 10 months from the release of
-Coq 8.5 and was based on a public roadmap. To date, it contains more
+|Coq| 8.5 and was based on a public roadmap. To date, it contains more
 external contributions than any previous |Coq| system. Code reviews were
 systematically done before integration of new features, with an
 important focus given to compatibility and performance issues, resulting
 in a hopefully more robust release than |Coq| 8.5.
 
-Coq Enhancement Proposals (CEPs for short) were introduced by Enrico
+|Coq| Enhancement Proposals (CEPs for short) were introduced by Enrico
 Tassi to provide more visibility and a discussion period on new
 features, they are publicly available https://github.com/coq/ceps.
 
@@ -4134,13 +4134,13 @@ General infrastructure
 - New configurable warning system which can be controlled with the vernacular
   command "Set Warnings", or, under coqc/coqtop, with the flag "-w". In
   particular, the default is now that warnings are printed by coqc.
-- In asynchronous mode, Coq is now capable of recovering from errors and
+- In asynchronous mode, |Coq| is now capable of recovering from errors and
   continue processing the document.
 
 Tools
 
 - coqc accepts a -o option to specify the output file name
-- coqtop accepts --print-version to print Coq and OCaml versions in
+- coqtop accepts --print-version to print |Coq| and |OCaml| versions in
   easy to parse format
 - Setting [Printing Dependent Evars Line] can be unset to disable the
   computation associated with printing the "dependent evars: " line in
@@ -4169,7 +4169,7 @@ Other bug fixes in universes, type class shelving,...
 Details of changes in 8.6.1
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-- Fix #5380: Default colors for CoqIDE are actually applied.
+- Fix #5380: Default colors for |CoqIDE| are actually applied.
 - Fix plugin warnings
 - Document named evars (including Show ident)
 - Fix Bug #5574, document function scope
@@ -4221,7 +4221,7 @@ Version 8.5
 Summary of changes
 ~~~~~~~~~~~~~~~~~~
 
-Coq version 8.5 contains the result of five specific long-term projects:
+|Coq| version 8.5 contains the result of five specific long-term projects:
 
 -  A new asynchronous evaluation and compilation mode by Enrico Tassi
    with help from Bruno Barras and Carst Tankink.
@@ -4312,7 +4312,7 @@ conversion test and normal form computation using the OCaml native
 compiler. It complements the virtual machine conversion offering much
 faster computation for expensive functions.
 
-Coq 8.5 also comes with a bunch of many various smaller-scale changes
+|Coq| 8.5 also comes with a bunch of many various smaller-scale changes
 and improvements regarding the different components of the system. We
 shall only list a few of them.
 
@@ -4375,8 +4375,8 @@ Tankink. Maxime Dénès coordinated the release process.
 Potential sources of incompatibilities
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-List of typical changes to be done to adapt files from Coq 8.4
-to Coq 8.5 when not using compatibility option ``-compat 8.4``.
+List of typical changes to be done to adapt files from |Coq| 8.4
+to |Coq| 8.5 when not using compatibility option ``-compat 8.4``.
 
 - Symptom: "The reference omega was not found in the current environment".
 
@@ -4511,7 +4511,7 @@ Logic
   logic inconsistent).
 - The guard condition for fixpoints is now a bit stricter. Propagation
   of subterm value through pattern matching is restricted according to
-  the return predicate. Restores compatibility of Coq's logic with the
+  the return predicate. Restores compatibility of |Coq|'s logic with the
   propositional extensionality axiom. May create incompatibilities in
   recursive programs heavily using dependent types.
 - Trivial inductive types are no longer defined in Type but in Prop, which
@@ -4551,7 +4551,7 @@ Vernacular commands
 - A new Print Strategies command allows visualizing the opacity status
   of the whole engine.
 - The "Locate" command now searches through all sorts of qualified namespaces of
-  Coq: terms, modules, tactics, etc. The old behavior of the command can be
+  |Coq|: terms, modules, tactics, etc. The old behavior of the command can be
   retrieved using the "Locate Term" command.
 - New "Derive" command to help writing program by derivation.
 - New "Refine Instance Mode" option that allows to deactivate the generation of
@@ -4879,24 +4879,24 @@ Tools
   files from the quickly generated proofs.
 - The XML plugin was discontinued and removed from the source.
 - A new utility called coqworkmgr can be used to limit the number of
-  concurrent workers started by independent processes, like make and CoqIDE.
+  concurrent workers started by independent processes, like make and |CoqIDE|.
   This is of interest for users of the par: goal selector.
 
 Interfaces
 
-- CoqIDE supports asynchronous edition of the document, ongoing tasks and
+- |CoqIDE| supports asynchronous edition of the document, ongoing tasks and
   errors are reported in the bottom right window.  The number of workers
   taking care of processing proofs can be selected with -async-proofs-j.
-- CoqIDE highlights in yellow "unsafe" commands such as axiom
+- |CoqIDE| highlights in yellow "unsafe" commands such as axiom
   declarations, and tactics like "give_up".
-- CoqIDE supports Proof General like key bindings;
+- |CoqIDE| supports Proof General like key bindings;
   to activate the PG mode go to Edit -> Preferences -> Editor.
   For the documentation see Help -> Help for PG mode.
-- CoqIDE automatically retracts the locked area when one edits the
+- |CoqIDE| automatically retracts the locked area when one edits the
   locked text.
-- CoqIDE search and replace got regular expressions power. See the
+- |CoqIDE| search and replace got regular expressions power. See the
   documentation of OCaml's Str module for the supported syntax.
-- Many CoqIDE windows, including the query one, are now detachable to
+- Many |CoqIDE| windows, including the query one, are now detachable to
   improve usability on multi screen work stations.
 - Coqtop/coqc outputs highlighted syntax. Colors can be configured thanks
   to the COQ_COLORS environment variable, and their current state can
@@ -4907,7 +4907,7 @@ Interfaces
 Internal Infrastructure
 
 - Many reorganizations in the ocaml source files. For instance,
-  many internal a.s.t. of Coq are now placed in mli files in
+  many internal a.s.t. of |Coq| are now placed in mli files in
   a new directory intf/, for instance constrexpr.mli or glob_term.mli.
   More details in dev/doc/changes.
 
@@ -4959,7 +4959,7 @@ Tactics
 Extraction
 
 - Definitions extracted to Haskell GHC should no longer randomly
-  segfault when some Coq types cannot be represented by Haskell types.
+  segfault when some |Coq| types cannot be represented by Haskell types.
 - Definitions can now be extracted to Json for post-processing.
 
 Tools
@@ -5057,8 +5057,8 @@ Tools
 Standard Library
 
  - There is now a Coq.Compat.Coq84 library, which sets the various compatibility
-   options and does a few redefinitions to make Coq behave more like Coq v8.4.
-   The standard way of putting Coq in v8.4 compatibility mode is to pass the command
+   options and does a few redefinitions to make |Coq| behave more like |Coq| v8.4.
+   The standard way of putting |Coq| in v8.4 compatibility mode is to pass the command
    line flags "-require Coq.Compat.Coq84 -compat 8.4".
 
 Details of changes in 8.5
@@ -5067,7 +5067,7 @@ Details of changes in 8.5
 Tools
 
 - Flag "-compat 8.4" now loads Coq.Compat.Coq84. The standard way of
-  putting Coq in v8.4 compatibility mode is to pass the command line flag
+  putting |Coq| in v8.4 compatibility mode is to pass the command line flag
   "-compat 8.4". It can be followed by "-require Coq.Compat.AdmitAxiom"
   if the 8.4 behavior of admit is needed, in which case it uses an axiom.
 
@@ -5108,7 +5108,7 @@ Various performance improvements (time, space used by .vo files)
 Other bugfixes
 
 - Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v
-- Added compatibility coercions from Specif.v which were present in Coq 8.4.
+- Added compatibility coercions from Specif.v which were present in |Coq| 8.4.
 - Fixing a source of inefficiency and an artificial dependency in the printer in the congruence tactic.
 - Allow to unset the refinement mode of Instance in ML
 - Fixing an incorrect use of prod_appvect on a term which was not a product in setoid_rewrite.
@@ -5123,7 +5123,7 @@ Other bugfixes
 - #4623: set tactic too weak with universes (regression)
 - Fix incorrect behavior of CS resolution
 - #4591: Uncaught exception in directory browsing.
-- CoqIDE is more resilient to initialization errors.
+- |CoqIDE| is more resilient to initialization errors.
 - #4614: "Fully check the document" is uninterruptible.
 - Try eta-expansion of records only on non-recursive ones
 - Fix bug when a sort is ascribed to a Record
@@ -5133,23 +5133,23 @@ Other bugfixes
 - Fix strategy of Keyed Unification
 - #4608: Anomaly "output_value: abstract value (outside heap)".
 - #4607: do not read native code files if native compiler was disabled.
-- #4105: poor escaping in the protocol between CoqIDE and coqtop.
+- #4105: poor escaping in the protocol between |CoqIDE| and coqtop.
 - #4596: [rewrite] broke in the past few weeks.
 - #4533 (partial): respect declared global transparency of projections in unification.ml
 - #4544: Backtrack on using full betaiota reduction during keyed unification.
-- #4540: CoqIDE bottom progress bar does not update.
+- #4540: |CoqIDE| bottom progress bar does not update.
 - Fix regression from 8.4 in reflexivity
 - #4580: [Set Refine Instance Mode] also used for Program Instance.
 - #4582: cannot override notation [ x ]. MAY CREATE INCOMPATIBILITIES, see #4683.
 - STM: Print/Extraction have to be skipped if -quick
-- #4542: CoqIDE: STOP button also stops workers
+- #4542: |CoqIDE|: STOP button also stops workers
 - STM: classify some variants of Instance as regular `` `Fork `` nodes.
 - #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
 - Do not give a name to anonymous evars anymore. See bug #4547.
 - STM: always stock in vio files the first node (state) of a proof
 - STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530
 - Don't fail fatally if PATH is not set.
-- #4537: Coq 8.5 is slower in typeclass resolution.
+- #4537: |Coq| 8.5 is slower in typeclass resolution.
 - #4522: Incorrect "Warning..." on windows.
 - #4373: coqdep does not know about .vio files.
 - #3826: "Incompatible module types" is uninformative.
@@ -5158,7 +5158,7 @@ Other bugfixes
 - #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported.
 - #4519: oops, global shadowed local universe level bindings.
 - #4506: Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20: Assertion failed.
-- #4548: Coqide crashes when going back one command
+- #4548: |CoqIDE| crashes when going back one command
 
 Details of changes in 8.5pl2
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -5179,8 +5179,8 @@ Other bugfixes
 - #4644: a regression in unification.
 - #4725: Function (Error: Conversion test raised an anomaly) and Program
   (Error: Cannot infer this placeholder of type)
-- #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings
-- #4752: CoqIDE crash on files not ended by ".v".
+- #4747: Problem building |Coq| 8.5pl1 with OCaml 4.03.0: Fatal warnings
+- #4752: |CoqIDE| crash on files not ended by ".v".
 - #4777: printing inefficiency with implicit arguments
 - #4818: "Admitted" fails due to undefined universe anomaly after calling
   "destruct"
@@ -5194,7 +5194,7 @@ Other bugfixes
 - #4881: synchronizing "Declare Implicit Tactic" with backtrack.
 - #4882: anomaly with Declare Implicit Tactic on hole of type with evars
 - Fix use of "Declare Implicit Tactic" in refine.
-  triggered by CoqIDE
+  triggered by |CoqIDE|
 - #4069, #4718: congruence fails when universes are involved.
 
 Universes
@@ -5257,7 +5257,7 @@ Other bugfixes
 - #5097: status of evars refined by "clear" in ltac: closed wrt evars.
 - #5150: Missing dependency of the test-suite subsystems in prerequisite.
 - Fix a bug in error printing of unif constraints
-- #3941: Do not stop propagation of signals when Coq is busy.
+- #3941: Do not stop propagation of signals when |Coq| is busy.
 - #4822: Incorrect assertion in cbn.
 - #3479 parsing of "{" and "}" when a keyword starts with "{" or "}".
 - #5127: Memory corruption with the VM.
@@ -5271,7 +5271,7 @@ Version 8.4
 Summary of changes
 ~~~~~~~~~~~~~~~~~~
 
-Coq version 8.4 contains the result of three long-term projects: a new
+|Coq| version 8.4 contains the result of three long-term projects: a new
 modular library of arithmetic by Pierre Letouzey, a new proof engine by
 Arnaud Spiwack and a new communication protocol for |CoqIDE| by Vincent
 Gross.
@@ -5304,7 +5304,7 @@ sessions in parallel. Relying on the infrastructure work made by Vincent
 Gross, Pierre Letouzey, Pierre Boutillier and Pierre-Marie Pédrot
 contributed many various refinements of |CoqIDE|.
 
-Coq 8.4 also comes with a bunch of various smaller-scale changes
+|Coq| 8.4 also comes with a bunch of various smaller-scale changes
 and improvements regarding the different components of the system.
 
 The underlying logic has been extended with :math:`\eta`-conversion
@@ -5382,14 +5382,14 @@ Julien Forest maintained the Function command.
 
 Matthieu Sozeau maintained the setoid rewriting mechanism.
 
-Coq related tools have been upgraded too. In particular, coq\_makefile
+|Coq| related tools have been upgraded too. In particular, coq\_makefile
 has been largely revised by Pierre Boutillier. Also, patches from Adam
 Chlipala for coqdoc have been integrated by Pierre Boutillier.
 
 Bruno Barras and Pierre Letouzey maintained the `coqchk` checker.
 
 Pierre Courtieu and Arnaud Spiwack contributed new features for using
-Coq through Proof General.
+|Coq| through Proof General.
 
 The Dp plugin has been removed. Use the plugin provided with Why 3
 instead (http://why3.lri.fr/).
@@ -5641,7 +5641,7 @@ Libraries
 
   * "<?" "<=?" "=?" for boolean tests such as Z.ltb Z.leb Z.eqb.
   * "÷" for the alternative integer division Z.quot implementing the Truncate
-    convention (former ZOdiv), while the notation for the Coq usual division
+    convention (former ZOdiv), while the notation for the |Coq| usual division
     Z.div implementing the Flooring convention remains "/". Their corresponding
     modulo functions are Z.rem (no notations) for Z.quot and Z.modulo (infix
     "mod" notation) for Z.div.
@@ -5701,31 +5701,31 @@ Extraction
   universe polymorphism it cannot handle yet (the pair (I,I) being Prop).
 - Support of anonymous fields in record (#2555).
 
-CoqIDE
+|CoqIDE|
 
-- Coqide now runs coqtop as separated process, making it more robust:
+- |CoqIDE| now runs coqtop as separated process, making it more robust:
   coqtop subprocess can be interrupted, or even killed and relaunched
   (cf button "Restart Coq", ex-"Go to Start"). For allowing such
   interrupts, the Windows version of coqide now requires Windows >= XP
   SP1.
-- The communication between CoqIDE and Coqtop is now done via a dialect
+- The communication between |CoqIDE| and coqtop is now done via a dialect
   of XML (DOC TODO).
-- The backtrack engine of CoqIDE has been reworked, it now uses the
+- The backtrack engine of |CoqIDE| has been reworked, it now uses the
   "Backtrack" command similarly to Proof General.
-- The Coqide parsing of sentences has be reworked and now supports
+- The |CoqIDE| parsing of sentences has be reworked and now supports
   tactic delimitation via { }.
-- Coqide now accepts the Abort command (wish #2357).
-- Coqide can read coq_makefile files as "project file" and use it to
+- |CoqIDE| now accepts the Abort command (wish #2357).
+- |CoqIDE| can read coq_makefile files as "project file" and use it to
   set automatically options to send to coqtop.
 - Preference files have moved to $XDG_CONFIG_HOME/coq and accelerators
   are not stored as a list anymore.
 
 Tools
 
-- Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq,
+- |Coq| now searches directories specified in COQPATH, $XDG_DATA_HOME/coq,
   $XDG_DATA_DIRS/coq, and user-contribs before the standard library.
 
-- Coq rc file has moved to $XDG_CONFIG_HOME/coq.
+- |Coq| rc file has moved to $XDG_CONFIG_HOME/coq.
 
 - Major changes to coq_makefile:
 
@@ -5783,9 +5783,9 @@ Module System
   namespace from ordinary definitions: "Definition E:=0. Module E. End E."
   is now accepted.
 
-CoqIDE
+|CoqIDE|
 
-- Coqide now supports the "Restart" command, and "Undo" (with a warning).
+- |CoqIDE| now supports the "Restart" command, and "Undo" (with a warning).
   Better support for "Abort".
 
 Details of changes in 8.4
@@ -5802,9 +5802,9 @@ Vernacular commands
 Notations
 
 - Most compatibility notations of the standard library are now tagged as
-  (compat xyz), where xyz is a former Coq version, for instance "8.3".
+  (compat xyz), where xyz is a former |Coq| version, for instance "8.3".
   These notations behave as (only parsing) notations, except that they may
-  triggers warnings (or errors) when used while Coq is not in a corresponding
+  triggers warnings (or errors) when used while |Coq| is not in a corresponding
   -compat mode.
 - To activate these compatibility warnings, use "Set Verbose Compat Notations"
   or the command-line flag -verbose-compat-notations.
@@ -5834,7 +5834,7 @@ Version 8.3
 Summary of changes
 ~~~~~~~~~~~~~~~~~~
 
-Coq version 8.3 is before all a transition version with refinements or
+|Coq| version 8.3 is before all a transition version with refinements or
 extensions of the existing features and libraries and a new tactic nsatz
 based on Hilbert’s Nullstellensatz for deciding systems of equations
 over rings.
@@ -5873,7 +5873,7 @@ been done by Matthieu Sozeau, Hugo Herbelin and Pierre Letouzey.
 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
+|Coq| checker, Julien Forest maintained the Function mechanism for
 reasoning over recursively defined functions. Matthieu Sozeau, Hugo
 Herbelin and Jean-Marc Notin maintained coqdoc. Frédéric Besson
 maintained the Micromega platform for deciding systems of inequalities.
@@ -6037,12 +6037,12 @@ Module system
   "Inline" annotation in the type of its argument(s) (for examples of
   use of the new features, see libraries Structures and Numbers).
 - Coercions are now active only when modules are imported (use "Set Automatic
-  Coercions Import" to get the behavior of the previous versions of Coq).
+  Coercions Import" to get the behavior of the previous versions of |Coq|).
 
 Extraction
 
 - When using (Recursive) Extraction Library, the filenames are directly the
-  Coq ones with new appropriate extensions : we do not force anymore
+  |Coq| ones with new appropriate extensions : we do not force anymore
   uncapital first letters for Ocaml and capital ones for Haskell.
 - The extraction now tries harder to avoid code transformations that can be
   dangerous for the complexity. In particular many eta-expansions at the top
@@ -6125,7 +6125,7 @@ Vernacular commands
 
 Library
 
-- Use "standard" Coq names for the properties of eq and identity
+- Use "standard" |Coq| names for the properties of eq and identity
   (e.g. refl_equal is now eq_refl). Support for compatibility is provided.
 
 - The function Compare_dec.nat_compare is now defined directly,
@@ -6176,7 +6176,7 @@ Library
 - MSets library: an important evolution of the FSets library.
   "MSets" stands for Modular (Finite) Sets, by contrast with a forthcoming
   library of Class (Finite) Sets contributed by S. Lescuyer which will be
-  integrated with the next release of Coq. The main features of MSets are:
+  integrated with the next release of |Coq|. The main features of MSets are:
 
   + The use of Equivalence, Proper and other Type Classes features
     easing the handling of setoid equalities.
@@ -6191,7 +6191,7 @@ Library
 
   Note: No Maps yet in MSets. The FSets library is still provided
   for compatibility, but will probably be considered as deprecated in the
-  next release of Coq.
+  next release of |Coq|.
 
 - Numbers library:
 
@@ -6207,12 +6207,12 @@ Library
 
 Tools
 
-- Option -R now supports binding Coq root read-only.
+- Option -R now supports binding |Coq| root read-only.
 - New coqtop/coqc option -beautify to reformat .v files (usable
   e.g. to globally update notations).
 - New tool beautify-archive to beautify a full archive of developments.
 - New coqtop/coqc option -compat X.Y to simulate the general behavior
-  of previous versions of Coq (provides e.g. support for 8.2 compatibility).
+  of previous versions of |Coq| (provides e.g. support for 8.2 compatibility).
 
 Coqdoc
 
@@ -6228,7 +6228,7 @@ Coqdoc
 - New option "--parse-comments" to allow parsing of regular ``(* *)``
   comments.
 - New option "--plain-comments" to disable interpretation inside comments.
-- New option "--interpolate" to try and typeset identifiers in Coq escapings
+- New option "--interpolate" to try and typeset identifiers in |Coq| escapings
   using the available globalization information.
 - New option "--external url root" to refer to external libraries.
 - Links to section variables and notations now supported.
@@ -6242,7 +6242,7 @@ Internal infrastructure
 - An experimental build mechanism via ocamlbuild is provided.
   From the top of the archive, run ./configure as usual, and
   then ./build. Feedback about this build mechanism is most welcome.
-  Compiling Coq on platforms such as Windows might be simpler
+  Compiling |Coq| on platforms such as Windows might be simpler
   this way, but this remains to be tested.
 - The Makefile system has been simplified and factorized with
   the ocamlbuild system. In particular "make" takes advantage
@@ -6255,7 +6255,7 @@ Version 8.2
 Summary of changes
 ~~~~~~~~~~~~~~~~~~
 
-Coq version 8.2 adds new features, new libraries and improves on many
+|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
@@ -6410,7 +6410,7 @@ Vernacular commands
   qualified names (this holds also for coqtop/coqc option -R).
 - SearchAbout supports negated search criteria, reference to logical objects
   by their notation, and more generally search of subterms.
-- "Declare ML Module" now allows to import .cmxs files when Coq is
+- "Declare ML Module" now allows to import .cmxs files when |Coq| is
   compiled in native code with a version of OCaml that supports native
   Dynlink (>= 3.11).
 - Specific sort constraints on Record now taken into account.
@@ -6451,7 +6451,7 @@ Libraries
   version should be fairly good, but some adaptations may be required.
 
   * Interfaces of unordered ("weak") and ordered sets have been factorized
-    thanks to new features of Coq modules (in particular Include), see
+    thanks to new features of |Coq| modules (in particular Include), see
     FSetInterface. Same for maps. Hints in these interfaces have been
     reworked (they are now placed in a "set" database).
   * To allow full subtyping between weak and ordered sets, a field
@@ -6482,7 +6482,7 @@ Libraries
     initial Ocaml code and written via the Function framework.
 
 - Library IntMap, subsumed by FSets/FMaps, has been removed from
-  Coq Standard Library and moved into a user contribution Cachan/IntMap
+  |Coq| Standard Library and moved into a user contribution Cachan/IntMap
 
 - Better computational behavior of some constants (eq_nat_dec and
   le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare
@@ -6687,7 +6687,7 @@ Tactics
 - New tactic "specialize H with a" or "specialize (H a)" allows to transform
   in-place a universally-quantified hypothesis (H : forall x, T x) into its
   instantiated form (H : T a). Nota: "specialize" was in fact there in earlier
-  versions of Coq, but was undocumented, and had a slightly different behavior.
+  versions of |Coq|, but was undocumented, and had a slightly different behavior.
 
 - New tactic "contradict H" can be used to solve any kind of goal as long as
   the user can provide afterwards a proof of the negation of the hypothesis H.
@@ -6731,7 +6731,7 @@ Program
 - Program Lemma, Axiom etc... now permit to have obligations in the statement
   iff they can be automatically solved by the default tactic.
 - Renamed "Obligations Tactic" command to "Obligation Tactic".
-- New command "Preterm [ of id ]" to see the actual term fed to Coq for
+- New command "Preterm [ of id ]" to see the actual term fed to |Coq| for
   debugging purposes.
 - New option "Transparent Obligations" to control the declaration of
   obligations as transparent or opaque. All obligations are now transparent
@@ -6823,7 +6823,7 @@ Extraction
   not happen anymore.
 
 - The command Extract Inductive has now a syntax for infix notations. This
-  allows in particular to map Coq lists and pairs onto Caml ones:
+  allows in particular to map |Coq| lists and pairs onto |OCaml| ones:
 
   + Extract Inductive list => list [ "[]" "(::)" ].
   + Extract Inductive prod => "(*)" [ "(,)" ].
@@ -6837,16 +6837,16 @@ Extraction
   conflits with existing code, for instance when extracting module List
   to Ocaml.
 
-CoqIDE
+|CoqIDE|
 
-- CoqIDE font defaults to monospace so as indentation to be meaningful.
-- CoqIDE supports nested goals and any other kind of declaration in the middle
+- |CoqIDE| font defaults to monospace so as indentation to be meaningful.
+- |CoqIDE| supports nested goals and any other kind of declaration in the middle
   of a proof.
-- Undoing non-tactic commands in CoqIDE works faster.
-- New CoqIDE menu for activating display of various implicit informations.
+- Undoing non-tactic commands in |CoqIDE| works faster.
+- New |CoqIDE| menu for activating display of various implicit informations.
 - Added the possibility to choose the location of tabs in coqide:
   (in Edit->Preferences->Misc)
-- New Open and Save As dialogs in CoqIDE which filter ``*.v`` files.
+- New Open and Save As dialogs in |CoqIDE| which filter ``*.v`` files.
 
 Tools
 
@@ -6855,22 +6855,22 @@ Tools
 - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
 - The binary "parser" has been renamed to "coq-parser".
 - Improved coqdoc and dump of globalization information to give more
-  meta-information on identifiers. All categories of Coq definitions are
+  meta-information on identifiers. All categories of |Coq| definitions are
   supported, which makes typesetting trivial in the generated documentation.
   Support for hyperlinking and indexing developments in the tex output
   has been implemented as well.
 
 Miscellaneous
 
-- Coq installation provides enough files so that Ocaml's extensions need not
-  the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5).
+- |Coq| installation provides enough files so that Ocaml's extensions need not
+  the |Coq| sources to be compiled (this assumes O'Caml 3.10 and Camlp5).
 - New commands "Set Whelp Server" and "Set Whelp Getter" to customize the
   Whelp search tool.
 - Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
   "Test Printing Let for ref" and "Test Printing If for ref".
 - An overhauled build system (new Makefiles); see dev/doc/build-system.txt.
 - Add -browser option to configure script.
-- Build a shared library for the C part of Coq, and use it by default on
+- Build a shared library for the C part of |Coq|, and use it by default on
   non-(Windows or MacOS) systems. Bytecode executables are now pure. The
   behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and
   -custom configure options.
@@ -6883,7 +6883,7 @@ Version 8.1
 Summary of changes
 ~~~~~~~~~~~~~~~~~~
 
-Coq version 8.1 adds various new functionalities.
+|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
@@ -6991,7 +6991,7 @@ Vernacular commands
 
 Ltac and tactic syntactic extensions
 
-- New primitive "external" for communication with tool external to Coq
+- New primitive "external" for communication with tool external to |Coq|
 - New semantics for "match t with": if a clause returns a
   tactic, it is now applied to the current goal. If it fails, the next
   clause or next matching subterm is tried (i.e. it behaves as "match
@@ -7016,7 +7016,7 @@ Tactics
 - New conversion tactic "vm_compute": evaluates the goal (or an hypothesis)
   with a call-by-value strategy, using the compiled version of terms.
 
-- When rewriting H where H is not directly a Coq equality, search first H for
+- When rewriting H where H is not directly a |Coq| equality, search first H for
   a registered setoid equality before starting to reduce in H. This is unlikely
   to break any script. Should this happen nonetheless, one can insert manually
   some "unfold ... in H" before rewriting.
@@ -7061,7 +7061,7 @@ Tactics
 
 - New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns.
 
-- New introduction pattern "?" for letting Coq choose a name.
+- New introduction pattern "?" for letting |Coq| choose a name.
 
 - Introduction patterns now support side hypotheses (e.g. intros [|] on
   "(nat -> nat) -> nat" works).
@@ -7147,7 +7147,7 @@ Libraries
   Zlt_square_simpl removed; fixed names mentioning letter O instead of
   digit 0; weaken premises in Z_lt_induction).
 - Restructuration of Eqdep_dec.v and Eqdep.v: more lemmas in Type.
-- Znumtheory now contains a gcd function that can compute within Coq.
+- Znumtheory now contains a gcd function that can compute within |Coq|.
 - More lemmas stated on Type in Wf.v, removal of redundant Acc_iter and
   Acc_iter2.
 - Change of the internal names of lemmas in OmegaLemmas.
@@ -7180,7 +7180,7 @@ Tools
 - Tool coq_makefile now removes custom targets that are file names in
   "make clean"
 - New environment variable COQREMOTEBROWSER to set the command invoked
-  to start the remote browser both in Coq and coqide. Standard syntax:
+  to start the remote browser both in |Coq| and |CoqIDE|. Standard syntax:
   "%s" is the placeholder for the URL.
 
 Details of changes in 8.1gamma
@@ -7256,7 +7256,7 @@ Version 8.0
 Summary of changes
 ~~~~~~~~~~~~~~~~~~
 
-Coq version 8 is a major revision of the |Coq| proof assistant. First, the
+|Coq| version 8 is a major revision of the |Coq| proof assistant. First, the
 underlying logic is slightly different. The so-called *impredicativity*
 of the sort Set has been dropped. The main reason is that it is
 inconsistent with the principle of description which is quite a useful
@@ -7294,7 +7294,7 @@ purpose here is a better uniformity making the tactics and commands
 easier to use and to remember.
 
 Thirdly, a restructuring and uniformization of the standard library of
-Coq has been performed. There is now just one Leibniz equality usable
+|Coq| has been performed. There is now just one Leibniz equality usable
 for all the different kinds of |Coq| objects. Also, the set of real
 numbers now lies at the same level as the sets of natural and integer
 numbers. Finally, the names of the standard properties of numbers now
@@ -7511,19 +7511,19 @@ Miscellaneous
 
 Incompatibilities
 
-- Persistence of true_sub (4 incompatibilities in Coq user contributions)
+- Persistence of true_sub (4 incompatibilities in |Coq| user contributions)
 - Variable names of some constants changed for a better uniformity (2 changes
-  in Coq user contributions)
+  in |Coq| user contributions)
 - Naming of quantified names in goal now avoid global names (2 occurrences)
 - NewInduction naming for inductive types with functional arguments
-  (no incompatibility in Coq user contributions)
+  (no incompatibility in |Coq| user contributions)
 - Contradiction now solve more goals (source of 2 incompatibilities)
 - Merge of eq and eqT may exceptionally result in subgoals now
   solved automatically
 - Redundant pairs of ZArith lemmas may have different names: it may
   cause "Apply/Rewrite with" to fail if using the first name of a pair
   of redundant lemmas (this is solved by renaming the variables bound by
-  "with"; 3 incompatibilities in Coq user contribs)
+  "with"; 3 incompatibilities in |Coq| user contribs)
 - ML programs referring to constants from fast_integer.v must use
   "Coqlib.gen_constant_modules Coqlib.zarith_base_modules" instead
 
@@ -7559,7 +7559,7 @@ Revision of the standard library
   "Zmult_le_compat_r", "SUPERIEUR" -> "Gt", "ZERO" -> "Z0")
 - Order and names of arguments of basic lemmas on nat, Z, positive and R
   have been made uniform.
-- Notions of Coq initial state are declared with (strict) implicit arguments
+- Notions of |Coq| initial state are declared with (strict) implicit arguments
 - eq merged with eqT: old eq disappear, new eq (written =) is old eqT
   and new eqT is syntactic sugar for new eq (notation == is an alias
   for = and is written as it, exceptional source of incompatibilities)
@@ -7590,7 +7590,7 @@ Known problems of the automatic translation
 - iso-latin-1 characters are no longer supported: move your files to
   7-bits ASCII or unicode before translation (switch to unicode is
   automatically done if a file is loaded and saved again by coqide)
-- Renaming in ZArith: incompatibilities in Coq user contribs due to
+- Renaming in ZArith: incompatibilities in |Coq| user contribs due to
   merging names INZ, from Reals, and inject_nat.
 - Renaming and new lemmas in ZArith: may clash with names used by users
 - Restructuration of ZArith: replace requirement of specific modules
@@ -7640,7 +7640,7 @@ Tactics and the tactic Language
 Executables and tools
 
 - Added option -top to change the name of the toplevel module "Top"
-- Coqdoc updated to new syntax and now part of Coq sources
+- Coqdoc updated to new syntax and now part of |Coq| sources
 - XML exportation tool now exports the structure of vernacular files
   (cf chapter 13 in the reference manual)
 
diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst
index 02821613cc..bab9bfcadb 100644
--- a/doc/sphinx/history.rst
+++ b/doc/sphinx/history.rst
@@ -1,16 +1,16 @@
 .. _history:
 
---------------------
-Early history of Coq
---------------------
+----------------------
+Early history of |Coq|
+----------------------
 
 Historical roots
 ----------------
 
-Coq is a proof assistant for higher-order logic, allowing the
+|Coq| is a proof assistant for higher-order logic, allowing the
 development of computer programs consistent with their formal
 specification. It is the result of about ten years [#years]_ of research
-of the Coq project. We shall briefly survey here three main aspects: the
+of the |Coq| project. We shall briefly survey here three main aspects: the
 *logical language* in which we write our axiomatizations and
 specifications, the *proof assistant* which allows the development of
 verified mathematical proofs, and the *program extractor* which
@@ -153,7 +153,7 @@ by A. Felty. It allowed operation of the theorem-prover through the
 manipulation of windows, menus, mouse-sensitive buttons, and other
 widgets. This system (Version 5.6) was released in 1991.
 
-Coq was ported to the new implementation Caml-light of X. Leroy and D.
+|Coq| was ported to the new implementation Caml-light of X. Leroy and D.
 Doligez by D. de Rauglaudre (Version 5.7) in 1992. A new version of |Coq|
 was then coordinated by C. Murthy, with new tools designed by C. Parent
 to prove properties of ML programs (this methodology is dual to program
@@ -477,7 +477,7 @@ C. Paulin-Mohring. *Inductively defined types* :cite:`CP90`.
 
 This led to the Calculus of Inductive Constructions, logical formalism
 implemented in Versions 5 upward of the system, and documented in:
-C. Paulin-Mohring. *Inductive Definitions in the System Coq - Rules
+C. Paulin-Mohring. *Inductive Definitions in the System |Coq| - Rules
 and Properties* :cite:`P93`.
 
 The last version of CONSTR is Version 4.11, which was last distributed
@@ -489,7 +489,7 @@ Version 5
 ~~~~~~~~~
 
 At the end of 1989, Version 5.1 was started, and renamed as the system
-Coq for the Calculus of Inductive Constructions. It was then ported to
+|Coq| for the Calculus of Inductive Constructions. It was then ported to
 the new stand-alone implementation of ML called Caml-light.
 
 In 1990 many changes occurred. Thierry Coquand left for Chalmers
@@ -497,7 +497,7 @@ University in Göteborg. Christine Paulin-Mohring took a CNRS
 researcher position at the LIP laboratory of École Normale Supérieure
 de Lyon. Project Formel was terminated, and gave rise to two teams:
 Cristal at INRIA-Roquencourt, that continued developments in
-functional programming with Caml-light then OCaml, and Coq, continuing
+functional programming with Caml-light then OCaml, and |Coq|, continuing
 the type theory research, with a joint team headed by Gérard Huet at
 INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory
 of CNRS-ENS Lyon.
@@ -736,7 +736,7 @@ Notes:
 Main novelties
 ^^^^^^^^^^^^^^
 
-References are to Coq 7.1 reference manual
+References are to |Coq| 7.1 reference manual
 
 - New primitive let-in construct (see sections 1.2.8 and )
 - Long names (see sections 2.6 and 2.7)
@@ -770,7 +770,7 @@ Language: long names
   name, the name of the module in which they are defined (Top if in
   coqtop), and possibly an arbitrary long sequence of directory (e.g.
   "Coq.Lists.PolyList.flat_map" where "Coq" means that "flat_map" is part
-  of Coq standard library, "Lists" means it is defined in the Lists
+  of |Coq| standard library, "Lists" means it is defined in the Lists
   library and "PolyList" means it is in the file Polylist) (+)
 
 - Constructions can be referred by their base name, or, in case of
@@ -829,7 +829,7 @@ Reduction
 - Constants declared as opaque (using Qed) can no longer become
   transparent (a constant intended to be alternatively opaque and
   transparent must be declared as transparent (using Defined)); a risk
-  exists (until next Coq version) that Simpl and Hnf reduces opaque
+  exists (until next |Coq| version) that Simpl and Hnf reduces opaque
   constants (*)
 
 
@@ -1171,7 +1171,7 @@ Incompatibilities
 
 - New naming strategy for NewInduction/NewDestruct may affect 7.1 compatibility
 - Extra parentheses may exceptionally be needed in tactic definitions.
-- Coq extensions written in Ocaml need to be updated (see dev/changements.txt
+- |Coq| extensions written in |OCaml| need to be updated (see dev/changements.txt
   for a description of the main changes in the interface files of V7.2)
 - New behaviour of Intuition/Tauto may exceptionally lead to incompatibilities
 
@@ -1205,7 +1205,7 @@ Tactics
   product if needed (source of incompatibilities)
 - "Match Context" now matching more recent hypotheses first and failing only
   on user errors and Fail tactic (possible source of incompatibilities)
-- Tactic Definition's without arguments now allowed in Coq states
+- Tactic Definition's without arguments now allowed in |Coq| states
 - Better simplification and discrimination made by Inversion (source
   of incompatibilities)
 
@@ -1239,7 +1239,7 @@ User Contributions
 - CongruenceClosure (congruence closure decision procedure)
   [Pierre Corbineau, ENS Cachan]
 - MapleMode (an interface to embed Maple simplification procedures over
-  rational fractions in Coq)
+  rational fractions in |Coq|)
   [David Delahaye, Micaela Mayero, Chalmers University]
 - Presburger: A formalization of Presburger's algorithm
   [Laurent Thery, INRIA Sophia Antipolis]
@@ -1283,7 +1283,7 @@ Bug fixes
 
 Misc
 
-  - Ocaml version >= 3.06 is needed to compile Coq from sources
+  - Ocaml version >= 3.06 is needed to compile |Coq| from sources
   - Simplification of fresh names creation strategy for Assert, Pose and
     LetTac (#1402)
 
@@ -1398,7 +1398,7 @@ Extraction (See details in plugins/extraction/CHANGES and README):
 - An experimental Scheme extraction is provided.
 - Concerning OCaml, extracted code is now ensured to always type check,
   thanks to automatic inserting of Obj.magic.
-- Experimental extraction of Coq new modules to Ocaml modules.
+- Experimental extraction of |Coq| new modules to Ocaml modules.
 
 Proof rendering in natural language
 
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index b059fb4069..dc16897d42 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -1,8 +1,8 @@
-This is the reference manual of |Coq|.  Coq is an interactive theorem
+This is the reference manual of |Coq|.  |Coq| is an interactive theorem
 prover.  It lets you formalize mathematical concepts and then helps
 you interactively generate machine-checked proofs of theorems.
 Machine checking gives users much more confidence that the proofs are
-correct compared to human-generated and -checked proofs.  Coq has been
+correct compared to human-generated and -checked proofs.  |Coq| has been
 used in a number of flagship verification projects, including the
 `CompCert verified C compiler <http://compcert.inria.fr/>`_, and has
 served to verify the proof of the `four color theorem
@@ -18,49 +18,49 @@ arithmetic).  :ref:`Ltac <ltac>` and its planned replacement,
 combining existing tactics with looping and conditional constructs.
 These permit automation of large parts of proofs and sometimes entire
 proofs.  Furthermore, users can add novel tactics or functionality by
-creating Coq plugins using OCaml.
+creating |Coq| plugins using |OCaml|.
 
-The Coq kernel, a small part of Coq, does the final verification that
+The |Coq| kernel, a small part of |Coq|, does the final verification that
 the tactic-generated proof is valid.  Usually the tactic-generated
 proof is indeed correct, but delegating proof verification to the
 kernel means that even if a tactic is buggy, it won't be able to
 introduce an incorrect proof into the system.
 
-Finally, Coq also supports extraction of verified programs to
-programming languages such as OCaml and Haskell.  This provides a way
-of executing Coq code efficiently and can be used to create verified
+Finally, |Coq| also supports extraction of verified programs to
+programming languages such as |OCaml| and Haskell.  This provides a way
+of executing |Coq| code efficiently and can be used to create verified
 software libraries.
 
-To learn Coq, beginners are advised to first start with a tutorial /
+To learn |Coq|, beginners are advised to first start with a tutorial /
 book.  Several such tutorials / books are listed at
 https://coq.inria.fr/documentation.
 
 This manual is organized in three main parts, plus an appendix:
 
-- **The first part presents the specification language of Coq**, that
+- **The first part presents the specification language of |Coq|**, that
   allows to define programs and state mathematical theorems.
-  :ref:`core-language` presents the language that the kernel of Coq
+  :ref:`core-language` presents the language that the kernel of |Coq|
   understands.  :ref:`extensions` presents the richer language, with
   notations, implicits, etc. that a user can use and which is
   translated down to the language of the kernel by means of an
   "elaboration process".
 
 - **The second part presents the interactive proof mode**, the central
-  feature of Coq.  :ref:`writing-proofs` introduces this interactive
+  feature of |Coq|.  :ref:`writing-proofs` introduces this interactive
   proof mode and the available proof languages.
   :ref:`automatic-tactics` presents some more advanced tactics, while
   :ref:`writing-tactics` is about the languages that allow a user to
   combine tactics together and develop new ones.
 
-- **The third part shows how to use Coq in practice.**
+- **The third part shows how to use |Coq| in practice.**
   :ref:`libraries` presents some of the essential reusable blocks from
   the ecosystem and some particularly important extensions such as the
   program extraction mechanism.  :ref:`tools` documents important
-  tools that a user needs to build a Coq project.
+  tools that a user needs to build a |Coq| project.
 
 - In the appendix, :ref:`history-and-changes` presents the history of
-  Coq and changes in recent releases.  This is an important reference
-  if you upgrade the version of Coq that you use.  The various
+  |Coq| and changes in recent releases.  This is an important reference
+  if you upgrade the version of |Coq| that you use.  The various
   :ref:`indexes <indexes>` are very useful to **quickly browse the
   manual and find what you are looking for.** They are often the main
   entry point to the manual.
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 41e1c30f0d..6cdc272fd4 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -117,7 +117,7 @@ Assumptions
 
 Assumptions extend the environment with axioms, parameters, hypotheses
 or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted
-by Coq if and only if this :n:`@type` is a correct type in the environment
+by |Coq| if and only if this :n:`@type` is a correct type in the environment
 preexisting the declaration and if :n:`@ident` was not previously defined in
 the same module. This :n:`@type` is considered to be the type (or
 specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident`
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 45bdc019ac..3cc3fe231a 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -134,7 +134,7 @@ Numbers
      hexdigit ::= {| 0 .. 9 | a .. f | A .. F }
 
   :n:`@integer` and :n:`@natural` are limited to the range that fits
-  into an OCaml integer (63-bit integers on most architectures).
+  into an |OCaml| integer (63-bit integers on most architectures).
   :n:`@bigint` and :n:`@bignat` have no range limitation.
 
   The :ref:`standard library <thecoqlibrary>` provides some
@@ -152,8 +152,8 @@ Strings
   :token:`string`.
 
 Keywords
-  The following character sequences are keywords defined in the main Coq grammar
-  that cannot be used as identifiers (even when starting Coq with the `-noinit`
+  The following character sequences are keywords defined in the main |Coq| grammar
+  that cannot be used as identifiers (even when starting |Coq| with the `-noinit`
   command-line flag)::
 
     _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop
@@ -168,8 +168,8 @@ Keywords
   keywords.
 
 Other tokens
-  The following character sequences are tokens defined in the main Coq grammar
-  (even when starting Coq with the `-noinit` command-line flag)::
+  The following character sequences are tokens defined in the main |Coq| grammar
+  (even when starting |Coq| with the `-noinit` command-line flag)::
 
     ! #[ % & ' ( () ) * + , - ->
     . .( .. ... / : ::= := :> :>> ; < <+ <- <:
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index c034b7f302..0520afd600 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -76,7 +76,7 @@ propositional η-equality, which itself would require full η-conversion for
 subject reduction to hold, but full η-conversion is not acceptable as it would
 make type checking undecidable.
 
-Since the introduction of primitive records in Coq 8.5, an alternative
+Since the introduction of primitive records in |Coq| 8.5, an alternative
 presentation is available, called *negative co-inductive types*. This consists
 in defining a co-inductive type as a primitive record type through its
 projections. Such a technique is akin to the *co-pattern* style that can be
@@ -115,7 +115,7 @@ equality:
 
    Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2.
 
-As of Coq 8.9, it is now advised to use negative co-inductive types rather than
+As of |Coq| 8.9, it is now advised to use negative co-inductive types rather than
 their positive counterparts.
 
 .. seealso::
@@ -195,7 +195,7 @@ Top-level definitions of co-recursive functions
    As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously
    defining several mutual cofixpoints.
 
-   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
+   If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 42203d9d65..592b16a72f 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -90,7 +90,7 @@ Section :ref:`typing-rules`.
    :attr:`universes(monomorphic)`, :attr:`program` and
    :attr:`canonical` attributes.
 
-   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
+   If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
@@ -135,7 +135,7 @@ Chapter :ref:`Tactics`. The basic assertion command is:
       | Proposition
       | Property
 
-   After the statement is asserted, Coq needs a proof. Once a proof of
+   After the statement is asserted, |Coq| needs a proof. Once a proof of
    :n:`@type` under the assumptions represented by :n:`@binder`\s is given and
    validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and
    the theorem is bound to the name :n:`@ident` in the environment.
@@ -172,7 +172,7 @@ Chapter :ref:`Tactics`. The basic assertion command is:
       This feature, called nested proofs, is disabled by default.
       To activate it, turn the :flag:`Nested Proofs Allowed` flag on.
 
-Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode
+Proofs start with the keyword :cmd:`Proof`. Then |Coq| enters the proof editing mode
 until the proof is completed. In proof editing mode, the user primarily enters
 tactics, which are described in chapter :ref:`Tactics`. The user may also enter
 commands to manage the proof editing mode. They are described in Chapter
diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst
index de780db267..c7b1df28db 100644
--- a/doc/sphinx/language/core/index.rst
+++ b/doc/sphinx/language/core/index.rst
@@ -4,7 +4,7 @@
 Core language
 =============
 
-At the heart of the Coq proof assistant is the Coq kernel.  While
+At the heart of the |Coq| proof assistant is the |Coq| kernel.  While
 users have access to a language with many convenient features such as
 :ref:`notations <syntax-extensions-and-notation-scopes>`,
 :ref:`implicit arguments <ImplicitArguments>`, etc.  (presented in the
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 39b154de8d..0b18c9dcf1 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -17,7 +17,7 @@ Inductive types
       constructor ::= @ident {* @binder } {? @of_type }
 
    This command defines one or more
-   inductive types and its constructors.  Coq generates destructors
+   inductive types and its constructors.  |Coq| generates destructors
    depending on the universe that the inductive type belongs to.
 
    The destructors are named :n:`@ident`\ ``_rect``, :n:`@ident`\ ``_ind``,
@@ -405,7 +405,7 @@ constructions.
    It is especially useful when defining functions over mutually defined
    inductive types.  Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`.
 
-   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
+   If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 866104d5d1..1309a47ff4 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -1001,12 +1001,12 @@ of the ``Require`` command can be used to bypass the implicit shortening
 by providing an absolute root to the required file (see :ref:`compiled-files`).
 
 There also exists another independent loadpath mechanism attached to
-OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object
-files as described above. The OCaml loadpath is managed using
-the option ``-I`` `path` (in the OCaml world, there is neither a
+|OCaml| object files (``.cmo`` or ``.cmxs``) rather than |Coq| object
+files as described above. The |OCaml| loadpath is managed using
+the option ``-I`` `path` (in the |OCaml| world, there is neither a
 notion of logical name prefix nor a way to access files in
 subdirectories of path). See the command :cmd:`Declare ML Module` in
-:ref:`compiled-files` to understand the need of the OCaml loadpath.
+:ref:`compiled-files` to understand the need of the |OCaml| loadpath.
 
 See :ref:`command-line-options` for a more general view over the |Coq| command
 line options.
diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst
index 48647deeff..17f569ca2a 100644
--- a/doc/sphinx/language/core/primitive.rst
+++ b/doc/sphinx/language/core/primitive.rst
@@ -45,13 +45,13 @@ applications of these primitive operations.
 
 The extraction of these primitives can be customized similarly to the extraction
 of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63`
-module can be used when extracting to OCaml: it maps the Coq primitives to types
-and functions of a :g:`Uint63` module. Said OCaml module is not produced by
+module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types
+and functions of a :g:`Uint63` module. That |OCaml| module is not produced by
 extraction. Instead, it has to be provided by the user (if they want to compile
 or execute the extracted code). For instance, an implementation of this module
-can be taken from the kernel of Coq.
+can be taken from the kernel of |Coq|.
 
-Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values
+Literal values (at type :g:`Int63.int`) are extracted to literal |OCaml| values
 wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on
 64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the
 function :g:`Uint63.compile` from the kernel).
@@ -94,13 +94,13 @@ to comply with the IEEE 754 standard for floating-point arithmetic.
 
 The extraction of these primitives can be customized similarly to the extraction
 of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats`
-module can be used when extracting to OCaml: it maps the Coq primitives to types
-and functions of a :g:`Float64` module. Said OCaml module is not produced by
+module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types
+and functions of a :g:`Float64` module. Said |OCaml| module is not produced by
 extraction. Instead, it has to be provided by the user (if they want to compile
 or execute the extracted code). For instance, an implementation of this module
-can be taken from the kernel of Coq.
+can be taken from the kernel of |Coq|.
 
-Literal values (of type :g:`Float64.t`) are extracted to literal OCaml
+Literal values (of type :g:`Float64.t`) are extracted to literal |OCaml|
 values (of type :g:`float`) written in hexadecimal notation and
 wrapped into the :g:`Float64.of_float` constructor, e.g.:
 :g:`Float64.of_float (0x1p+0)`.
@@ -144,19 +144,19 @@ operations.
 
 The extraction of these primitives can be customized similarly to the extraction
 of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlPArray`
-module can be used when extracting to OCaml: it maps the Coq primitives to types
-and functions of a :g:`Parray` module. Said OCaml module is not produced by
+module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types
+and functions of a :g:`Parray` module. Said |OCaml| module is not produced by
 extraction. Instead, it has to be provided by the user (if they want to compile
 or execute the extracted code). For instance, an implementation of this module
-can be taken from the kernel of Coq (see ``kernel/parray.ml``).
+can be taken from the kernel of |Coq| (see ``kernel/parray.ml``).
 
-Coq's primitive arrays are persistent data structures. Semantically, a set operation
+|Coq|'s primitive arrays are persistent data structures. Semantically, a set operation
 ``t.[i <- a]`` represents a new array that has the same values as ``t``, except
 at position ``i`` where its value is ``a``. The array ``t`` still exists, can
 still be used and its values were not modified. Operationally, the implementation
-of Coq's primitive arrays is optimized so that the new array ``t.[i <- a]`` does not
+of |Coq|'s primitive arrays is optimized so that the new array ``t.[i <- a]`` does not
 copy all of ``t``. The details are in section 2.3 of :cite:`ConchonFilliatre07wml`.
-In short, the implementation keeps one version of ``t`` as an OCaml native array and
+In short, the implementation keeps one version of ``t`` as an |OCaml| native array and
 other versions as lists of modifications to ``t``. Accesses to the native array
 version are constant time operations. However, accesses to versions where all the cells of
 the array are modified have O(n) access time, the same as a list. The version that is kept as the native array
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
index df50dbafe3..c70f7a347b 100644
--- a/doc/sphinx/language/core/sections.rst
+++ b/doc/sphinx/language/core/sections.rst
@@ -84,7 +84,7 @@ Sections create local contexts which can be shared across multiple definitions.
    will be wrapped with a :n:`@term_let` with the same declaration.
 
    As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`,
-   if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
+   if :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 0ae9fab7ab..29877e1b32 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -377,7 +377,7 @@ Effects of :cmd:`Arguments` on unfolding
 Bidirectionality hints
 ~~~~~~~~~~~~~~~~~~~~~~
 
-When type-checking an application, Coq normally does not use information from
+When type-checking an application, |Coq| normally does not use information from
 the context to infer the types of the arguments. It only checks after the fact
 that the type inferred for the application is coherent with the expected type.
 Bidirectionality hints make it possible to specify that after type-checking the
@@ -394,7 +394,7 @@ the context to help inferring the types of the remaining arguments.
   * *type inference*, with is inferring the type of a construct by analyzing the construct.
 
   Methods that combine these approaches are known as *bidirectional typing*.
-  Coq normally uses only the first approach to infer the types of arguments,
+  |Coq| normally uses only the first approach to infer the types of arguments,
   then later verifies that the inferred type is consistent with the expected type.
   *Bidirectionality hints* specify to use both methods: after type checking the
   first arguments of an application (appearing before the `&` in :cmd:`Arguments`),
@@ -416,7 +416,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`).
       Definition b2n (b : bool) := if b then 1 else 0.
       Coercion b2n : bool >-> nat.
 
-   Coq cannot automatically coerce existential statements over ``bool`` to
+   |Coq| cannot automatically coerce existential statements over ``bool`` to
    statements over ``nat``, because the need for inserting a coercion is known
    only from the expected type of a subterm:
 
@@ -431,7 +431,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`).
       Arguments ex_intro _ _ & _ _.
       Check (ex_intro _ true _ : exists n : nat, n > 0).
 
-Coq will attempt to produce a term which uses the arguments you
+|Coq| will attempt to produce a term which uses the arguments you
 provided, but in some cases involving Program mode the arguments after
 the bidirectionality starts may be replaced by convertible but
 syntactically different terms.
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index bfda8befff..38c9fa336d 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -159,7 +159,7 @@ of the terms that are compared.
     End theory.
   End EQ.
 
-We use Coq modules as namespaces. This allows us to follow the same
+We use |Coq| modules as namespaces. This allows us to follow the same
 pattern and naming convention for the rest of the chapter. The base
 namespace contains the definitions of the algebraic structure. To
 keep the example small, the algebraic structure ``EQ.type`` we are
@@ -224,7 +224,7 @@ example work:
   Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b).
 
 The error message is telling that |Coq| has no idea on how to compare
-pairs of objects. The following construction is telling Coq exactly
+pairs of objects. The following construction is telling |Coq| exactly
 how to do that.
 
 .. coqtop:: all
diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
index 20f4310d13..dc208a63a0 100644
--- a/doc/sphinx/language/extensions/evars.rst
+++ b/doc/sphinx/language/extensions/evars.rst
@@ -68,7 +68,7 @@ Inferable subterms
 ~~~~~~~~~~~~~~~~~~
 
 Expressions often contain redundant pieces of information. Subterms that can be
-automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will
+automatically inferred by |Coq| can be replaced by the symbol ``_`` and |Coq| will
 guess the missing piece of information.
 
 .. extracted from Gallina extensions chapter
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index f8375e93ce..9457505feb 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -115,7 +115,7 @@ application will include that argument.  Otherwise, the argument is
 *non-maximally inserted* and the partial application will not include that argument.
 
 Each implicit argument can be declared to be inserted maximally or non
-maximally. In Coq, maximally inserted implicit arguments are written between curly braces
+maximally. In |Coq|, maximally inserted implicit arguments are written between curly braces
 "{ }" and non-maximally inserted implicit arguments are written in square brackets "[ ]".
 
 .. seealso:: :flag:`Maximal Implicit Insertion`
diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst
index ed207ca743..ea7271179e 100644
--- a/doc/sphinx/language/extensions/index.rst
+++ b/doc/sphinx/language/extensions/index.rst
@@ -4,7 +4,7 @@
 Language extensions
 ===================
 
-Elaboration extends the language accepted by the Coq kernel to make it
+Elaboration extends the language accepted by the |Coq| kernel to make it
 easier to use.  For example, this lets the user omit most type
 annotations because they can be inferred, call functions with implicit
 arguments which will be inferred as well, extend the syntax with
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index c36b9deef3..561262262b 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -639,7 +639,7 @@ Dependent pattern matching
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The examples given so far do not need an explicit elimination
-predicate because all the |rhs| have the same type and Coq
+predicate because all the |rhs| have the same type and |Coq|
 succeeds to synthesize it. Unfortunately when dealing with dependent
 patterns it often happens that we need to write cases where the types
 of the |rhs| are different instances of the elimination predicate. The
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index ec182ce08f..59e1c65a49 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -24,13 +24,13 @@ develop his theories and proofs step by step. The |Coq| toplevel is run
 by the command ``coqtop``.
 
 There are two different binary images of |Coq|: the byte-code one and the
-native-code one (if OCaml provides a native-code compiler for
+native-code one (if |OCaml| provides a native-code compiler for
 your platform, which is supposed in the following). By default,
 ``coqtop`` executes the native-code version; run ``coqtop.byte`` to get
 the byte-code version.
 
-The byte-code toplevel is based on an OCaml toplevel (to
-allow dynamic linking of tactics). You can switch to the OCaml toplevel
+The byte-code toplevel is based on an |OCaml| toplevel (to
+allow dynamic linking of tactics). You can switch to the |OCaml| toplevel
 with the command ``Drop.``, and come back to the |Coq|
 toplevel with the command ``Coqloop.loop();;``.
 
@@ -61,7 +61,7 @@ By resource file
 
 When |Coq| is launched, with either ``coqtop`` or ``coqc``, the
 resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will
-be implicitly prepended to any document read by Coq, whether it is an
+be implicitly prepended to any document read by |Coq|, whether it is an
 interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME``
 is the configuration directory of the user (by default it's ``~/.config``)
 and ``xxx`` is the version number (e.g. 8.8). If
@@ -133,7 +133,7 @@ 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.
+  to the |OCaml| loadpath.
 
   .. seealso::
 
@@ -253,8 +253,8 @@ and ``coqtop``, unless stated otherwise:
 
   .. 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. Within Coq, the :flag:`Mangle Names` flag turns this behavior on,
+  |Coq|'s auto-generated name scheme with names of the form *ident0*, *ident1*,
+  etc. Within |Coq|, the :flag:`Mangle Names` flag turns this behavior on,
   and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature
   is intended to be used as a linter for developments that want to be robust to
   changes in the auto-generated name scheme. The options are provided to
@@ -264,7 +264,7 @@ and ``coqtop``, unless stated otherwise:
    type of the option. For flags :n:`@setting_name` is equivalent to
    :n:`@setting_name=true`. For instance ``-set "Universe Polymorphism"``
    will enable :flag:`Universe Polymorphism`. Note that the quotes are
-   shell syntax, Coq does not see them.
+   shell syntax, |Coq| does not see them.
    See the :ref:`note above <interleave-command-line>` regarding the order
    of command-line options.
 :-unset *string*: As ``-set`` but used to disable options and flags.
@@ -304,7 +304,7 @@ and ``coqtop``, unless stated otherwise:
 Compiled interfaces (produced using ``-vos``)
 ----------------------------------------------
 
-Compiled interfaces help saving time while developing Coq formalizations,
+Compiled interfaces help saving time while developing |Coq| formalizations,
 by compiling the formal statements exported by a library independently of
 the proofs that it contains.
 
@@ -473,7 +473,7 @@ set of reflexive transitive dependencies of set :math:`S`. Then:
   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
+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
 course, the latter is slightly slower since it makes more disk access.
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index 42e752841d..64b433115c 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -5,9 +5,9 @@
 |Coq| Integrated Development Environment
 ========================================
 
-The Coq Integrated Development Environment is a graphical tool, to be
+The |Coq| Integrated Development Environment is a graphical tool, to be
 used as a user-friendly replacement to `coqtop`. Its main purpose is to
-allow the user to navigate forward and backward into a Coq vernacular
+allow the user to navigate forward and backward into a |Coq| vernacular
 file, executing corresponding commands or undoing them respectively.
 
 |CoqIDE| is run by typing the command `coqide` on the command line.
@@ -23,7 +23,7 @@ no meaning for |CoqIDE| being ignored.
      :alt: |CoqIDE| main screen
 
 A sample |CoqIDE| main screen, while navigating into a file `Fermat.v`,
-is shown in the figure :ref:`CoqIDE main screen <coqide_mainscreen>`.
+is shown in the figure :ref:`|CoqIDE| main screen <coqide_mainscreen>`.
 At the top is a menu bar, and a tool bar
 below it. The large window on the left is displaying the various
 *script buffers*. The upper right window is the *goal window*, where
@@ -39,7 +39,7 @@ The *File* menu allows you to open files or create some, save them,
 print or export them into various formats. Among all these buffers,
 there is always one which is the current *running buffer*, whose name
 is displayed on a background in the *processed* color (green by default), which
-is the one where Coq commands are currently executed.
+is the one where |Coq| commands are currently executed.
 
 Buffers may be edited as in any text editor, and classical basic
 editing commands (Copy/Paste, …) are available in the *Edit* menu.
@@ -47,7 +47,7 @@ editing commands (Copy/Paste, …) are available in the *Edit* menu.
 editing commands, you may launch your favorite text editor on the
 current buffer, using the *Edit/External Editor* menu.
 
-Interactive navigation into Coq scripts
+Interactive navigation into |Coq| scripts
 --------------------------------------------
 
 The running buffer is the one where navigation takes place. The toolbar offers
@@ -58,7 +58,7 @@ processed color. If that command fails, the error message is displayed in the
 message window, and the location of the error is emphasized by an underline in
 the error foreground color (red by default).
 
-In the figure :ref:`CoqIDE main screen <coqide_mainscreen>`,
+In the figure :ref:`|CoqIDE| main screen <coqide_mainscreen>`,
 the running buffer is `Fermat.v`, all commands until
 the ``Theorem`` have been already executed, and the user tried to go
 forward executing ``Induction n``. That command failed because no such
@@ -153,7 +153,7 @@ as standard |GtkSourceView| styles are available. Other styles can be
 added e.g. in ``$HOME/.local/share/gtksourceview-3.0/styles/`` (see
 the general documentation about |GtkSourceView| for the various
 possibilities). Note that the style of the rest of graphical part of
-Coqide is not under the control of |GtkSourceView| but of GTK+ and
+|CoqIDE| is not under the control of |GtkSourceView| but of GTK+ and
 governed by files such as ``settings.ini`` and ``gtk.css`` in
 ``$XDG_CONFIG_HOME/gtk-3.0`` or files in
 ``$HOME/.themes/NameOfTheme/gtk-3.0``, as well as the environment
@@ -219,7 +219,7 @@ mathematical symbols ∀ and ∃, you may define:
      : type_scope.
 
 There exists a small set of such notations already defined, in the
-file `utf8.v` of Coq library, so you may enable them just by
+file `utf8.v` of |Coq| library, so you may enable them just by
 ``Require Import Unicode.Utf8`` inside |CoqIDE|, or equivalently,
 by starting |CoqIDE| with ``coqide -l utf8``.
 
@@ -237,7 +237,7 @@ use antialiased fonts or not, by setting the environment variable
 Bindings for input of Unicode symbols
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-CoqIDE supports a builtin mechanism to input non-ASCII symbols.
+|CoqIDE| supports a builtin mechanism to input non-ASCII symbols.
 For example, to input ``π``, it suffices to type ``\pi`` then press the
 combination of key ``Shift+Space`` (default key binding). Often, it
 suffices to type a prefix of the latex token, e.g. typing ``\p``
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index daae46ad11..c3286199e8 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -8,8 +8,8 @@ The distribution provides utilities to simplify some tedious works
 beside proof development, tactics writing or documentation.
 
 
-Using Coq as a library
-----------------------
+Using |Coq| as a library
+------------------------
 
 In previous versions, ``coqmktop`` was used to build custom
 toplevels - for example for better debugging or custom static
@@ -37,10 +37,10 @@ and similarly for other plugins.
 Building a |Coq| project
 ------------------------
 
-As of today it is possible to build Coq projects using two tools:
+As of today it is possible to build |Coq| projects using two tools:
 
-- coq_makefile, which is distributed by Coq and is based on generating a makefile,
-- Dune, the standard OCaml build tool, which, since version 1.9, supports building Coq libraries.
+- coq_makefile, which is distributed by |Coq| and is based on generating a makefile,
+- Dune, the standard |OCaml| build tool, which, since version 1.9, supports building |Coq| libraries.
 
 .. _coq_makefile:
 
@@ -142,7 +142,7 @@ Here we describe only few of them.
 
 :CAMLPKGS:
    can be used to specify third party findlib packages, and is
-   passed to the OCaml compiler on building or linking of modules. Eg:
+   passed to the |OCaml| compiler on building or linking of modules. Eg:
    ``-package yojson``.
 :CAMLFLAGS:
    can be used to specify additional flags to the |OCaml|
@@ -150,15 +150,15 @@ Here we describe only few of them.
 :OCAMLWARN:
    it contains a default of ``-warn-error +a-3``, useful to modify
    this setting; beware this is not recommended for projects in
-   Coq's CI.
+   |Coq|'s CI.
 :COQC, COQDEP, COQDOC:
    can be set in order to use alternative binaries
    (e.g. wrappers)
 :COQ_SRC_SUBDIRS:
    can be extended by including other paths in which ``*.cm*`` files
    are searched. For example ``COQ_SRC_SUBDIRS+=user-contrib/Unicoq``
-   lets you build a plugin containing OCaml code that depends on the
-   OCaml code of ``Unicoq``
+   lets you build a plugin containing |OCaml| code that depends on the
+   |OCaml| code of ``Unicoq``
 :COQFLAGS:
    override the flags passed to ``coqc``. By default ``-q``.
 :COQEXTRAFLAGS:
@@ -172,7 +172,7 @@ Here we describe only few of them.
 :COQDOCEXTRAFLAGS:
    extend the flags passed to ``coqdoc``
 :COQLIBINSTALL, COQDOCINSTALL:
-   specify where the Coq libraries and documentation will be installed.
+   specify where the |Coq| libraries and documentation will be installed.
    By default a combination of ``$(DESTDIR)`` (if defined) with
    ``$(COQLIB)/user-contrib`` and ``$(DOCDIR)/user-contrib``.
 
@@ -560,22 +560,22 @@ Building a |Coq| project with Dune
 
 .. note::
 
-   Dune's Coq support is still experimental; we strongly recommend
+   Dune's |Coq| support is still experimental; we strongly recommend
    using Dune 2.3 or later.
 
 .. note::
 
-   The canonical documentation for the Coq Dune extension is
+   The canonical documentation for the |Coq| Dune extension is
    maintained upstream; please refer to the `Dune manual
    <https://dune.readthedocs.io/>`_ for up-to-date information. This
    documentation is up to date for Dune 2.3.
 
-Building a Coq project with Dune requires setting up a Dune project
+Building a |Coq| project with Dune requires setting up a Dune project
 for your files. This involves adding a ``dune-project`` and
 ``pkg.opam`` file to the root (``pkg.opam`` can be empty or generated
 by Dune itself), and then providing ``dune`` files in the directories
 your ``.v`` files are placed. For the experimental version "0.1" of
-the Coq Dune language, |Coq| library stanzas look like:
+the |Coq| Dune language, |Coq| library stanzas look like:
 
 .. code:: scheme
 
@@ -592,12 +592,12 @@ the library under ``<module_prefix>``. If you declare an
 ``<opam_package>``, an ``.install`` file for the library will be
 generated; the optional ``(modules <ordered_set_lang>)`` field allows
 you to filter the list of modules, and ``(libraries
-<ocaml_libraries>)`` allows the Coq theory depend on ML plugins. For
-the moment, Dune relies on Coq's standard mechanisms (such as
-``COQPATH``) to locate installed Coq libraries.
+<ocaml_libraries>)`` allows the |Coq| theory depend on ML plugins. For
+the moment, Dune relies on |Coq|'s standard mechanisms (such as
+``COQPATH``) to locate installed |Coq| libraries.
 
 By default Dune will skip ``.v`` files present in subdirectories. In
-order to enable the usual recursive organization of Coq projects add
+order to enable the usual recursive organization of |Coq| projects add
 
 .. code:: scheme
 
@@ -611,7 +611,7 @@ of your project.
 
 .. example::
 
-   A typical stanza for a Coq plugin is split into two parts. An OCaml build directive, which is standard Dune:
+   A typical stanza for a |Coq| plugin is split into two parts. An |OCaml| build directive, which is standard Dune:
 
    .. code:: scheme
 
@@ -623,7 +623,7 @@ of your project.
 
        (coq.pp (modules g_equations))
 
-   And a Coq-specific part that depends on it via the ``libraries`` field:
+   And a |Coq|-specific part that depends on it via the ``libraries`` field:
 
    .. code:: scheme
 
@@ -656,10 +656,10 @@ command ``Declare ML Module``.
 See the man page of ``coqdep`` for more details and options.
 
 Both Dune and ``coq_makefile`` use ``coqdep`` to compute the
-dependencies among the files part of a Coq project.
+dependencies among the files part of a |Coq| project.
 
-Embedded Coq phrases inside |Latex| documents
----------------------------------------------
+Embedded |Coq| phrases inside |Latex| documents
+-----------------------------------------------
 
 When writing documentation about a proof development, one may want
 to insert |Coq| phrases inside a |Latex| document, possibly together
@@ -670,7 +670,7 @@ evaluates them, and insert the outcome of the evaluation after each
 phrase.
 
 Starting with a file ``file.tex`` containing |Coq| phrases, the ``coq-tex``
-filter produces a file named ``file.v.tex`` with the Coq outcome.
+filter produces a file named ``file.v.tex`` with the |Coq| outcome.
 
 There are options to produce the |Coq| parts in smaller font, italic,
 between horizontal rules, etc. See the man page of ``coq-tex`` for more
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
diff --git a/doc/sphinx/proofs/creating-tactics/index.rst b/doc/sphinx/proofs/creating-tactics/index.rst
index 1af1b0b726..f1d4fa789d 100644
--- a/doc/sphinx/proofs/creating-tactics/index.rst
+++ b/doc/sphinx/proofs/creating-tactics/index.rst
@@ -18,13 +18,13 @@ new tactics:
 
 - `Mtac2 <https://github.com/Mtac2/Mtac2>`_ is an external plugin
   which provides another typed tactic language.  While Ltac2 belongs
-  to the ML language family, Mtac2 reuses the language of Coq itself
-  as the language to build Coq tactics.
+  to the ML language family, Mtac2 reuses the language of |Coq| itself
+  as the language to build |Coq| tactics.
 
 - The most traditional way of building new complex tactics is to write
-  a Coq plugin in OCaml.  Beware that this also requires much more
-  effort and commitment.  A tutorial for writing Coq plugins is
-  available in the Coq repository in `doc/plugin_tutorial
+  a |Coq| plugin in |OCaml|.  Beware that this also requires much more
+  effort and commitment.  A tutorial for writing |Coq| plugins is
+  available in the |Coq| repository in `doc/plugin_tutorial
   <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_.
 
 .. toctree::
diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst
index a279a5957f..3f5526dba8 100644
--- a/doc/sphinx/proofs/writing-proofs/index.rst
+++ b/doc/sphinx/proofs/writing-proofs/index.rst
@@ -4,7 +4,7 @@
 Writing proofs
 ==============
 
-Coq is an interactive theorem prover, or proof assistant, which means
+|Coq| is an interactive theorem prover, or proof assistant, which means
 that proofs can be constructed interactively through a dialog between
 the user and the assistant.  The building blocks for this dialog are
 tactics which the user will use to represent steps in the proof of a
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 8e23e61018..19c7c659e0 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -128,7 +128,7 @@ Automatic declaration of schemes
 
 .. warning::
 
-   You have to be careful with these flags since Coq may now reject well-defined
+   You have to be careful with these flags since |Coq| may now reject well-defined
    inductive types because it cannot compute a Boolean equality for them.
 
 .. flag:: Rewriting Schemes
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index d6db305300..1791c53aa8 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -3,7 +3,7 @@
 Syntax extensions and notation scopes
 =====================================
 
-In this chapter, we introduce advanced commands to modify the way Coq
+In this chapter, we introduce advanced commands to modify the way |Coq|
 parses and prints objects, i.e. the translations between the concrete
 and internal representations of terms and commands.
 
@@ -71,7 +71,7 @@ least 3 characters and starting with a simple quote must be quoted
    Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3).
 
 A notation binds a syntactic expression to a term. Unless the parser
-and pretty-printer of Coq already know how to deal with the syntactic
+and pretty-printer of |Coq| already know how to deal with the syntactic
 expression (such as through :cmd:`Reserved Notation` or for notations
 that contain only literals), explicit precedences and
 associativity rules have to be given.
@@ -88,7 +88,7 @@ Precedences and associativity
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Mixing different symbolic notations in the same text may cause serious
-parsing ambiguity. To deal with the ambiguity of notations, Coq uses
+parsing ambiguity. To deal with the ambiguity of notations, |Coq| uses
 precedence levels ranging from 0 to 100 (plus one extra level numbered
 200) and associativity rules.
 
@@ -99,7 +99,7 @@ Consider for example the new notation
    Notation "A \/ B" := (or A B).
 
 Clearly, an expression such as :g:`forall A:Prop, True /\ A \/ A \/ False`
-is ambiguous. To tell the Coq parser how to interpret the
+is ambiguous. To tell the |Coq| parser how to interpret the
 expression, a priority between the symbols ``/\`` and ``\/`` has to be
 given. Assume for instance that we want conjunction to bind more than
 disjunction. This is expressed by assigning a precedence level to each
@@ -117,7 +117,7 @@ defaults to :g:`True /\ (False /\ False)` (right associativity) or to
 expression is not well-formed and that parentheses are mandatory (this is a “no
 associativity”) [#no_associativity]_. We do not know of a special convention for
 the associativity of disjunction and conjunction, so let us apply
-right associativity (which is the choice of Coq).
+right associativity (which is the choice of |Coq|).
 
 Precedence levels and associativity rules of notations are specified with a list of
 parenthesized :n:`@syntax_modifier`\s.  Here is how the previous examples refine:
@@ -187,7 +187,7 @@ left. See the next section for more about factorization.
 Simple factorization rules
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Coq extensible parsing is performed by *Camlp5* which is essentially a LL1
+|Coq| extensible parsing is performed by *Camlp5* which is essentially a LL1
 parser: it decides which notation to parse by looking at tokens from left to right.
 Hence, some care has to be taken not to hide already existing rules by new
 rules. Some simple left factorization work has to be done. Here is an example.
@@ -209,16 +209,16 @@ need to force the parsing level of ``y``, as follows.
    Notation "x < y" := (lt x y) (at level 70).
    Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level).
 
-For the sake of factorization with Coq predefined rules, simple rules
+For the sake of factorization with |Coq| predefined rules, simple rules
 have to be observed for notations starting with a symbol, e.g., rules
 starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list
-of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`.
+of |Coq| predefined notations can be found in the chapter on :ref:`thecoqlibrary`.
 
 Displaying symbolic notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The command :cmd:`Notation` has an effect both on the Coq parser and on the
-Coq printer. For example:
+The command :cmd:`Notation` has an effect both on the |Coq| parser and on the
+|Coq| printer. For example:
 
 .. coqtop:: all
 
@@ -226,7 +226,7 @@ Coq printer. For example:
 
 However, printing, especially pretty-printing, also requires some
 care. We may want specific indentations, line breaks, alignment if on
-several lines, etc. For pretty-printing, |Coq| relies on |ocaml|
+several lines, etc. For pretty-printing, |Coq| relies on |OCaml|
 formatting library, which provides indentation and automatic line
 breaks depending on page width by means of *formatting boxes*.
 
@@ -349,12 +349,12 @@ Reserving notations
 
 .. cmd:: Reserved Notation @string {? ( {+, @syntax_modifier } ) }
 
-   A given notation may be used in different contexts. Coq expects all
+   A given notation may be used in different contexts. |Coq| expects all
    uses of the notation to be defined at the same precedence and with the
    same associativity. To avoid giving the precedence and associativity
    every time, this command declares a parsing rule (:token:`string`) in advance
    without giving its interpretation. Here is an example from the initial
-   state of Coq.
+   state of |Coq|.
 
    .. coqtop:: in
 
@@ -762,7 +762,7 @@ recursive patterns. The basic example is:
    Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
 
 On the right-hand side, an extra construction of the form ``.. t ..`` can
-be used. Notice that ``..`` is part of the Coq syntax and it must not be
+be used. Notice that ``..`` is part of the |Coq| syntax and it must not be
 confused with the three-dots notation “``…``” used in this manual to denote
 a sequence of arbitrary size.
 
@@ -942,7 +942,7 @@ Custom entries
 Custom entries have levels, like the main grammar of terms and grammar
 of patterns have. The lower level is 0 and this is the level used by
 default to put rules delimited with tokens on both ends. The level is
-left to be inferred by Coq when using :n:`in custom @ident`. The
+left to be inferred by |Coq| when using :n:`in custom @ident`. The
 level is otherwise given explicitly by using the syntax
 :n:`in custom @ident at level @natural`, where :n:`@natural` refers to the level.
 
@@ -996,7 +996,7 @@ associated to the custom entry ``expr``. The level can be omitted, as in
 
    Notation "[ e ]" := e (e custom expr).
 
-in which case Coq infer it. If the sub-expression is at a border of
+in which case |Coq| infer it. If the sub-expression is at a border of
 the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is
 determined by the associativity. If the sub-expression is not at the
 border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is
@@ -1097,7 +1097,7 @@ Here are the syntax elements used by the various notation commands.
           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`).
+          the initial state of |Coq| (see directory :file:`$COQLIB/theories/Init`).
 
 .. note:: The notation ``"{ x }"`` has a special status in the main grammars of
           terms and patterns so that
@@ -1122,7 +1122,7 @@ Here are the syntax elements used by the various notation commands.
           .. warn:: Use of @string Notation is deprecated as it is inconsistent with pattern syntax.
 
              This warning is disabled by default to avoid spurious diagnostics
-             due to legacy notation in the Coq standard library.
+             due to legacy notation in the |Coq| standard library.
              It can be turned on with the ``-w disj-pattern-notation`` flag.
 
 .. _Scopes:
@@ -1156,7 +1156,7 @@ Most commands use :token:`scope_name`; :token:`scope_key`\s are used within :tok
 .. cmd:: Declare Scope @scope_name
 
    Declares a new notation scope. Note that the initial
-   state of Coq declares the following notation scopes:
+   state of |Coq| declares the following notation scopes:
    ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``,
    ``bool_scope``, ``list_scope``, ``int_scope``, ``uint_scope``.
 
@@ -1308,10 +1308,10 @@ recognized to be a ``Funclass`` instance, i.e., of type :g:`forall x:A, B` or
 
 .. _notation-scopes:
 
-Notation scopes used in the standard library of Coq
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Notation scopes used in the standard library of |Coq|
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-We give an overview of the scopes used in the standard library of Coq.
+We give an overview of the scopes used in the standard library of |Coq|.
 For a complete list of notations in each scope, use the commands :cmd:`Print
 Scopes` or :cmd:`Print Scope`.
 
@@ -1377,7 +1377,7 @@ Scopes` or :cmd:`Print Scope`.
 
 ``string_scope``
   This scope includes notation for strings as elements of the type string.
-  Special characters and escaping follow Coq conventions on strings (see
+  Special characters and escaping follow |Coq| conventions on strings (see
   :ref:`lexical-conventions`). Especially, there is no convention to visualize non
   printable characters of a string. The file :file:`String.v` shows an example
   that contains quotes, a newline and a beep (i.e. the ASCII character
@@ -1478,7 +1478,7 @@ Abbreviations
 
    An abbreviation expects no precedence nor associativity, since it
    is parsed as an usual application. Abbreviations are used as
-   much as possible by the Coq printers unless the modifier ``(only
+   much as possible by the |Coq| printers unless the modifier ``(only
    parsing)`` is given.
 
    An abbreviation is bound to an absolute name as an ordinary definition is
@@ -1634,7 +1634,7 @@ Number notations
             with :n:`(abstract after @bignat)`, this warning is emitted when
             parsing a number greater than or equal to :token:`bignat`.
             Typically, this indicates that the fully computed representation
-            of numbers can be so large that non-tail-recursive OCaml
+            of numbers can be so large that non-tail-recursive |OCaml|
             functions run out of stack space when trying to walk them.
 
          .. warn:: The 'abstract after' directive has no effect when the parsing function (@qualid__parse) targets an option type.
@@ -1978,9 +1978,9 @@ Tactic notations allow customizing the syntax of tactics.
 .. rubric:: Footnotes
 
 .. [#and_or_levels] which are the levels effectively chosen in the current
-   implementation of Coq
+   implementation of |Coq|
 
-.. [#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``
+.. [#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
diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst
index 0bd3054788..95218322ff 100644
--- a/doc/sphinx/using/libraries/index.rst
+++ b/doc/sphinx/using/libraries/index.rst
@@ -4,15 +4,15 @@
 Libraries and plugins
 =====================
 
-Coq is distributed with a standard library and a set of internal
+|Coq| is distributed with a standard library and a set of internal
 plugins (most of which provide tactics that have already been
 presented in :ref:`writing-proofs`).  This chapter presents this
 standard library and some of these internal plugins which provide
 features that are not tactics.
 
-In addition, Coq has a rich ecosystem of external libraries and
+In addition, |Coq| has a rich ecosystem of external libraries and
 plugins.  These libraries and plugins can be browsed online through
-the `Coq Package Index <https://coq.inria.fr/opam/www/>`_ and
+the `|Coq| Package Index <https://coq.inria.fr/opam/www/>`_ and
 installed with the `opam package manager
 <https://coq.inria.fr/opam-using.html>`_.
 
diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst
index 325ea2af60..724bcd0488 100644
--- a/doc/sphinx/using/libraries/writing.rst
+++ b/doc/sphinx/using/libraries/writing.rst
@@ -1,9 +1,9 @@
-Writing Coq libraries and plugins
-=================================
+Writing |Coq| libraries and plugins
+===================================
 
-This section presents the part of the Coq language that is useful only
-to library and plugin authors.  A tutorial for writing Coq plugins is
-available in the Coq repository in `doc/plugin_tutorial
+This section presents the part of the |Coq| language that is useful only
+to library and plugin authors.  A tutorial for writing |Coq| plugins is
+available in the |Coq| repository in `doc/plugin_tutorial
 <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_.
 
 Deprecating library objects or tactics
diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst
index 9ac3d2adda..88c1a575d9 100644
--- a/doc/sphinx/using/tools/coqdoc.rst
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -253,7 +253,7 @@ The latter cannot be used around some inner parts of a proof, but can
 be used around a whole proof.
 
 Lastly, it is possible to adopt a middle-ground approach when the
-desired output is HTML, where a given snippet of Coq material is
+desired output is HTML, where a given snippet of |Coq| material is
 hidden by default, but can be made visible with user interaction.
 
 ::
@@ -358,11 +358,11 @@ Command line options
 **Hyperlink options**
 
   :--glob-from file: Make references using |Coq| globalizations from file
-    file. (Such globalizations are obtained with Coq option ``-dump-glob``).
+    file. (Such globalizations are obtained with |Coq| option ``-dump-glob``).
   :--no-externals: Do not insert links to the |Coq| standard library.
   :--external url coqdir: Use given URL for linking references whose
     name starts with prefix ``coqdir``.
-  :--coqlib url: Set base URL for the Coq standard library (default is
+  :--coqlib url: Set base URL for the |Coq| standard library (default is
     `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url
     Coq``.
   :-R dir coqdir: Recursively map physical directory dir to |Coq| logical
diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst
index dfe38dfce9..8543c5de8a 100644
--- a/doc/sphinx/using/tools/index.rst
+++ b/doc/sphinx/using/tools/index.rst
@@ -5,11 +5,11 @@ Command-line and graphical tools
 ================================
 
 This chapter presents the command-line tools that users will need to
-build their Coq project, the documentation of the CoqIDE standalone
+build their |Coq| project, the documentation of the |CoqIDE| standalone
 user interface and the documentation of the parallel proof processing
-feature that is supported by CoqIDE and several other user interfaces.
-A list of available user interfaces to interact with Coq is available
-on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_.
+feature that is supported by |CoqIDE| and several other user interfaces.
+A list of available user interfaces to interact with |Coq| is available
+on the `|Coq| website <https://coq.inria.fr/user-interfaces.html>`_.
 
 .. toctree::
    :maxdepth: 1