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

10 files changed, 79 insertions, 79 deletions

diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index a38282d41a..e029068630 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -117,7 +117,7 @@ Assumptions
 
 Assumptions extend the environment with axioms, parameters, hypotheses
 or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted
-by |Coq| if and only if this :n:`@type` is a correct type in the environment
+by Coq if and only if this :n:`@type` is a correct type in the environment
 preexisting the declaration and if :n:`@ident` was not previously defined in
 the same module. This :n:`@type` is considered to be the type (or
 specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident`
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index dfa2aaf8ff..5406da38a1 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -10,7 +10,7 @@ manual.  Then, we present the essential vocabulary necessary to read
 the rest of the manual.  Other terms are defined throughout the manual.
 The reader may refer to the :ref:`glossary index <glossary_index>`
 for a complete list of defined terms.  Finally, we describe the various types of
-settings that |Coq| provides.
+settings that Coq provides.
 
 Syntax and lexical conventions
 ------------------------------
@@ -21,7 +21,7 @@ Syntax conventions
 ~~~~~~~~~~~~~~~~~~
 
 The syntax described in this documentation is equivalent to that
-accepted by the |Coq| parser, but the grammar has been edited
+accepted by the Coq parser, but the grammar has been edited
 to improve readability and presentation.
 
 In the grammar presented in this manual, the terminal symbols are
@@ -49,13 +49,13 @@ graphically using the following kinds of blocks:
 
 `Precedence levels
 <https://en.wikipedia.org/wiki/Order_of_operations>`_ that are
-implemented in the |Coq| parser are shown in the documentation by
+implemented in the Coq parser are shown in the documentation by
 appending the level to the nonterminal name (as in :n:`@term100` or
 :n:`@ltac_expr3`).
 
 .. note::
 
-   |Coq| uses an extensible parser.  Plugins and the :ref:`notation
+   Coq uses an extensible parser.  Plugins and the :ref:`notation
    system <syntax-extensions-and-notation-scopes>` can extend the
    syntax at run time.  Some notations are defined in the :term:`prelude`,
    which is loaded by default.  The documented grammar doesn't include
@@ -71,8 +71,8 @@ appending the level to the nonterminal name (as in :n:`@term100` or
 
    Given the complexity of these parsing rules, it would be extremely
    difficult to create an external program that can properly parse a
-   |Coq| document.  Therefore, tool writers are advised to delegate
-   parsing to |Coq|, by communicating with it, for instance through
+   Coq document.  Therefore, tool writers are advised to delegate
+   parsing to Coq, by communicating with it, for instance through
    `SerAPI <https://github.com/ejgallego/coq-serapi>`_.
 
 .. seealso:: :cmd:`Print Grammar`
@@ -134,7 +134,7 @@ Numbers
      hexdigit ::= {| 0 .. 9 | a .. f | A .. F }
 
   :n:`@integer` and :n:`@natural` are limited to the range that fits
-  into an |OCaml| integer (63-bit integers on most architectures).
+  into an OCaml integer (63-bit integers on most architectures).
   :n:`@bigint` and :n:`@bignat` have no range limitation.
 
   The :ref:`standard library <thecoqlibrary>` provides some
@@ -152,8 +152,8 @@ Strings
   :token:`string`.
 
 Keywords
-  The following character sequences are keywords defined in the main |Coq| grammar
-  that cannot be used as identifiers (even when starting |Coq| with the `-noinit`
+  The following character sequences are keywords defined in the main Coq grammar
+  that cannot be used as identifiers (even when starting Coq with the `-noinit`
   command-line flag)::
 
     _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop
@@ -168,8 +168,8 @@ Keywords
   keywords.
 
 Other tokens
-  The following character sequences are tokens defined in the main |Coq| grammar
-  (even when starting |Coq| with the `-noinit` command-line flag)::
+  The following character sequences are tokens defined in the main Coq grammar
+  (even when starting Coq with the `-noinit` command-line flag)::
 
     ! #[ % & ' ( () ) * + , - ->
     . .( .. ... / : ::= := :> ; < <+ <- <:
@@ -195,7 +195,7 @@ Essential vocabulary
 --------------------
 
 This section presents the most essential notions to understand the
-rest of the |Coq| manual: :term:`terms <term>` and :term:`types
+rest of the Coq manual: :term:`terms <term>` and :term:`types
 <type>` on the one hand, :term:`commands <command>` and :term:`tactics
 <tactic>` on the other hand.
 
@@ -203,14 +203,14 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
 
    term
 
-     Terms are the basic expressions of |Coq|.  Terms can represent
+     Terms are the basic expressions of Coq.  Terms can represent
      mathematical expressions, propositions and proofs, but also
      executable programs and program types.
 
      Here is the top-level syntax of terms.  Each of the listed
      constructs is presented in a dedicated section.  Some of these
      constructs (like :n:`@term_forall_or_fun`) are part of the core
-     language that the kernel of |Coq| understands and are therefore
+     language that the kernel of Coq understands and are therefore
      described in :ref:`this chapter <core-language>`, while
      others (like :n:`@term_if`) are language extensions that are
      presented in :ref:`the next chapter <extensions>`.
@@ -256,18 +256,18 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
 
    type
 
-     To be valid and accepted by the |Coq| kernel, a term needs an
+     To be valid and accepted by the Coq kernel, a term needs an
      associated type.  We express this relationship by “:math:`x` *of
      type* :math:`T`”, which we write as “:math:`x:T`”.  Informally,
      “:math:`x:T`” can be thought as “:math:`x` *belongs to*
      :math:`T`”.
 
-     The |Coq| kernel is a type checker: it verifies that a term has
+     The Coq kernel is a type checker: it verifies that a term has
      the expected type by applying a set of typing rules (see
      :ref:`Typing-rules`).  If that's indeed the case, we say that the
      term is :gdef:`well-typed`.
 
-     A special feature of the |Coq| language is that types can depend
+     A special feature of the Coq language is that types can depend
      on terms (we say that the language is `dependently-typed
      <https://en.wikipedia.org/wiki/Dependent_type>`_).  Because of
      this, types and terms share a common syntax.  All types are terms,
@@ -289,13 +289,13 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
      mathematics alternative to the standard `"set theory"
      <https://en.wikipedia.org/wiki/Set_theory>`_: we call such
      logical foundations `"type theories"
-     <https://en.wikipedia.org/wiki/Type_theory>`_.  |Coq| is based on
+     <https://en.wikipedia.org/wiki/Type_theory>`_.  Coq is based on
      the Calculus of Inductive Constructions, which is a particular
      instance of type theory.
 
    sentence
 
-     |Coq| documents are made of a series of sentences that contain
+     Coq documents are made of a series of sentences that contain
      :term:`commands <command>` or :term:`tactics <tactic>`, generally
      terminated with a period and optionally decorated with
      :term:`attributes <attribute>`.
@@ -315,7 +315,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
 
    command
 
-     A :production:`command` can be used to modify the state of a |Coq|
+     A :production:`command` can be used to modify the state of a Coq
      document, for instance by declaring a new object, or to get
      information about the current state.
 
@@ -334,7 +334,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
 
      Tactics specify how to transform the current proof state as a
      step in creating a proof.  They are syntactically valid only when
-     |Coq| is in proof mode, such as after a :cmd:`Theorem` command
+     Coq is in proof mode, such as after a :cmd:`Theorem` command
      and before any subsequent proof-terminating command such as
      :cmd:`Qed`.  See :ref:`proofhandling` for more on proof mode.
 
@@ -346,10 +346,10 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
 Settings
 --------
 
-There are several mechanisms for changing the behavior of |Coq|.  The
+There are several mechanisms for changing the behavior of Coq.  The
 :term:`attribute` mechanism is used to modify the behavior of a single
 :term:`sentence`.  The :term:`flag`, :term:`option` and :term:`table`
-mechanisms are used to modify the behavior of |Coq| more globally in a
+mechanisms are used to modify the behavior of Coq more globally in a
 document or project.
 
 .. _attributes:
@@ -420,7 +420,7 @@ boldface label "Attribute:".  Attributes are listed in the
 Flags, Options and Tables
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The following types of settings can be used to change the behavior of |Coq| in
+The following types of settings can be used to change the behavior of Coq in
 subsequent commands and tactics (see :ref:`set_unset_scope_qualifiers` for a
 more precise description of the scope of these settings):
 
@@ -463,10 +463,10 @@ they appear after a boldface label.  They are listed in the
       This warning message can be raised by :cmd:`Set` and
       :cmd:`Unset` when :n:`@setting_name` is unknown.  It is a
       warning rather than an error because this helps library authors
-      produce |Coq| code that is compatible with several |Coq| versions.
+      produce Coq code that is compatible with several Coq versions.
       To preserve the same behavior, they may need to set some
       compatibility flags or options that did not exist in previous
-      |Coq| versions.
+      Coq versions.
 
 .. cmd:: Unset @setting_name
    :name: Unset
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index 2e5dff42ac..3e2ecdc0f0 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -76,7 +76,7 @@ propositional η-equality, which itself would require full η-conversion for
 subject reduction to hold, but full η-conversion is not acceptable as it would
 make type checking undecidable.
 
-Since the introduction of primitive records in |Coq| 8.5, an alternative
+Since the introduction of primitive records in Coq 8.5, an alternative
 presentation is available, called *negative co-inductive types*. This consists
 in defining a co-inductive type as a primitive record type through its
 projections. Such a technique is akin to the *co-pattern* style that can be
@@ -115,7 +115,7 @@ equality:
 
    Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2.
 
-As of |Coq| 8.9, it is now advised to use negative co-inductive types rather than
+As of Coq 8.9, it is now advised to use negative co-inductive types rather than
 their positive counterparts.
 
 .. seealso::
@@ -195,7 +195,7 @@ Top-level definitions of co-recursive functions
    As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously
    defining several mutual cofixpoints.
 
-   If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
+   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst
index 6b031cfea3..7395b12339 100644
--- a/doc/sphinx/language/core/conversion.rst
+++ b/doc/sphinx/language/core/conversion.rst
@@ -85,7 +85,7 @@ reduction is called δ-reduction and shows as follows.
 ζ-reduction
 ~~~~~~~~~~~
 
-|Coq| allows also to remove local definitions occurring in terms by
+Coq allows also to remove local definitions occurring in terms by
 replacing the defined variable by its value. The declaration being
 destroyed, this reduction differs from δ-reduction. It is called
 ζ-reduction and shows as follows.
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 1681eee6e7..4ea3ea5e6d 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -90,7 +90,7 @@ Section :ref:`typing-rules`.
    :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`),
    :attr:`canonical` and :attr:`using` attributes.
 
-   If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
+   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
@@ -135,7 +135,7 @@ Chapter :ref:`Tactics`. The basic assertion command is:
       | Proposition
       | Property
 
-   After the statement is asserted, |Coq| needs a proof. Once a proof of
+   After the statement is asserted, Coq needs a proof. Once a proof of
    :n:`@type` under the assumptions represented by :n:`@binder`\s is given and
    validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and
    the theorem is bound to the name :n:`@ident` in the environment.
@@ -176,7 +176,7 @@ Chapter :ref:`Tactics`. The basic assertion command is:
       This feature, called nested proofs, is disabled by default.
       To activate it, turn the :flag:`Nested Proofs Allowed` flag on.
 
-Proofs start with the keyword :cmd:`Proof`. Then |Coq| enters the proof editing mode
+Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode
 until the proof is completed. In proof editing mode, the user primarily enters
 tactics, which are described in chapter :ref:`Tactics`. The user may also enter
 commands to manage the proof editing mode. They are described in Chapter
diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst
index c7b1df28db..de780db267 100644
--- a/doc/sphinx/language/core/index.rst
+++ b/doc/sphinx/language/core/index.rst
@@ -4,7 +4,7 @@
 Core language
 =============
 
-At the heart of the |Coq| proof assistant is the |Coq| kernel.  While
+At the heart of the Coq proof assistant is the Coq kernel.  While
 users have access to a language with many convenient features such as
 :ref:`notations <syntax-extensions-and-notation-scopes>`,
 :ref:`implicit arguments <ImplicitArguments>`, etc.  (presented in the
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 1642482bb1..d3bd787587 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -17,7 +17,7 @@ Inductive types
       constructor ::= @ident {* @binder } {? @of_type }
 
    This command defines one or more
-   inductive types and its constructors.  |Coq| generates destructors
+   inductive types and its constructors.  Coq generates destructors
    depending on the universe that the inductive type belongs to.
 
    The destructors are named :n:`@ident`\ ``_rect``, :n:`@ident`\ ``_ind``,
@@ -411,7 +411,7 @@ constructions.
    It is especially useful when defining functions over mutually defined
    inductive types.  Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`.
 
-   If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
+   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
@@ -552,7 +552,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort`
       \end{array}
       \right]}
 
-   which corresponds to the result of the |Coq| declaration:
+   which corresponds to the result of the Coq declaration:
 
    .. coqtop:: in reset
 
@@ -573,7 +573,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort`
                 \consf &:& \tree → \forest → \forest\\
                           \end{array}\right]}
 
-   which corresponds to the result of the |Coq| declaration:
+   which corresponds to the result of the Coq declaration:
 
    .. coqtop:: in
 
@@ -596,7 +596,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort`
                 \oddS &:& ∀ n,~\even~n → \odd~(\nS~n)
                           \end{array}\right]}
 
-   which corresponds to the result of the |Coq| declaration:
+   which corresponds to the result of the Coq declaration:
 
    .. coqtop:: in
 
@@ -1099,7 +1099,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    template polymorphic, even if the :flag:`Auto Template
    Polymorphism` flag is on.
 
-In practice, the rule **Ind-Family** is used by |Coq| only when all the
+In practice, the rule **Ind-Family** is used by Coq only when all the
 inductive types of the inductive definition are declared with an arity
 whose sort is in the Type hierarchy. Then, the polymorphism is over
 the parameters whose type is an arity of sort in the Type hierarchy.
@@ -1237,7 +1237,7 @@ at the computational level it implements a generic operator for doing
 primitive recursion over the structure.
 
 But this operator is rather tedious to implement and use. We choose in
-this version of |Coq| to factorize the operator for primitive recursion
+this version of Coq to factorize the operator for primitive recursion
 into two more primitive operations as was first suggested by Th.
 Coquand in :cite:`Coq92`. One is the definition by pattern matching. The
 second one is a definition by guarded fixpoints.
@@ -1252,7 +1252,7 @@ The basic idea of this operator is that we have an object :math:`m` in an
 inductive type :math:`I` and we want to prove a property which possibly
 depends on :math:`m`. For this, it is enough to prove the property for
 :math:`m = (c_i~u_1 … u_{p_i} )` for each constructor of :math:`I`.
-The |Coq| term for this proof
+The Coq term for this proof
 will be written:
 
 .. math::
@@ -1267,7 +1267,7 @@ Actually, for type checking a :math:`\Match…\with…\kwend` expression we also
 to know the predicate :math:`P` to be proved by case analysis. In the general
 case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate
 over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I`
-(parameters excluded), and the last one corresponds to object :math:`m`. |Coq|
+(parameters excluded), and the last one corresponds to object :math:`m`. Coq
 can sometimes infer this predicate but sometimes not. The concrete
 syntax for describing this predicate uses the :math:`\as…\In…\return`
 construction. For instance, let us assume that :math:`I` is an unary predicate
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 1309a47ff4..54252689e1 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -864,17 +864,17 @@ Libraries and qualified names
 Names of libraries
 ~~~~~~~~~~~~~~~~~~
 
-The theories developed in |Coq| are stored in *library files* which are
+The theories developed in Coq are stored in *library files* which are
 hierarchically classified into *libraries* and *sublibraries*. To
 express this hierarchy, library names are represented by qualified
 identifiers qualid, i.e. as list of identifiers separated by dots (see
 :ref:`qualified-names`). For instance, the library file ``Mult`` of the standard
-|Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts
+Coq library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts
 the name of a library is called a *library root*. All library files of
-the standard library of |Coq| have the reserved root |Coq| but library
-filenames based on other roots can be obtained by using |Coq| commands
+the standard library of Coq have the reserved root Coq but library
+filenames based on other roots can be obtained by using Coq commands
 (coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`command-line-options`).
-Also, when an interactive |Coq| session starts, a library of root ``Top`` is
+Also, when an interactive Coq session starts, a library of root ``Top`` is
 started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-options`).
 
 .. _qualified-names:
@@ -897,7 +897,7 @@ followed by the sequence of submodules names encapsulating the
 construction and ended by the proper name of the construction.
 Typically, the absolute name ``Coq.Init.Logic.eq`` denotes Leibniz’
 equality defined in the module Logic in the sublibrary ``Init`` of the
-standard library of |Coq|.
+standard library of Coq.
 
 The proper name that ends the name of a construction is the short name
 (or sometimes base name) of the construction (for instance, the short
@@ -906,7 +906,7 @@ name is a *partially qualified name* (e.g. ``Logic.eq`` is a partially
 qualified name for ``Coq.Init.Logic.eq``). Especially, the short name of a
 construction is its shortest partially qualified name.
 
-|Coq| does not accept two constructions (definition, theorem, …) with
+Coq does not accept two constructions (definition, theorem, …) with
 the same absolute name but different constructions can have the same
 short name (or even same partially qualified names as soon as the full
 names are different).
@@ -916,14 +916,14 @@ names also applies to library filenames.
 
 **Visibility**
 
-|Coq| maintains a table called the name table which maps partially qualified
+Coq maintains a table called the name table which maps partially qualified
 names of constructions to absolute names. This table is updated by the
 commands :cmd:`Require`, :cmd:`Import` and :cmd:`Export` and
 also each time a new declaration is added to the context. An absolute
 name is called visible from a given short or partially qualified name
 when this latter name is enough to denote it. This means that the
 short or partially qualified name is mapped to the absolute name in
-|Coq| name table. Definitions with the :attr:`local` attribute are only accessible with
+Coq name table. Definitions with the :attr:`local` attribute are only accessible with
 their fully qualified name (see :ref:`gallina-definitions`).
 
 It may happen that a visible name is hidden by the short name or a
@@ -953,13 +953,13 @@ accessible, absolute names can never be hidden.
 Libraries and filesystem
 ~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. note:: The questions described here have been subject to redesign in |Coq| 8.5.
-   Former versions of |Coq| use the same terminology to describe slightly different things.
+.. note:: The questions described here have been subject to redesign in Coq 8.5.
+   Former versions of Coq use the same terminology to describe slightly different things.
 
 Compiled files (``.vo`` and ``.vio``) store sub-libraries. In order to refer
-to them inside |Coq|, a translation from file-system names to |Coq| names
+to them inside Coq, a translation from file-system names to Coq names
 is needed. In this translation, names in the file system are called
-*physical* paths while |Coq| names are contrastingly called *logical*
+*physical* paths while Coq names are contrastingly called *logical*
 names.
 
 A logical prefix Lib can be associated with a physical path using
@@ -967,7 +967,7 @@ the command line option ``-Q`` `path` ``Lib``. All subfolders of path are
 recursively associated to the logical path ``Lib`` extended with the
 corresponding suffix coming from the physical path. For instance, the
 folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding
-to invalid |Coq| identifiers are skipped, and, by convention,
+to invalid Coq identifiers are skipped, and, by convention,
 subdirectories named ``CVS`` or ``_darcs`` are skipped too.
 
 Thanks to this mechanism, ``.vo`` files are made available through the
@@ -979,7 +979,7 @@ its logical name, so that an error is issued if it is loaded with the
 wrong loadpath afterwards.
 
 Some folders have a special status and are automatically put in the
-path. |Coq| commands associate automatically a logical path to files in
+path. Coq commands associate automatically a logical path to files in
 the repository trees rooted at the directory from where the command is
 launched, ``coqlib/user-contrib/``, the directories listed in the
 ``$COQPATH``, ``${XDG_DATA_HOME}/coq/`` and ``${XDG_DATA_DIRS}/coq/``
@@ -1001,12 +1001,12 @@ of the ``Require`` command can be used to bypass the implicit shortening
 by providing an absolute root to the required file (see :ref:`compiled-files`).
 
 There also exists another independent loadpath mechanism attached to
-|OCaml| object files (``.cmo`` or ``.cmxs``) rather than |Coq| object
-files as described above. The |OCaml| loadpath is managed using
-the option ``-I`` `path` (in the |OCaml| world, there is neither a
+OCaml object files (``.cmo`` or ``.cmxs``) rather than Coq object
+files as described above. The OCaml loadpath is managed using
+the option ``-I`` `path` (in the OCaml world, there is neither a
 notion of logical name prefix nor a way to access files in
 subdirectories of path). See the command :cmd:`Declare ML Module` in
-:ref:`compiled-files` to understand the need of the |OCaml| loadpath.
+:ref:`compiled-files` to understand the need of the OCaml loadpath.
 
-See :ref:`command-line-options` for a more general view over the |Coq| command
+See :ref:`command-line-options` for a more general view over the Coq command
 line options.
diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst
index 17f569ca2a..4505fc4b4d 100644
--- a/doc/sphinx/language/core/primitive.rst
+++ b/doc/sphinx/language/core/primitive.rst
@@ -45,13 +45,13 @@ applications of these primitive operations.
 
 The extraction of these primitives can be customized similarly to the extraction
 of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63`
-module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types
-and functions of a :g:`Uint63` module. That |OCaml| module is not produced by
+module can be used when extracting to OCaml: it maps the Coq primitives to types
+and functions of a :g:`Uint63` module. That OCaml module is not produced by
 extraction. Instead, it has to be provided by the user (if they want to compile
 or execute the extracted code). For instance, an implementation of this module
-can be taken from the kernel of |Coq|.
+can be taken from the kernel of Coq.
 
-Literal values (at type :g:`Int63.int`) are extracted to literal |OCaml| values
+Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values
 wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on
 64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the
 function :g:`Uint63.compile` from the kernel).
