[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gall…

…ina.

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

doc/changelog/09-coqide/00000-title.rst

@@ -1,3 +1,3 @@
 
-**|CoqIDE|**
+**CoqIDE**
 

doc/sphinx/README.rst

@@ -551,7 +551,7 @@ Add either ``abort`` to the first block or ``reset`` to the second block to avoi
 Abbreviations and macros
 ------------------------
 
-Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_.  This file is automatically included in all manual pages.
+Substitutions for specially-formatted names (like ``|Cic|``, ``|Ltac|`` and ``|Latex|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_.  This file is automatically included in all manual pages.
 
 Emacs
 -----

doc/sphinx/README.template.rst

@@ -290,7 +290,7 @@ Add either ``abort`` to the first block or ``reset`` to the second block to avoi
 Abbreviations and macros
 ------------------------
 
-Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_.  This file is automatically included in all manual pages.
+Substitutions for specially-formatted names (like ``|Cic|``, ``|Ltac|`` and ``|Latex|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_.  This file is automatically included in all manual pages.
 
 Emacs
 -----

doc/sphinx/addendum/generalized-rewriting.rst

@@ -35,7 +35,7 @@ the previous implementation in several ways:
   the new implementation, if one provides the proper morphisms. Again,
   most of the work is handled in the tactics.
 + First-class morphisms and signatures. Signatures and morphisms are
-  ordinary |Coq| terms, hence they can be manipulated inside |Coq|, put
+  ordinary Coq terms, hence they can be manipulated inside Coq, put
   inside structures and lemmas about them can be proved inside the
   system. Higher-order morphisms are also allowed.
 + Performance. The implementation is based on a depth-first search for
@@ -103,7 +103,7 @@ argument.
 Morphisms can also be contravariant in one or more of their arguments.
 A morphism is contravariant on an argument associated to the relation
 instance :math:`R` if it is covariant on the same argument when the inverse
-relation :math:`R^{−1}` (``inverse R`` in |Coq|) is considered. The special arrow ``-->``
+relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->``
 is used in signatures for contravariant morphisms.
 
 Functions having arguments related by symmetric relations instances
@@ -144,7 +144,7 @@ always the intended equality for a given structure.
 
 In the next section we will describe the commands to register terms as
 parametric relations and morphisms. Several tactics that deal with
-equality in |Coq| can also work with the registered relations. The exact
+equality in Coq can also work with the registered relations. The exact
 list of tactics will be given :ref:`in this section <tactics-enabled-on-user-provided-relations>`.
 For instance, the tactic reflexivity can be used to solve a goal ``R n n`` whenever ``R``
 is an instance of a registered reflexive relation. However, the

doc/sphinx/addendum/implicit-coercions.rst

@@ -8,7 +8,7 @@ Implicit Coercions
 General Presentation
 ---------------------
 
-This section describes the inheritance mechanism of |Coq|. In |Coq| with
+This section describes the inheritance mechanism of Coq. In Coq with
 inheritance, we are not interested in adding any expressive power to
 our theory, but only convenience. Given a term, possibly not typable,
 we are interested in the problem of determining if it can be well

doc/sphinx/addendum/micromega.rst

@@ -260,7 +260,7 @@ proof by abstracting monomials by variables.
    that might miss a refutation.
 
    To illustrate the working of the tactic, consider we wish to prove the
-   following |Coq| goal:
+   following Coq goal:
 
 .. needs csdp
 .. coqdoc::

doc/sphinx/addendum/miscellaneous-extensions.rst

@@ -1,7 +1,7 @@
 Program derivation
 ==================
 
-|Coq| comes with an extension called ``Derive``, which supports program
+Coq comes with an extension called ``Derive``, which supports program
 derivation. Typically in the style of Bird and Meertens or derivations
 of program refinements. To use the Derive extension it must first be
 required with ``Require Coq.derive.Derive``. When the extension is loaded,

doc/sphinx/addendum/omega.rst

@@ -9,7 +9,7 @@ Omega: a (deprecated) solver for arithmetic
 
    The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia`
    tactic.  The goal is to consolidate the arithmetic solving
-   capabilities of |Coq| into a single engine; moreover, :tacn:`lia` is
+   capabilities of Coq into a single engine; moreover, :tacn:`lia` is
    in general more powerful than :tacn:`omega` (it is a complete
    Presburger arithmetic solver while :tacn:`omega` was known to be
    incomplete).
@@ -143,7 +143,7 @@ Options
 
    .. deprecated:: 8.5
 
-   This deprecated flag (on by default) is for compatibility with |Coq| pre 8.5. It
+   This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It
    resets internal name counters to make executions of :tacn:`omega` independent.
 
 .. flag:: Omega UseLocalDefs

doc/sphinx/addendum/parallel-proof-processing.rst

@@ -6,8 +6,8 @@ Asynchronous and Parallel Proof Processing
 :Author: Enrico Tassi
 
 This chapter explains how proofs can be asynchronously processed by
-|Coq|. This feature improves the reactivity of the system when used in
-interactive mode via |CoqIDE|. In addition, it allows |Coq| to take
+Coq. This feature improves the reactivity of the system when used in
+interactive mode via CoqIDE. In addition, it allows Coq to take
 advantage of parallel hardware when used as a batch compiler by
 decoupling the checking of statements and definitions from the
 construction and checking of proofs objects.
@@ -20,26 +20,26 @@ This feature has some technical limitations that may make it
 unsuitable for some use cases.
 
 For example, in interactive mode, some errors coming from the kernel
-of |Coq| are signaled late. The type of errors belonging to this
+of Coq are signaled late. The type of errors belonging to this
 category are universe inconsistencies.
 
 At the time of writing, only opaque proofs (ending with ``Qed`` or
 ``Admitted``) can be processed asynchronously.
 
-Finally, asynchronous processing is disabled when running |CoqIDE| in
+Finally, asynchronous processing is disabled when running CoqIDE in
 Windows. The current implementation of the feature is not stable on
 Windows. It can be enabled, as described below at :ref:`interactive-mode`,
 though doing so is not recommended.
 
 Proof annotations
 ----------------------
 
-To process a proof asynchronously |Coq| needs to know the precise
+To process a proof asynchronously Coq needs to know the precise
 statement of the theorem without looking at the proof. This requires
 some annotations if the theorem is proved inside a Section (see
 Section :ref:`section-mechanism`).
 
-When a section ends, |Coq| looks at the proof object to decide which
+When a section ends, Coq looks at the proof object to decide which
 section variables are actually used and hence have to be quantified in
 the statement of the theorem. To avoid making the construction of
 proofs mandatory when ending a section, one can start each proof with
@@ -58,25 +58,25 @@ variables used.
 Automatic suggestion of proof annotations
 `````````````````````````````````````````
 
-The :flag:`Suggest Proof Using` flag makes |Coq| suggest, when a ``Qed``
+The :flag:`Suggest Proof Using` flag makes Coq suggest, when a ``Qed``
 command is processed, a correct proof annotation. It is up to the user
 to modify the proof script accordingly.
 
 
 Proof blocks and error resilience
 --------------------------------------
 
-|Coq| 8.6 introduced a mechanism for error resilience: in interactive
-mode |Coq| is able to completely check a document containing errors
+Coq 8.6 introduced a mechanism for error resilience: in interactive
+mode Coq is able to completely check a document containing errors
 instead of bailing out at the first failure.
 
 Two kind of errors are supported: errors occurring in vernacular
 commands and errors occurring in proofs.
 
-To properly recover from a failing tactic, |Coq| needs to recognize the
+To properly recover from a failing tactic, Coq needs to recognize the
 structure of the proof in order to confine the error to a sub proof.
 Proof block detection is performed by looking at the syntax of the
-proof script (i.e. also looking at indentation). |Coq| comes with four
+proof script (i.e. also looking at indentation). Coq comes with four
 kind of proof blocks, and an ML API to add new ones.
 
 :curly: blocks are delimited by { and }, see Chapter :ref:`proofhandling`
@@ -92,13 +92,13 @@ Caveats
 When a vernacular command fails the subsequent error messages may be
 bogus, i.e. caused by the first error. Error resilience for vernacular
 commands can be switched off by passing ``-async-proofs-command-error-resilience off``
-to |CoqIDE|.
+to CoqIDE.
 
 An incorrect proof block detection can result into an incorrect error
 recovery and hence in bogus errors. Proof block detection cannot be
 precise for bullets or any other non well parenthesized proof
 structure. Error resilience can be turned off or selectively activated
-for any set of block kind passing to |CoqIDE| one of the following
+for any set of block kind passing to CoqIDE one of the following
 options:
 
 - ``-async-proofs-tactic-error-resilience off``
@@ -113,13 +113,13 @@ Interactive mode
 ---------------------
 
 At the time of writing the only user interface supporting asynchronous
-proof processing is |CoqIDE|.
+proof processing is CoqIDE.
 
-When |CoqIDE| is started, two |Coq| processes are created. The master one
+When CoqIDE is started, two Coq processes are created. The master one
 follows the user, giving feedback as soon as possible by skipping
 proofs, which are delegated to the worker process. The worker process,
 whose state can be seen by clicking on the button in the lower right
-corner of the main |CoqIDE| window, asynchronously processes the proofs.
+corner of the main CoqIDE window, asynchronously processes the proofs.
 If a proof contains an error, it is reported in red in the label of
 the very same button, that can also be used to see the list of errors
 and jump to the corresponding line.
@@ -137,14 +137,14 @@ Only then all the universe constraints are checked.
 Caveats
 ```````
 
-The number of worker processes can be increased by passing |CoqIDE|
+The number of worker processes can be increased by passing CoqIDE
 the ``-async-proofs-j n`` flag. Note that the memory consumption increases too,
 since each worker requires the same amount of memory as the master
 process. Also note that increasing the number of workers may reduce
 the reactivity of the master process to user commands.
 
 To disable this feature, one can pass the ``-async-proofs off`` flag to
-|CoqIDE|. Conversely, on Windows, where the feature is disabled by
+CoqIDE. Conversely, on Windows, where the feature is disabled by
 default, pass the ``-async-proofs on`` flag to enable it.
 
 Proofs that are known to take little time to process are not delegated
@@ -166,9 +166,9 @@ Batch mode
       a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is
       assigned higher priority than the loading of a ``.vio`` file.
 
-When |Coq| is used as a batch compiler by running ``coqc``, it produces
+When Coq is used as a batch compiler by running ``coqc``, it produces
 a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other
-things, theorem statements and proofs. Hence to produce a .vo |Coq|
+things, theorem statements and proofs. Hence to produce a .vo Coq
 need to process all the proofs of the ``.v`` file.
 
 The asynchronous processing of proofs can decouple the generation of a
@@ -224,17 +224,17 @@ heavy use of the ``Type`` hierarchy.
 Limiting the number of parallel workers
 --------------------------------------------
 
-Many |Coq| processes may run on the same computer, and each of them may
+Many Coq processes may run on the same computer, and each of them may
 start many additional worker processes. The ``coqworkmgr`` utility lets
 one limit the number of workers, globally.
 
 The utility accepts the ``-j`` argument to specify the maximum number of
 workers (defaults to 2). ``coqworkmgr`` automatically starts in the
 background and prints an environment variable assignment
 like ``COQWORKMGR_SOCKET=localhost:45634``. The user must set this variable
-in all the shells from which |Coq| processes will be started. If one
+in all the shells from which Coq processes will be started. If one
 uses just one terminal running the bash shell, then
 ``export ‘coqworkmgr -j 4‘`` will do the job.
 
-After that, all |Coq| processes, e.g. ``coqide`` and ``coqc``, will respect the
+After that, all Coq processes, e.g. ``coqide`` and ``coqc``, will respect the
 limit, globally.

doc/sphinx/addendum/program.rst

@@ -8,25 +8,25 @@ Program
 :Author: Matthieu Sozeau
 
 We present here the |Program| tactic commands, used to build
-certified |Coq| programs, elaborating them from their algorithmic
+certified Coq programs, elaborating them from their algorithmic
 skeleton and a rich specification :cite:`sozeau06`. It can be thought of as a
 dual of :ref:`Extraction <extraction>`. The goal of |Program| is to
 program as in a regular functional programming language whilst using
 as rich a specification as desired and proving that the code meets the
-specification using the whole |Coq| proof apparatus. This is done using
+specification using the whole Coq proof apparatus. This is done using
 a technique originating from the “Predicate subtyping” mechanism of
 PVS :cite:`Rushby98`, which generates type checking conditions while typing a
 term constrained to a particular type. Here we insert existential
 variables in the term, which must be filled with proofs to get a
-complete |Coq| term. |Program| replaces the |Program| tactic by Catherine
+complete Coq term. |Program| replaces the |Program| tactic by Catherine
 Parent :cite:`Parent95b` which had a similar goal but is no longer maintained.
 
-The languages available as input are currently restricted to |Coq|’s
-term language, but may be extended to |OCaml|, Haskell and
-others in the future. We use the same syntax as |Coq| and permit to use
+The languages available as input are currently restricted to Coq’s
+term language, but may be extended to OCaml, Haskell and
+others in the future. We use the same syntax as Coq and permit to use
 implicit arguments and the existing coercion mechanism. Input terms
 and types are typed in an extended system (Russell) and interpreted
-into |Coq| terms. The interpretation process may produce some proof
+into Coq terms. The interpretation process may produce some proof
 obligations which need to be resolved to create the final term.
 
 
@@ -35,7 +35,7 @@ obligations which need to be resolved to create the final term.
 Elaborating programs
 --------------------
 
-The main difference from |Coq| is that an object in a type :g:`T : Set` can
+The main difference from Coq is that an object in a type :g:`T : Set` can
 be considered as an object of type :g:`{x : T | P}` for any well-formed
 :g:`P : Prop`. If we go from :g:`T` to the subset of :g:`T` verifying property
 :g:`P`, we must prove that the object under consideration verifies it. Russell
@@ -86,7 +86,7 @@ coercions.
    Controls the special treatment of pattern matching generating equalities
    and disequalities when using |Program| (it is on by default). All
    pattern-matches and let-patterns are handled using the standard algorithm
-   of |Coq| (see :ref:`extendedpatternmatching`) when this flag is
+   of Coq (see :ref:`extendedpatternmatching`) when this flag is
    deactivated.
 
 .. flag:: Program Generalized Coercion
@@ -116,7 +116,7 @@ Syntactic control over equalities
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 To give more control over the generation of equalities, the
-type checker will fall back directly to |Coq|’s usual typing of dependent
+type checker will fall back directly to Coq’s usual typing of dependent
 pattern matching if a ``return`` or ``in`` clause is specified. Likewise, the
 if construct is not treated specially by |Program| so boolean tests in
 the code are not automatically reflected in the obligations. One can
@@ -161,13 +161,13 @@ Program Definition
 A :cmd:`Definition` command with the :attr:`program` attribute types
 the value term in Russell and generates proof
 obligations. Once solved using the commands shown below, it binds the
-final |Coq| term to the name :n:`@ident` in the environment.
+final Coq term to the name :n:`@ident` in the environment.
 
 :n:`Program Definition @ident : @type := @term`
 
 Interprets the type :n:`@type`, potentially generating proof
-obligations to be resolved. Once done with them, we have a |Coq|
-type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a |Coq|
+obligations to be resolved. Once done with them, we have a Coq
+type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a Coq
 term :n:`@term__0`, checking that the type of :n:`@term__0` is coercible to
 :n:`@type__0`, and registers :n:`@ident` as being of type :n:`@type__0` once the
 set of obligations generated during the interpretation of :n:`@term__0`
@@ -342,7 +342,7 @@ Frequently Asked Questions
 .. exn:: Ill-formed recursive definition.
 
   This error can happen when one tries to define a function by structural
-  recursion on a subset object, which means the |Coq| function looks like:
+  recursion on a subset object, which means the Coq function looks like:
 
   ::