[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.

4 files changed, 35 insertions, 35 deletions

diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst
index 95218322ff..0bd3054788 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 724bcd0488..917edf0774 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 88c1a575d9..7ab8f9d763 100644
--- a/doc/sphinx/using/tools/coqdoc.rst
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -2,14 +2,14 @@
 
 .. _coqdoc:
 
-Documenting |Coq| files with coqdoc
+Documenting Coq files with coqdoc
 -----------------------------------
 
-coqdoc is a documentation tool for the proof assistant |Coq|, similar to
+coqdoc is a documentation tool for the proof assistant Coq, similar to
 ``javadoc`` or ``ocamldoc``. The task of coqdoc is
 
 
-#. to produce a nice |Latex| and/or HTML document from |Coq| source files,
+#. to produce a nice |Latex| and/or HTML document from Coq source files,
    readable for a human and not only for the proof assistant;
 #. to help the user navigate his own (or third-party) sources.
 
@@ -18,9 +18,9 @@ coqdoc is a documentation tool for the proof assistant |Coq|, similar to
 Principles
 ~~~~~~~~~~
 
-Documentation is inserted into |Coq| files as *special comments*. Thus
+Documentation is inserted into Coq files as *special comments*. Thus
 your files will compile as usual, whether you use coqdoc or not. coqdoc
-presupposes that the given |Coq| files are well-formed (at least
+presupposes that the given Coq files are well-formed (at least
 lexically). Documentation starts with ``(**``, followed by a space, and
 ends with ``*)``. The documentation format is inspired by Todd
 A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with
@@ -29,10 +29,10 @@ shouldn’t fail, whatever the input is. But remember: “garbage in,
 garbage out”.
 
 
-|Coq| material inside documentation.
+Coq material inside documentation.
 ++++++++++++++++++++++++++++++++++++
 
-|Coq| material is quoted between the delimiters ``[`` and ``]``. Square brackets
+Coq material is quoted between the delimiters ``[`` and ``]``. Square brackets
 may be nested, the inner ones being understood as being part of the
 quoted code (thus you can quote a term like ``fun x => u`` by writing  ``[fun
 x => u]``). Inside quotations, the code is pretty-printed in the same
@@ -46,7 +46,7 @@ Pretty-printing.
 ++++++++++++++++
 
 coqdoc uses different faces for identifiers and keywords. The pretty-
-printing of |Coq| tokens (identifiers or symbols) can be controlled
+printing of Coq tokens (identifiers or symbols) can be controlled
 using one of the following commands:
 
 ::
@@ -63,7 +63,7 @@ or
     (** printing  *token* $...LATEX math...$ #...html...# *)
 
 
-It gives the |Latex| and HTML texts to be produced for the given |Coq|
+It gives the |Latex| and HTML texts to be produced for the given Coq
 token. Either the |Latex| or the HTML rule may be omitted, causing the
 default pretty-printing to be used for this token.
 
@@ -91,7 +91,7 @@ commands.
 
    The recognition of tokens is done by a (``ocaml``) lex
    automaton and thus applies the longest-match rule. For instance, `->~`
-   is recognized as a single token, where |Coq| sees two tokens. It is the
+   is recognized as a single token, where Coq sees two tokens. It is the
    responsibility of the user to insert space between tokens *or* to give
    pretty-printing rules for the possible combinations, e.g.
 
@@ -217,7 +217,7 @@ Then invoke coqdoc or ``coqdoc --glob-from file`` to tell coqdoc to look
 for name resolutions in the file ``file`` (it will look in ``file.glob``
 by default).
 
-Identifiers from the |Coq| standard library are linked to the Coq website
+Identifiers from the Coq standard library are linked to the Coq website
 `<http://coq.inria.fr/library/>`_. This behavior can be changed
 using command line options ``--no-externals`` and ``--coqlib``; see below.
 
@@ -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.
 
 ::
@@ -280,12 +280,12 @@ Usage
 coqdoc is invoked on a shell command line as follows:
 ``coqdoc <options and files>``.
 Any command line argument which is not an option is considered to be a
-file (even if it starts with a ``-``). |Coq| files are identified by the
+file (even if it starts with a ``-``). Coq files are identified by the
 suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``.
 
 
 :HTML output: This is the default output format. One HTML file is created for
-  each |Coq| file given on the command line, together with a file
+  each Coq file given on the command line, together with a file
   ``index.html`` (unless ``option-no-index is passed``). The HTML pages use a
   style sheet named ``style.css``. Such a file is distributed with coqdoc.
 :|Latex| output: A single |Latex| file is created, on standard
@@ -295,7 +295,7 @@ suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``.
   document . DVI and PostScript can be produced directly with the
   options ``-dvi`` and ``-ps`` respectively.
 :TEXmacs output: To translate the input files to TEXmacs format,
-  to be used by the TEXmacs |Coq| interface.
+  to be used by the TEXmacs Coq interface.
 
 
 
@@ -357,18 +357,18 @@ 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``).
-  :--no-externals: Do not insert links to the |Coq| standard library.
+  :--glob-from file: Make references using Coq globalizations from file
+    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
-    directory  ``coqdir`` (similarly to |Coq| option ``-R``).
-  :-Q dir coqdir: Map physical directory dir to |Coq| logical
-    directory  ``coqdir`` (similarly to |Coq| option ``-Q``).
+  :-R dir coqdir: Recursively map physical directory dir to Coq logical
+    directory  ``coqdir`` (similarly to Coq option ``-R``).
+  :-Q dir coqdir: Map physical directory dir to Coq logical
+    directory  ``coqdir`` (similarly to Coq option ``-Q``).
 
     .. note::
 
@@ -420,7 +420,7 @@ Command line options
   :--plain-comments: Do not interpret comments, simply copy them as
     plain-text.
   :--interpolate: Use the globalization information to typeset
-    identifiers appearing in |Coq| escapings inside comments.
+    identifiers appearing in Coq escapings inside comments.
 
 **Language options**
 
diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst
index 8543c5de8a..dfe38dfce9 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