@@ -94,13 +94,13 @@ to comply with the IEEE 754 standard for floating-point arithmetic.
 
 The extraction of these primitives can be customized similarly to the extraction
 of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats`
-module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types
-and functions of a :g:`Float64` module. Said |OCaml| module is not produced by
+module can be used when extracting to OCaml: it maps the Coq primitives to types
+and functions of a :g:`Float64` module. Said OCaml module is not produced by
 extraction. Instead, it has to be provided by the user (if they want to compile
 or execute the extracted code). For instance, an implementation of this module
-can be taken from the kernel of |Coq|.
+can be taken from the kernel of Coq.
 
-Literal values (of type :g:`Float64.t`) are extracted to literal |OCaml|
+Literal values (of type :g:`Float64.t`) are extracted to literal OCaml
 values (of type :g:`float`) written in hexadecimal notation and
 wrapped into the :g:`Float64.of_float` constructor, e.g.:
 :g:`Float64.of_float (0x1p+0)`.
@@ -144,19 +144,19 @@ operations.
 
 The extraction of these primitives can be customized similarly to the extraction
 of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlPArray`
-module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types
-and functions of a :g:`Parray` module. Said |OCaml| module is not produced by
+module can be used when extracting to OCaml: it maps the Coq primitives to types
+and functions of a :g:`Parray` module. Said OCaml module is not produced by
 extraction. Instead, it has to be provided by the user (if they want to compile
 or execute the extracted code). For instance, an implementation of this module
