Add some missing smallcaps.

4 files changed, 15 insertions, 15 deletions

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