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

6 files changed, 42 insertions, 42 deletions

diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index cc8af976d2..e6dc6f6c51 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -496,14 +496,14 @@ automatically created.
         ``typeclass_instances`` hint database.
 
 
-Hint databases defined in the |Coq| standard library
+Hint databases defined in the Coq standard library
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Several hint databases are defined in the |Coq| standard library. The
+Several hint databases are defined in the Coq standard library. The
 actual content of a database is the collection of hints declared
 to belong to this database in each of the various modules currently
 loaded. Especially, requiring new modules may extend the database.
-At |Coq| startup, only the core database is nonempty and can be used.
+At Coq startup, only the core database is nonempty and can be used.
 
 :core: This special database is automatically used by ``auto``, except when
        pseudo-database ``nocore`` is given to ``auto``. The core database
@@ -624,7 +624,7 @@ but this is a mere workaround and has some limitations (for instance, external
 hints cannot be removed).
 
 A proper way to fix this issue is to bind the hints to their module scope, as
-for most of the other objects |Coq| uses. Hints should only be made available when
+for most of the other objects Coq uses. Hints should only be made available when
 the module they are defined in is imported, not just required. It is very
 difficult to change the historical behavior, as it would break a lot of scripts.
 We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior`
diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst
index acf64ae437..c4faa7284f 100644
--- a/doc/sphinx/proofs/automatic-tactics/logic.rst
+++ b/doc/sphinx/proofs/automatic-tactics/logic.rst
@@ -208,7 +208,7 @@ some incompatibilities.
 .. exn:: I don’t know how to handle dependent equality.
 
   The decision procedure managed to find a proof of the goal or of a
-  discriminable equality but this proof could not be built in |Coq| because of
+  discriminable equality but this proof could not be built in Coq because of
   dependently-typed functions.
 
 .. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms.
diff --git a/doc/sphinx/proofs/creating-tactics/index.rst b/doc/sphinx/proofs/creating-tactics/index.rst
index f1d4fa789d..1af1b0b726 100644
--- a/doc/sphinx/proofs/creating-tactics/index.rst
+++ b/doc/sphinx/proofs/creating-tactics/index.rst
@@ -18,13 +18,13 @@ new tactics:
 
 - `Mtac2 <https://github.com/Mtac2/Mtac2>`_ is an external plugin
   which provides another typed tactic language.  While Ltac2 belongs
-  to the ML language family, Mtac2 reuses the language of |Coq| itself
-  as the language to build |Coq| tactics.
+  to the ML language family, Mtac2 reuses the language of Coq itself
+  as the language to build Coq tactics.
 
 - The most traditional way of building new complex tactics is to write
-  a |Coq| plugin in |OCaml|.  Beware that this also requires much more
-  effort and commitment.  A tutorial for writing |Coq| plugins is
-  available in the |Coq| repository in `doc/plugin_tutorial
+  a Coq plugin in OCaml.  Beware that this also requires much more
+  effort and commitment.  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>`_.
 
 .. toctree::
diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst
index 1c7fd050f1..7724d7433c 100644
--- a/doc/sphinx/proofs/writing-proofs/index.rst
+++ b/doc/sphinx/proofs/writing-proofs/index.rst
@@ -4,7 +4,7 @@
 Basic proof writing
 ===================
 
-|Coq| is an interactive theorem prover, or proof assistant, which means
+Coq is an interactive theorem prover, or proof assistant, which means
 that proofs can be constructed interactively through a dialog between
 the user and the assistant.  The building blocks for this dialog are
 tactics which the user will use to represent steps in the proof of a
diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
index b74c9d3a23..fd8a0329d6 100644
--- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst
+++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
@@ -4,14 +4,14 @@
  Proof handling
 -------------------
 
-In |Coq|’s proof editing mode all top-level commands documented in
+In Coq’s proof editing mode all top-level commands documented in
 Chapter :ref:`vernacularcommands` remain available and the user has access to specialized
 commands dealing with proof development pragmas documented in this
 section. They can also use some other specialized commands called
 *tactics*. They are the very tools allowing the user to deal with
 logical reasoning. They are documented in Chapter :ref:`tactics`.
 
-|Coq| user interfaces usually have a way of marking whether the user has
+Coq user interfaces usually have a way of marking whether the user has
 switched to proof editing mode. For instance, in coqtop the prompt ``Coq <``   is changed into
 :n:`@ident <`   where :token:`ident` is the declared name of the theorem currently edited.
 
