Add some missing smallcaps.

3 files changed, 43 insertions, 43 deletions

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