[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.

The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.

3 files changed, 124 insertions, 124 deletions

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 59e1c65a49..d20a82e6c0 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -1,13 +1,13 @@
 .. _thecoqcommands:
 
-The |Coq| commands
+The Coq commands
 ====================
 
-There are three |Coq| commands:
+There are three Coq commands:
 
-+ ``coqtop``: the |Coq| toplevel (interactive mode);
-+ ``coqc``: the |Coq| compiler (batch compilation);
-+ ``coqchk``: the |Coq| checker (validation of compiled libraries).
++ ``coqtop``: the Coq toplevel (interactive mode);
++ ``coqc``: the Coq compiler (batch compilation);
++ ``coqchk``: the Coq checker (validation of compiled libraries).
 
 
 The options are (basically) the same for the first two commands, and
@@ -19,19 +19,19 @@ roughly described below. You can also look at the ``man`` pages of
 Interactive use (coqtop)
 ------------------------
 
-In the interactive mode, also known as the |Coq| toplevel, the user can
-develop his theories and proofs step by step. The |Coq| toplevel is run
+In the interactive mode, also known as the Coq toplevel, the user can
+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
+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
 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
-with the command ``Drop.``, and come back to the |Coq|
+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();;``.
 
 .. flag:: Coqtop Exit On Error
@@ -48,7 +48,7 @@ vernacular file named *file*.v, and tries to compile it into a
 
 .. caution::
 
-   The name *file* should be a regular |Coq| identifier as defined in Section :ref:`lexical-conventions`.
+   The name *file* should be a regular Coq identifier as defined in Section :ref:`lexical-conventions`.
    It should contain only letters, digits or underscores (_). For example ``/bar/foo/toto.v`` is valid,
    but ``/bar/foo/to-to.v`` is not.
 
@@ -59,9 +59,9 @@ Customization at launch time
 By resource file
 ~~~~~~~~~~~~~~~~~~~~~~~
 
-When |Coq| is launched, with either ``coqtop`` or ``coqc``, the
+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
@@ -73,7 +73,7 @@ You can also specify an arbitrary name for the resource file
 (see option ``-init-file`` below).
 
 The resource file may contain, for instance, ``Add LoadPath`` commands to add
-directories to the load path of |Coq|. It is possible to skip the
+directories to the load path of Coq. It is possible to skip the
 loading of the resource file with the option ``-q``.
 
 .. _customization-by-environment-variables:
@@ -82,10 +82,10 @@ By environment variables
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
 ``$COQPATH`` can be used to specify the load path. It is a list of directories separated by
-``:`` (``;`` on Windows). |Coq| will also honor ``$XDG_DATA_HOME`` and
+``:`` (``;`` on Windows). Coq will also honor ``$XDG_DATA_HOME`` and
 ``$XDG_DATA_DIRS`` (see Section :ref:`libraries-and-filesystem`).
 
-Some |Coq| commands call other |Coq| commands. In this case, they look for
+Some Coq commands call other Coq commands. In this case, they look for
 the commands in directory specified by ``$COQBIN``. If this variable is
 not set, they look for the commands in the executable path.
 
@@ -115,7 +115,7 @@ can be used to specify certain runtime and memory usage parameters.  In most cas
 experimenting with these settings will likely not cause a significant performance difference
 and should be harmless.
 
-If the variable is not set, |Coq| uses the
+If the variable is not set, Coq uses the
 `default values <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEcontrol>`_,
 except that ``space_overhead`` is set to 120 and ``minor_heap_size`` is set to 32Mwords
 (256MB with 64-bit executables or 128MB with 32-bit executables).
@@ -133,21 +133,21 @@ 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::
 
      :ref:`names-of-libraries` and the
      command Declare ML Module Section :ref:`compiled-files`.
 :-Q *directory* *dirpath*: Add physical path *directory* to the list of
-  directories where |Coq| looks for a file and bind it to the logical
+  directories where Coq looks for a file and bind it to the logical
   directory *dirpath*. The subdirectory structure of *directory* is
-  recursively available from |Coq| using absolute names (extending the
+  recursively available from Coq using absolute names (extending the
   :n:`@dirpath` prefix) (see Section :ref:`qualified-names`). Note that only those
   subdirectories and files which obey the lexical conventions of what is
   an :n:`@ident` are taken into account. Conversely, the
   underlying file systems or operating systems may be more restrictive
-  than |Coq|. While Linux’s ext4 file system supports any |Coq| recursive
+  than Coq. While Linux’s ext4 file system supports any Coq recursive
   layout (within the limit of 255 bytes per filename), the default on
   NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to
   disallow two files differing only in the case in the same directory.
@@ -155,7 +155,7 @@ and ``coqtop``, unless stated otherwise:
   .. seealso:: Section :ref:`names-of-libraries`.
 :-R *directory* *dirpath*: Do as ``-Q`` *directory* *dirpath* but make the
   subdirectory structure of *directory* recursively visible so that the
-  recursive contents of physical *directory* is available from |Coq| using
+  recursive contents of physical *directory* is available from Coq using
   short or partially qualified names.
 
   .. seealso:: Section :ref:`names-of-libraries`.
@@ -172,12 +172,12 @@ and ``coqtop``, unless stated otherwise:
   loading the default resource file from the standard configuration
   directories.
 :-q: Do not to load the default resource file.
-:-l *file*, -load-vernac-source *file*: Load and execute the |Coq|
+:-l *file*, -load-vernac-source *file*: Load and execute the Coq
   script from *file.v*.
 :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the
-  |Coq| script from *file.v*. Write its contents to the standard output as
+  Coq script from *file.v*. Write its contents to the standard output as
   it is executed.
-:-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This
+:-load-vernac-object *qualid*: Load Coq compiled library :n:`@qualid`. This
   is equivalent to running :cmd:`Require` :n:`@qualid`.
 
   .. _interleave-command-line:
@@ -191,27 +191,27 @@ and ``coqtop``, unless stated otherwise:
      :cmd:`Unset` commands will be executed in the order specified on
      the command-line.
 
-:-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`.
+:-rfrom *dirpath* *qualid*: Load Coq compiled library :n:`@qualid`.
   This is equivalent to running :cmd:`From <From … Require>`
   :n:`@dirpath` :cmd:`Require <From … Require>` :n:`@qualid`.
   See the :ref:`note above <interleave-command-line>` regarding the order
   of command-line options.
-:-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
+:-ri *qualid*, -require-import *qualid*: Load Coq compiled library :n:`@qualid` and import it.
   This is equivalent to running :cmd:`Require Import` :n:`@qualid`.
   See the :ref:`note above <interleave-command-line>` regarding the order
   of command-line options.
-:-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
+:-re *qualid*, -require-export *qualid*: Load Coq compiled library :n:`@qualid` and transitively import it.
   This is equivalent to running :cmd:`Require Export` :n:`@qualid`.
   See the :ref:`note above <interleave-command-line>` regarding the order
   of command-line options.
 :-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*:
-  Load |Coq| compiled library :n:`@qualid` and import it.  This is
+  Load Coq compiled library :n:`@qualid` and import it.  This is
   equivalent to running :cmd:`From <From … Require>` :n:`@dirpath`
   :cmd:`Require Import <From … Require>` :n:`@qualid`.  See the
   :ref:`note above <interleave-command-line>` regarding the order of
   command-line options.
 :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*:
-  Load |Coq| compiled library :n:`@qualid` and transitively import it.
+  Load Coq compiled library :n:`@qualid` and transitively import it.
   This is equivalent to running :cmd:`From <From … Require>`
   :n:`@dirpath` :cmd:`Require Export <From … Require>` :n:`@qualid`.
   See the :ref:`note above <interleave-command-line>` regarding the
@@ -219,11 +219,11 @@ and ``coqtop``, unless stated otherwise:
 :-batch: Exit just after argument parsing. Available for ``coqtop`` only.
 :-verbose: Output the content of the input file as it is compiled.
   This option is available for ``coqc`` only.
-:-vos: Indicate |Coq| to skip the processing of opaque proofs
+:-vos: Indicate Coq to skip the processing of opaque proofs
   (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files
   instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files
   when interpreting :cmd:`Require` commands.
-:-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead
+:-vok: Indicate Coq to check a file completely, to load ``.vos`` files instead
   of ``.vo`` files when interpreting :cmd:`Require` commands, and to output an empty
   ``.vok`` files upon success instead of writing a ``.vo`` file.
 :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This
@@ -241,7 +241,7 @@ and ``coqtop``, unless stated otherwise:
   syntax/definitions/notations.
 :-emacs, -ide-slave: Start a special toplevel to communicate with a
   specific IDE.
-:-impredicative-set: Change the logical theory of |Coq| by declaring the
+:-impredicative-set: Change the logical theory of Coq by declaring the
    sort :g:`Set` impredicative.
 
    .. warning::
@@ -249,12 +249,12 @@ and ``coqtop``, unless stated otherwise:
       This is known to be inconsistent with some
       standard axioms of classical mathematics such as the functional
       axiom of choice or the principle of description.
-:-type-in-type: Collapse the universe hierarchy of |Coq|.
+:-type-in-type: Collapse the universe hierarchy of Coq.
 
   .. 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.
@@ -285,16 +285,16 @@ and ``coqtop``, unless stated otherwise:
 :-no-glob: Disable the dumping of references for global names.
 :-image *file*: Set the binary image to be used by ``coqc`` to be *file*
   instead of the standard one. Not of general use.
-:-bindir *directory*: Set the directory containing |Coq| binaries to be
+:-bindir *directory*: Set the directory containing Coq binaries to be
   used by ``coqc``. It is equivalent to doing export COQBIN= *directory*
   before launching ``coqc``.
-:-where: Print the location of |Coq|’s standard library and exit.
-:-config: Print the locations of |Coq|’s binaries, dependencies, and
+:-where: Print the location of Coq’s standard library and exit.
+:-config: Print the locations of Coq’s binaries, dependencies, and
   libraries, then exit.
 :-filteropts: Print the list of command line arguments that `coqtop` has
   recognized as options and exit.
-:-v: Print |Coq|’s version and exit.
-:-list-tags: Print the highlight tags known by |Coq| as well as their
+:-v: Print Coq’s version and exit.
+:-list-tags: Print the highlight tags known by Coq as well as their
   currently associated color and exit.
 :-h, --help: Print a short usage and exit.
 
@@ -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.
 
@@ -401,7 +401,7 @@ within a section.
 
 .. warn:: You should use the “Proof using [...].” syntax instead of “Proof.” to enable skipping this proof which is located inside a section. Give as argument to “Proof using” the list of section variables that are not needed to typecheck the statement but that are required by the proof.
 
-     If |Coq| is invoked using the ``-vos`` option, whenever it finds the
+     If Coq is invoked using the ``-vos`` option, whenever it finds the
      command ``Proof.`` inside a section, it will compile the proof, that is,
      refuse to skip it, and it will raise a warning. To disable the warning, one
      may pass the flag ``-w -proof-without-using-in-section``.
@@ -412,7 +412,7 @@ When compiling a file ``foo.v`` using ``coqc`` in the standard way (i.e., withou
 ``-vos`` nor ``-vok``), an empty file ``foo.vos`` and an empty file ``foo.vok``
 are created in addition to the regular output file ``foo.vo``.
 If ``coqc`` is subsequently invoked on some other file ``bar.v`` using option
-``-vos`` or ``-vok``, and that ``bar.v`` requires ``foo.v``, if |Coq| finds an
+``-vos`` or ``-vok``, and that ``bar.v`` requires ``foo.v``, if Coq finds an
 empty file ``foo.vos``, then it will load ``foo.vo`` instead of ``foo.vos``.
 
 The purpose of this feature is to allow users to benefit from the ``-vos``
@@ -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 64b433115c..c239797cc2 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -2,28 +2,28 @@
 
 .. _coqintegrateddevelopmentenvironment:
 
-|Coq| Integrated Development Environment
+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.
+CoqIDE is run by typing the command `coqide` on the command line.
 Without argument, the main screen is displayed with an “unnamed
 buffer”, and with a filename as argument, another buffer displaying
 the contents of that file. Additionally, `coqide` accepts the same
 options as `coqtop`, given in :ref:`thecoqcommands`, the ones having obviously
-no meaning for |CoqIDE| being ignored.
+no meaning for CoqIDE being ignored.
 
 .. _coqide_mainscreen:
 
   .. image:: ../_static/coqide.png
-     :alt: |CoqIDE| main screen
+     :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>`.
+A sample CoqIDE main screen, while navigating into a file `Fermat.v`,
+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,15 +39,15 @@ 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.
-|CoqIDE| offers only basic editing commands, so if you need more complex
+CoqIDE offers only basic editing commands, so if you need more complex
 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
@@ -74,7 +74,7 @@ and use the goto button. Unlike with `coqtop`, you should never use
 There are two additional buttons for navigation within the running buffer. The
 "down" button with a line goes directly to the end; the "up" button with a line
 goes back to the beginning. The handling of errors when using the go-to-the-end
-button depends on whether |Coq| is running in asynchronous mode or not (see
+button depends on whether Coq is running in asynchronous mode or not (see
 Chapter :ref:`asynchronousandparallelproofprocessing`). If it is not running in that mode, execution
 stops as soon as an error is found. Otherwise, execution continues, and the
 error is marked with an underline in the error foreground color, with a
@@ -86,12 +86,12 @@ If you ever try to execute a command that runs for a long time
 and would like to abort it before it terminates, you may
 use the interrupt button (the white cross on a red circle).
 
-There are other buttons on the |CoqIDE| toolbar: a button to save the running
+There are other buttons on the CoqIDE toolbar: a button to save the running
 buffer; a button to close the current buffer (an "X"); buttons to switch among
 buffers (left and right arrows); an "information" button; and a "gears" button.
 
-The "gears" button submits proof terms to the |Coq| kernel for type checking.
-When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`),
+The "gears" button submits proof terms to the Coq kernel for type checking.
+When Coq uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`),
 proofs may have been completed without kernel-checking of generated proof terms.
 The presence of unchecked proof terms is indicated by ``Qed`` statements that
 have a subdued *being-processed* color (light blue by default), rather than the
@@ -114,11 +114,11 @@ Queries
 ------------
 
 .. image:: ../_static/coqide-queries.png
-   :alt: |CoqIDE| queries
+   :alt: CoqIDE queries
 
 We call *query* any vernacular command that does not change the current state,
 such as ``Check``, ``Search``, etc. To run such commands interactively, without
-writing them in scripts, |CoqIDE| offers a *query pane*. The query pane can be
+writing them in scripts, CoqIDE offers a *query pane*. The query pane can be
 displayed on demand by using the ``View`` menu, or using the shortcut ``F1``.
 Queries can also be performed by selecting a particular phrase, then choosing an
 item from the ``Queries`` menu. The response then appears in the message window.
@@ -148,12 +148,12 @@ The first section is for selecting the text font used for scripts,
 goal and message windows.
 
 The second and third sections are for controlling colors and style of
-the three main buffers. A predefined |Coq| highlighting style as well
+the three main buffers. A predefined Coq highlighting style as well
 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
@@ -169,7 +169,7 @@ The next section is devoted to file management: you may configure
 automatic saving of files, by periodically saving the contents into
 files named `#f#` for each opened file `f`. You may also activate the
 *revert* feature: in case a opened file is modified on the disk by a
-third party, |CoqIDE| may read it again for you. Note that in the case
+third party, CoqIDE may read it again for you. Note that in the case
 you edited that same file, you will be prompted to choose to either
 discard your changes or not. The File charset encoding choice is
 described below in :ref:`character-encoding-saved-files`.
@@ -196,9 +196,9 @@ still edit this configuration file by hand, but this is more involved.
 Using Unicode symbols
 --------------------------
 
-|CoqIDE| is based on GTK+ and inherits from it support for Unicode in
+CoqIDE is based on GTK+ and inherits from it support for Unicode in
 its text windows. Consequently a large set of symbols is available for
-notations. Furthermore, |CoqIDE| conveniently provides a simple way to
+notations. Furthermore, CoqIDE conveniently provides a simple way to
 input Unicode characters.
 
 
@@ -219,9 +219,9 @@ 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
-``Require Import Unicode.Utf8`` inside |CoqIDE|, or equivalently,
-by starting |CoqIDE| with ``coqide -l utf8``.
+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``.
 
 However, there are some issues when using such Unicode symbols: you of
 course need to use a character font which supports them. In the Fonts
@@ -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``
@@ -255,7 +255,7 @@ Custom bindings may be added, as explained further on.
 .. note::
 
     It remains possible to input non-ASCII symbols using system-wide
-    approaches independent of |CoqIDE|.
+    approaches independent of CoqIDE.
 
 
 Adding custom bindings
@@ -286,7 +286,7 @@ Similarly, the above settings ensure than ``\l`` resolves to ``\le``,
 and that ``\la`` resolves to ``\lambda``.
 
 It can be useful to work with per-project binding files. For this purpose
-|CoqIDE| accepts a command line argument of the form
+CoqIDE accepts a command line argument of the form
 ``-unicode-bindings file1,file2,...,fileN``.
 Each of the file tokens provided may consists of one of:
 
@@ -320,7 +320,7 @@ related to the way files are saved.
 If you have no need to exchange files with non UTF-8 aware
 applications, it is better to choose the UTF-8 encoding, since it
 guarantees that your files will be read again without problems. (This
-is because when |CoqIDE| reads a file, it tries to automatically detect
+is because when CoqIDE reads a file, it tries to automatically detect
 its character encoding.)
 
 If you choose something else than UTF-8, then missing characters will
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index c3286199e8..ec3689bbbe 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -8,7 +8,7 @@ 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
@@ -34,21 +34,21 @@ For example, to statically link |Ltac|, you can just do:
 
 and similarly for other plugins.
 
-Building a |Coq| project
+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:
 
-Building a |Coq| project with coq_makefile
+Building a Coq project with coq_makefile
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The majority of |Coq| projects are very similar: a collection of ``.v``
-files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of
+The majority of Coq projects are very similar: a collection of ``.v``
+files and eventually some ``.ml`` ones (a Coq plugin). The main piece of
 metadata needed in order to build the project are the command line
 options to ``coqc`` (e.g. ``-R``, ``Q``, ``-I``, see :ref:`command
 line options <command-line-options>`). Collecting the list of files
@@ -74,11 +74,11 @@ to literally pass an argument ``foo`` to ``coqc``: in the
 example, this allows to pass the two-word option ``-w all`` (see
 :ref:`command line options <command-line-options>`).
 
-|CoqIDE|, Proof-General and VSCoq all
-understand ``_CoqProject`` files and can be used to invoke |Coq| with the desired options.
+CoqIDE, Proof-General and VSCoq all
+understand ``_CoqProject`` files and can be used to invoke Coq with the desired options.
 
 The ``coq_makefile`` utility can be used to set up a build infrastructure
-for the |Coq| project based on makefiles. The recommended way of
+for the Coq project based on makefiles. The recommended way of
 invoking ``coq_makefile`` is the following one:
 
 ::
@@ -91,14 +91,14 @@ Such command generates the following files:
 CoqMakefile
   is a makefile for ``GNU Make`` with targets to build the project
   (e.g. generate .vo or .html files from .v or compile .ml* files)
-  and install it in the ``user-contrib`` directory where the |Coq|
+  and install it in the ``user-contrib`` directory where the Coq
   library is installed. Run ``make`` with the ``-f CoqMakefile``
   option to use ``CoqMakefile``.
 
 CoqMakefile.conf
   contains make variables assignments that reflect
   the contents of the ``_CoqProject`` file as well as the path relevant to
-  |Coq|.
+  Coq.
 
 
 An optional file ``CoqMakefile.local`` can be provided by the user in order to
@@ -111,11 +111,11 @@ The extensions of the files listed in ``_CoqProject`` is used in order to
 decide how to build them. In particular:
 
 
-+ |Coq| files must use the ``.v`` extension
-+ |OCaml| files must use the ``.ml`` or ``.mli`` extension
-+ |OCaml| files that require pre processing for syntax
++ Coq files must use the ``.v`` extension
++ OCaml files must use the ``.ml`` or ``.mli`` extension
++ OCaml files that require pre processing for syntax
   extensions (like ``VERNAC EXTEND``) must use the ``.mlg`` extension
-+ In order to generate a plugin one has to list all |OCaml|
++ In order to generate a plugin one has to list all OCaml
   modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib``
   file).
 
@@ -142,23 +142,23 @@ 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|
+   can be used to specify additional flags to the OCaml
    compiler, like ``-bin-annot`` or ``-w``....
 :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``.
 
@@ -524,7 +524,7 @@ Precompiling for ``native_compute``
 +++++++++++++++++++++++++++++++++++
 
 To compile files for ``native_compute``, one can use the
-``-native-compiler yes`` option of |Coq|, for instance by putting the
+``-native-compiler yes`` option of Coq, for instance by putting the
 following in a :ref:`coqmakefilelocal` file:
 
 ::
@@ -555,27 +555,27 @@ of installing the extra ``.coq-native`` directories.
    This requires all dependencies to be themselves compiled with
    ``-native-compiler yes``.
 
-Building a |Coq| project with Dune
+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
 
@@ -642,37 +642,37 @@ Computing Module dependencies
 -----------------------------
 
 In order to compute module dependencies (to be used by ``make`` or
-``dune``), |Coq| provides the ``coqdep`` tool.
+``dune``), Coq provides the ``coqdep`` tool.
 
-``coqdep`` computes inter-module dependencies for |Coq|
+``coqdep`` computes inter-module dependencies for Coq
 programs, and prints the dependencies on the standard output in a
 format readable by make. When a directory is given as argument, it is
 recursively looked at.
 
-Dependencies of |Coq| modules are computed by looking at ``Require``
+Dependencies of Coq modules are computed by looking at ``Require``
 commands (``Require``, ``Require Export``, ``Require Import``), but also at the
 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
+to insert Coq phrases inside a |Latex| document, possibly together
 with the corresponding answers of the system. We provide a mechanical
-way to process such |Coq| phrases embedded in |Latex| files: the ``coq-tex``
-filter. This filter extracts |Coq| phrases embedded in |Latex| files,
+way to process such Coq phrases embedded in |Latex| files: the ``coq-tex``
+filter. This filter extracts Coq phrases embedded in |Latex| files,
 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.
+Starting with a file ``file.tex`` containing Coq phrases, the ``coq-tex``
+filter produces a file named ``file.v.tex`` with the Coq outcome.
 
-There are options to produce the |Coq| parts in smaller font, italic,
+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
 details.