@@ -30,13 +30,13 @@ When a proof is completed, the message ``Proof completed`` is displayed.
 One can then register this proof as a defined constant in the
 environment. Because there exists a correspondence between proofs and
 terms of λ-calculus, known as the *Curry-Howard isomorphism*
-:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those
+:cite:`How80,Bar81,Gir89,H89`, Coq stores proofs as terms of |Cic|. Those
 terms are called *proof terms*.
 
 
 .. exn:: No focused proof.
 
-   |Coq| raises this error message when one attempts to use a proof editing command
+   Coq raises this error message when one attempts to use a proof editing command
    out of the proof editing mode.
 
 .. _proof-editing-mode:
@@ -62,7 +62,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
 
    This command is available in interactive editing proof mode when the
    proof is completed. Then :cmd:`Qed` extracts a proof term from the proof
-   script, switches back to |Coq| top-level and attaches the extracted
+   script, switches back to Coq top-level and attaches the extracted
    proof term to the declared name of the original goal. The name is
    added to the environment as an opaque constant.
 
@@ -104,7 +104,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
 .. cmd:: Abort {? {| All | @ident } }
 
    Cancels the current proof development, switching back to
-   the previous proof development, or to the |Coq| toplevel if no other
+   the previous proof development, or to the Coq toplevel if no other
    proof was being edited.
 
    :n:`@ident`
@@ -298,8 +298,8 @@ Proof modes
 ```````````
 
 When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`,
-|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes
-shipped in the standard |Coq| installation, and furthermore some plugins define
+Coq picks by default the |Ltac| mode. Nonetheless, there exist other proof modes
+shipped in the standard Coq installation, and furthermore some plugins define
 their own proof modes. The default proof mode used when opening a proof can
 be changed using the following option.
 
@@ -498,7 +498,7 @@ or focus the next one.
 
 .. note::
 
-   In Proof General (``Emacs`` interface to |Coq|), you must use
+   In Proof General (``Emacs`` interface to Coq), you must use
    bullets with the priority ordering shown above to have a correct
    indentation. For example ``-`` must be the outer bullet and ``**`` the inner
    one in the example below.
@@ -798,10 +798,10 @@ Requesting information
 Showing differences between proof steps
 ---------------------------------------
 
-|Coq| can automatically highlight the differences between successive proof steps
-and between values in some error messages.  |Coq| can also highlight differences
+Coq can automatically highlight the differences between successive proof steps
+and between values in some error messages.  Coq can also highlight differences
 in the proof term.
-For example, the following screenshots of |CoqIDE| and coqtop show the application
+For example, the following screenshots of CoqIDE and coqtop show the application
 of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
 The conclusion is entirely in pale green because although it’s changed, no tokens were added
 to it.  The second screenshot uses the "removed" option, so it shows the conclusion a
@@ -825,24 +825,24 @@ new, no line of old text is shown for them.
 ..
 
   .. image:: ../../_static/diffs-coqide-on.png
-     :alt: |CoqIDE| with Set Diffs on
+     :alt: CoqIDE with Set Diffs on
 
 ..
 
   .. image:: ../../_static/diffs-coqide-removed.png
-     :alt: |CoqIDE| with Set Diffs removed
+     :alt: CoqIDE with Set Diffs removed
 
 ..
 
   .. image:: ../../_static/diffs-coqtop-on3.png
      :alt: coqtop with Set Diffs on
 
-This image shows an error message with diff highlighting in |CoqIDE|:
+This image shows an error message with diff highlighting in CoqIDE:
 
 ..
 
   .. image:: ../../_static/diffs-error-message.png
-     :alt: |CoqIDE| error message with diffs
+     :alt: CoqIDE error message with diffs
 
 How to enable diffs
 ```````````````````
@@ -858,21 +858,21 @@ How to enable diffs
 
 For coqtop, showing diffs can be enabled when starting coqtop with the
 ``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option
-within |Coq|.  You will need to provide the ``-color on|auto`` command-line option when
+within Coq.  You will need to provide the ``-color on|auto`` command-line option when
 you start coqtop in either case.
 
 Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment
 variable.  See section :ref:`customization-by-environment-variables`.  Diffs
 use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``.
 
-In |CoqIDE|, diffs should be enabled from the ``View`` menu.  Don’t use the ``Set Diffs``
-command in |CoqIDE|.  You can change the background colors shown for diffs from the
+In CoqIDE, diffs should be enabled from the ``View`` menu.  Don’t use the ``Set Diffs``
+command in CoqIDE.  You can change the background colors shown for diffs from the
 ``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``,
 ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags.  This panel also
 lets you control other attributes of the highlights, such as the foreground
 color, bold, italic, underline and strikeout.
 
-Proof General can also display |Coq|-generated proof diffs automatically.
+Proof General can also display Coq-generated proof diffs automatically.
 Please see the PG documentation section
 "`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_)
 for details.
