Add some missing smallcaps.

1 files changed, 188 insertions, 188 deletions

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)