-can be taken from the kernel of |Coq| (see ``kernel/parray.ml``).
+can be taken from the kernel of Coq (see ``kernel/parray.ml``).
 
-|Coq|'s primitive arrays are persistent data structures. Semantically, a set operation
+Coq's primitive arrays are persistent data structures. Semantically, a set operation
 ``t.[i <- a]`` represents a new array that has the same values as ``t``, except
 at position ``i`` where its value is ``a``. The array ``t`` still exists, can
 still be used and its values were not modified. Operationally, the implementation
-of |Coq|'s primitive arrays is optimized so that the new array ``t.[i <- a]`` does not
+of Coq's primitive arrays is optimized so that the new array ``t.[i <- a]`` does not
 copy all of ``t``. The details are in section 2.3 of :cite:`ConchonFilliatre07wml`.
-In short, the implementation keeps one version of ``t`` as an |OCaml| native array and
+In short, the implementation keeps one version of ``t`` as an OCaml native array and
 other versions as lists of modifications to ``t``. Accesses to the native array
 version are constant time operations. However, accesses to versions where all the cells of
 the array are modified have O(n) access time, the same as a list. The version that is kept as the native array
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
index c70f7a347b..df50dbafe3 100644
--- a/doc/sphinx/language/core/sections.rst
+++ b/doc/sphinx/language/core/sections.rst
@@ -84,7 +84,7 @@ Sections create local contexts which can be shared across multiple definitions.
    will be wrapped with a :n:`@term_let` with the same declaration.
 
    As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`,
-   if :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
+   if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.