@@ -963,7 +963,7 @@ To show differences in the proof term:
 
 - In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command.
 
-- In |CoqIDE|, position the cursor on or just after a tactic to compare the proof term
+- In CoqIDE, position the cursor on or just after a tactic to compare the proof term
   after the tactic with the proof term before the tactic, then select
   `View / Show Proof` from the menu or enter the associated key binding.
   Differences will be shown applying the current `Show Diffs` setting
@@ -995,10 +995,10 @@ Controlling the effect of proof editing commands
 
    When turned on (it is off by default), this flag enables support for nested
    proofs: a new assertion command can be inserted before the current proof is
-   finished, in which case |Coq| will temporarily switch to the proof of this
+   finished, in which case Coq will temporarily switch to the proof of this
    *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed`
    or :cmd:`Defined`), its statement will be made available (as if it had been
-   proved before starting the previous proof) and |Coq| will switch back to the
+   proved before starting the previous proof) and Coq will switch back to the
    proof of the previous assertion.
 
 .. flag:: Printing Goal Names
@@ -1015,12 +1015,12 @@ Controlling memory usage
    Prints heap usage statistics, which are values from the `stat` type of the `Gc` module
    described
    `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_
-   in the |OCaml| documentation.
+   in the OCaml documentation.
    The `live_words`, `heap_words` and `top_heap_words` values give the basic information.
    Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables.
 
 When experiencing high memory usage the following commands can be used
-to force |Coq| to optimize some of its internal data structures.
+to force Coq to optimize some of its internal data structures.
 
 .. cmd:: Optimize Proof
 
@@ -1030,7 +1030,7 @@ to force |Coq| to optimize some of its internal data structures.
 .. cmd:: Optimize Heap
 
    Perform a heap compaction.  This is generally an expensive operation.
-   See: `|OCaml| Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
+   See: `OCaml Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
    There is also an analogous tactic :tacn:`optimize_heap`.
 
 Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>`
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 1358aad432..f3f69a2fdc 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -362,7 +362,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    These parameterized reduction tactics apply to any goal and perform
    the normalization of the goal according to the specified flags. In
-   correspondence with the kinds of reduction considered in |Coq| namely
+   correspondence with the kinds of reduction considered in Coq namely
    :math:`\beta` (reduction of functional application), :math:`\delta`
    (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`),
    :math:`\iota` (reduction of
@@ -444,8 +444,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
 .. tacv:: native_compute
    :name: native_compute
 
-   This tactic evaluates the goal by compilation to |OCaml| as described
-   in :cite:`FullReduction`. If |Coq| is running in native code, it can be
+   This tactic evaluates the goal by compilation to OCaml as described
+   in :cite:`FullReduction`. If Coq is running in native code, it can be
    typically two to five times faster than :tacn:`vm_compute`. Note however that the
    compilation cost is higher, so it is worth using only for intensive
    computations.
@@ -783,7 +783,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
       If we try to prove :g:`id (fact n) = fact n` by
       :tacn:`reflexivity`, it will now take time proportional to
-      :math:`n!`, because |Coq| will keep unfolding :g:`fact` and
+      :math:`n!`, because Coq will keep unfolding :g:`fact` and
       :g:`*` and :g:`+` before it unfolds :g:`id`, resulting in a full
       computation of :g:`fact n` (in unary, because we are using
       :g:`nat`), which takes time :math:`n!`.  We can see this cross
@@ -827,7 +827,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
          Time Defined.
 
       On small examples this sort of behavior doesn't matter, but
-      because |Coq| is a super-linear performance domain in so many
+      because Coq is a super-linear performance domain in so many
       places, unless great care is taken, tactic automation using
       :tacn:`with_strategy` may not be robustly performant when
       scaling the size of the input.