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

18 files changed, 129 insertions, 129 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index f1ed64e52a..85b04f6df0 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1,7 +1,7 @@
 Typing rules
 ====================================
 
-The underlying formal language of |Coq| is a *Calculus of Inductive
+The underlying formal language of Coq is a *Calculus of Inductive
 Constructions* (|Cic|) whose inference rules are presented in this
 chapter. The history of this formalism as well as pointers to related
 work are provided in a separate chapter; see *Credits*.
@@ -33,7 +33,7 @@ the following rules.
 #. variables, hereafter ranged over by letters :math:`x`, :math:`y`, etc., are terms
 #. constants, hereafter ranged over by letters :math:`c`, :math:`d`, etc., are terms.
 #. if :math:`x` is a variable and :math:`T`, :math:`U` are terms then
-   :math:`∀ x:T,~U` (:g:`forall x:T, U`   in |Coq| concrete syntax) is a term.
+   :math:`∀ x:T,~U` (:g:`forall x:T, U`   in Coq concrete syntax) is a term.
    If :math:`x` occurs in :math:`U`, :math:`∀ x:T,~U` reads as
    “for all :math:`x` of type :math:`T`, :math:`U`”.
    As :math:`U` depends on :math:`x`, one says that :math:`∀ x:T,~U` is
@@ -43,11 +43,11 @@ the following rules.
    written: :math:`T \rightarrow U`.
 #. if :math:`x` is a variable and :math:`T`, :math:`u` are terms then
    :math:`λ x:T .~u` (:g:`fun x:T => u`
-   in |Coq| concrete syntax) is a term. This is a notation for the
+   in Coq concrete syntax) is a term. This is a notation for the
    λ-abstraction of λ-calculus :cite:`Bar81`. The term :math:`λ x:T .~u` is a function
    which maps elements of :math:`T` to the expression :math:`u`.
 #. if :math:`t` and :math:`u` are terms then :math:`(t~u)` is a term
-   (:g:`t u` in |Coq| concrete
+   (:g:`t u` in Coq concrete
    syntax). The term :math:`(t~u)` reads as “:math:`t` applied to :math:`u`”.
 #. if :math:`x` is a variable, and :math:`t`, :math:`T` and :math:`u` are
    terms then :math:`\letin{x}{t:T}{u}` is
@@ -91,10 +91,10 @@ Let us assume that ``mult`` is a function of type :math:`\nat→\nat→\nat` and
 predicate of type :math:`\nat→\nat→ \Prop`. The λ-abstraction can serve to build
 “ordinary” functions as in :math:`λ x:\nat.~(\kw{mult}~x~x)` (i.e.
 :g:`fun x:nat => mult x x`
-in |Coq| notation) but may build also predicates over the natural
+in Coq notation) but may build also predicates over the natural
 numbers. For instance :math:`λ x:\nat.~(\kw{eqnat}~x~0)`
 (i.e. :g:`fun x:nat => eqnat x 0`
-in |Coq| notation) will represent the predicate of one variable :math:`x` which
+in Coq notation) will represent the predicate of one variable :math:`x` which
 asserts the equality of :math:`x` with :math:`0`. This predicate has type
 :math:`\nat → \Prop`
 and it can be applied to any expression of type :math:`\nat`, say :math:`t`, to give an
@@ -524,7 +524,7 @@ One can consequently derive the following property.
 The Calculus of Inductive Constructions with impredicative Set
 -----------------------------------------------------------------
 
-|Coq| can be used as a type checker for the Calculus of Inductive
+Coq can be used as a type checker for the Calculus of Inductive
 Constructions with an impredicative sort :math:`\Set` by using the compiler
 option ``-impredicative-set``. For example, using the ordinary `coqtop`
 command, the following is rejected,
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 485dfd964d..d061ed41f1 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -1,28 +1,28 @@
 .. _thecoqlibrary:
 
-The |Coq| library
+The Coq library
 =================
 
 .. index::
    single: Theories
 
 
-The |Coq| library has two parts:
+The Coq library has two parts:
 
   * The :gdef:`prelude`: definitions and theorems for
     the most commonly used elementary logical notions and
-    data types. |Coq| normally loads these files automatically when it starts.
+    data types. Coq normally loads these files automatically when it starts.
 
   * The :gdef:`standard library`: general-purpose libraries with
     definitions and theorems for sets, lists, sorting,
     arithmetic, etc. To use these files, users must load them explicitly
     with the ``Require`` command (see :ref:`compiled-files`)
 
-There are also many libraries provided by |Coq| users' community.
+There are also many libraries provided by Coq users' community.
 These libraries and developments are available
 for download at http://coq.inria.fr (see :ref:`userscontributions`).
 
-This chapter briefly reviews the |Coq| libraries whose contents can
+This chapter briefly reviews the Coq libraries whose contents can
 also be browsed at http://coq.inria.fr/stdlib/.
 
 
@@ -32,9 +32,9 @@ The prelude
 -----------
 
 This section lists the basic notions and results which are directly
-available in the standard |Coq| system. Most of these constructions
+available in the standard Coq system. Most of these constructions
 are defined in the ``Prelude`` module in directory ``theories/Init``
-in the |Coq| root directory; this includes the modules
+in the Coq root directory; this includes the modules
 ``Notations``,
 ``Logic``,
 ``Datatypes``,
@@ -92,7 +92,7 @@ Notation          Precedence    Associativity
 Logic
 ~~~~~
 
-The basic library of |Coq| comes with the definitions of standard
+The basic library of Coq comes with the definitions of standard
 (intuitionistic) logical connectives (they are defined as inductive
 constructions). They are equipped with an appealing syntax enriching the
 subclass :token:`form` of the syntactic class :token:`term`. The constructs
@@ -767,7 +767,7 @@ the modules they provide are compiled at installation time. So they
 are directly accessible with the command ``Require`` (see
 Section :ref:`compiled-files`).
 
-The different modules of the |Coq| standard library are documented
+The different modules of the Coq standard library are documented
 online at https://coq.inria.fr/stdlib.
 
 Peano’s arithmetic (nat)
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`.
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index f8c0e23696..2460461ede 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -182,7 +182,7 @@ Manual declaration of implicit arguments
 Automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-   The ":n:`default implicits`" :token:`args_modifier` clause tells |Coq| to automatically determine the
+   The ":n:`default implicits`" :token:`args_modifier` clause tells Coq to automatically determine the
    implicit arguments of the object.
 
    Auto-detection is governed by flags specifying whether strict,
@@ -378,7 +378,7 @@ Effects of :cmd:`Arguments` on unfolding
 Bidirectionality hints
 ~~~~~~~~~~~~~~~~~~~~~~
 
-When type-checking an application, |Coq| normally does not use information from
+When type-checking an application, Coq normally does not use information from
 the context to infer the types of the arguments. It only checks after the fact
 that the type inferred for the application is coherent with the expected type.
 Bidirectionality hints make it possible to specify that after type-checking the
@@ -395,7 +395,7 @@ the context to help inferring the types of the remaining arguments.
   * *type inference*, with is inferring the type of a construct by analyzing the construct.
 
   Methods that combine these approaches are known as *bidirectional typing*.
-  |Coq| normally uses only the first approach to infer the types of arguments,
+  Coq normally uses only the first approach to infer the types of arguments,
   then later verifies that the inferred type is consistent with the expected type.
   *Bidirectionality hints* specify to use both methods: after type checking the
   first arguments of an application (appearing before the `&` in :cmd:`Arguments`),
@@ -417,7 +417,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`).
       Definition b2n (b : bool) := if b then 1 else 0.
       Coercion b2n : bool >-> nat.
 
-   |Coq| cannot automatically coerce existential statements over ``bool`` to
+   Coq cannot automatically coerce existential statements over ``bool`` to
    statements over ``nat``, because the need for inserting a coercion is known
    only from the expected type of a subterm:
 
@@ -432,7 +432,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`).
       Arguments ex_intro _ _ & _ _.
       Check (ex_intro _ true _ : exists n : nat, n > 0).
 
-|Coq| will attempt to produce a term which uses the arguments you
+Coq will attempt to produce a term which uses the arguments you
 provided, but in some cases involving Program mode the arguments after
 the bidirectionality starts may be replaced by convertible but
 syntactically different terms.
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index 38c9fa336d..48120503af 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -159,7 +159,7 @@ of the terms that are compared.
     End theory.
   End EQ.
 
-We use |Coq| modules as namespaces. This allows us to follow the same
+We use Coq modules as namespaces. This allows us to follow the same
 pattern and naming convention for the rest of the chapter. The base
 namespace contains the definitions of the algebraic structure. To
 keep the example small, the algebraic structure ``EQ.type`` we are
@@ -196,7 +196,7 @@ We amend that by equipping ``nat`` with a comparison relation.
    Check 3 == 3.
    Eval compute in 3 == 4.
 
-This last test shows that |Coq| is now not only able to type check ``3 == 3``,
+This last test shows that Coq is now not only able to type check ``3 == 3``,
 but also that the infix relation was bound to the ``nat_eq`` relation.
 This relation is selected whenever ``==`` is used on terms of type nat.
 This can be read in the line declaring the canonical structure
@@ -223,8 +223,8 @@ example work:
 
   Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b).
 
-The error message is telling that |Coq| has no idea on how to compare
-pairs of objects. The following construction is telling |Coq| exactly
+The error message is telling that Coq has no idea on how to compare
+pairs of objects. The following construction is telling Coq exactly
 how to do that.
 
 .. coqtop:: all
@@ -241,7 +241,7 @@ how to do that.
 
   Check forall n m : nat, (3, 4) == (n, m).
 
-Thanks to the ``pair_EQty`` declaration, |Coq| is able to build a comparison
+Thanks to the ``pair_EQty`` declaration, Coq is able to build a comparison
 relation for pairs whenever it is able to build a comparison relation
 for each component of the pair. The declaration associates to the key ``*``
 (the type constructor of pairs) the canonical comparison
@@ -290,7 +290,7 @@ As before we register a canonical ``LE`` class for ``nat``.
 
   Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
 
-And we enable |Coq| to relate pair of terms with ``<=``.
+And we enable Coq to relate pair of terms with ``<=``.
 
 .. coqtop:: all
 
@@ -355,10 +355,10 @@ theory of this new class.
 
 
 The problem is that the two classes ``LE`` and ``LEQ`` are not yet related by
-a subclass relation. In other words |Coq| does not see that an object of
+a subclass relation. In other words Coq does not see that an object of
 the ``LEQ`` class is also an object of the ``LE`` class.
 
-The following two constructions tell |Coq| how to canonically build the
+The following two constructions tell Coq how to canonically build the
 ``LE.type`` and ``EQ.type`` structure given an ``LEQ.type`` structure on the same
 type.
 
@@ -413,7 +413,7 @@ setting to any concrete instate of the algebraic structure.
 
   Abort.
 
-Again one has to tell |Coq| that the type ``nat`` is in the ``LEQ`` class, and
+Again one has to tell Coq that the type ``nat`` is in the ``LEQ`` class, and
 how the type constructor ``*`` interacts with the ``LEQ`` class. In the
 following proofs are omitted for brevity.
 
@@ -468,7 +468,7 @@ Note that no direct proof of ``n <= m -> m <= n -> n == m`` is provided by
 the user for ``n`` and m of type ``nat * nat``. What the user provides is a
 proof of this statement for ``n`` and ``m`` of type ``nat`` and a proof that the
 pair constructor preserves this property. The combination of these two
-facts is a simple form of proof search that |Coq| performs automatically
+facts is a simple form of proof search that Coq performs automatically
 while inferring canonical structures.
 
 Compact declaration of Canonical Structures
@@ -507,7 +507,7 @@ instances: ``[find e | EQ.obj e ~ T | "is not an EQ.type" ]``. It should be
 read as: “find a class e such that its objects have type T or fail
 with message "T is not an EQ.type"”.
 
-The other utilities are used to ask |Coq| to solve a specific unification
+The other utilities are used to ask Coq to solve a specific unification
 problem, that will in turn require the inference of some canonical structures.
 They are explained in more details in :cite:`CSwcu`.
 
@@ -532,7 +532,7 @@ The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers al
 the other pieces of the class ``LEQ`` and declares them as canonical
 values associated to the ``T`` key. All in all, the only new piece of
 information we add in the ``LEQ`` class is the mixin, all the rest is
-already canonical for ``T`` and hence can be inferred by |Coq|.
+already canonical for ``T`` and hence can be inferred by Coq.
 
 ``Pack`` is a notation, hence it is not type checked at the time of its
 declaration. It will be type checked when it is used, an in that case ``T`` is
diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
index dc208a63a0..fd9695e270 100644
--- a/doc/sphinx/language/extensions/evars.rst
+++ b/doc/sphinx/language/extensions/evars.rst
@@ -13,7 +13,7 @@ Existential variables
    | ?[ ?@ident ]
    | ?@ident {? @%{ {+; @ident := @term } %} }
 
-|Coq| terms can include existential variables that represent unknown
+Coq terms can include existential variables that represent unknown
 subterms that are eventually replaced with actual subterms.
 
 Existential variables are generated in place of unsolved implicit
@@ -68,7 +68,7 @@ Inferable subterms
 ~~~~~~~~~~~~~~~~~~
 
 Expressions often contain redundant pieces of information. Subterms that can be
-automatically inferred by |Coq| can be replaced by the symbol ``_`` and |Coq| will
+automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will
 guess the missing piece of information.
 
 .. extracted from Gallina extensions chapter
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index 9457505feb..23ba5f703a 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -115,7 +115,7 @@ application will include that argument.  Otherwise, the argument is
 *non-maximally inserted* and the partial application will not include that argument.
 
 Each implicit argument can be declared to be inserted maximally or non
-maximally. In |Coq|, maximally inserted implicit arguments are written between curly braces
+maximally. In Coq, maximally inserted implicit arguments are written between curly braces
 "{ }" and non-maximally inserted implicit arguments are written in square brackets "[ ]".
 
 .. seealso:: :flag:`Maximal Implicit Insertion`
@@ -146,7 +146,7 @@ by replacing it with `_`.
 .. exn:: Cannot infer a term for this placeholder.
    :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments)
 
-   |Coq| was not able to deduce an instantiation of a “_”.
+   Coq was not able to deduce an instantiation of a “_”.
 
 .. _declare-implicit-args:
 
@@ -290,8 +290,8 @@ Controlling contextual implicit arguments
 
 .. flag:: Contextual Implicit
 
-   By default, |Coq| does not automatically set implicit the contextual
-   implicit arguments. You can turn this flag on to tell |Coq| to also
+   By default, Coq does not automatically set implicit the contextual
+   implicit arguments. You can turn this flag on to tell Coq to also
    infer contextual implicit argument.
 
 .. _controlling-rev-pattern-implicit-args:
@@ -301,8 +301,8 @@ Controlling reversible-pattern implicit arguments
 
 .. flag:: Reversible Pattern Implicit
 
-   By default, |Coq| does not automatically set implicit the reversible-pattern
-   implicit arguments. You can turn this flag on to tell |Coq| to also infer
+   By default, Coq does not automatically set implicit the reversible-pattern
+   implicit arguments. You can turn this flag on to tell Coq to also infer
    reversible-pattern implicit argument.
 
 .. _controlling-insertion-implicit-args:
diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst
index ea7271179e..ed207ca743 100644
--- a/doc/sphinx/language/extensions/index.rst
+++ b/doc/sphinx/language/extensions/index.rst
@@ -4,7 +4,7 @@
 Language extensions
 ===================
 
-Elaboration extends the language accepted by the |Coq| kernel to make it
+Elaboration extends the language accepted by the Coq kernel to make it
 easier to use.  For example, this lets the user omit most type
 annotations because they can be inferred, call functions with implicit
 arguments which will be inferred as well, extend the syntax with
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 3c1983ee97..23389eba3b 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -5,7 +5,7 @@ Extended pattern matching
 
 :Authors: Cristina Cornes and Hugo Herbelin
 
-This section describes the full form of pattern matching in |Coq| terms.
+This section describes the full form of pattern matching in Coq terms.
 
 .. |rhs| replace:: right hand sides
 
@@ -187,10 +187,10 @@ Printing nested patterns
    pattern matching into a single pattern matching over a nested
    pattern.
 
-   When this flag is on (default), |Coq|’s printer tries to do such
+   When this flag is on (default), Coq’s printer tries to do such
    limited re-factorization.
-   Turning it off tells |Coq| to print only simple pattern matching problems
-   in the same way as the |Coq| kernel handles them.
+   Turning it off tells Coq to print only simple pattern matching problems
+   in the same way as the Coq kernel handles them.
 
 
 Factorization of clauses with same right-hand side
@@ -200,7 +200,7 @@ Factorization of clauses with same right-hand side
 
    When several patterns share the same right-hand side, it is additionally
    possible to share the clauses using disjunctive patterns. Assuming that the
-   printing matching mode is on, this flag (on by default) tells |Coq|'s
+   printing matching mode is on, this flag (on by default) tells Coq's
    printer to try to do this kind of factorization.
 
 Use of a default clause
@@ -212,7 +212,7 @@ Use of a default clause
    arguments of the patterns, yet an extra factorization is possible: the
    disjunction of patterns can be replaced with a `_` default clause. Assuming that
    the printing matching mode and the factorization mode are on, this flag (on by
-   default) tells |Coq|'s printer to use a default clause when relevant.
+   default) tells Coq's printer to use a default clause when relevant.
 
 Printing of wildcard patterns
 ++++++++++++++++++++++++++++++
@@ -234,7 +234,7 @@ Printing of the elimination predicate
    In most of the cases, the type of the result of a matched term is
    mechanically synthesizable. Especially, if the result type does not
    depend of the matched term. When this flag is on (default),
-   the result type is not printed when |Coq| knows that it can re-
+   the result type is not printed when Coq knows that it can re-
    synthesize it.
 
 
@@ -676,7 +676,7 @@ Dependent pattern matching
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The examples given so far do not need an explicit elimination
-predicate because all the |rhs| have the same type and |Coq|
+predicate because all the |rhs| have the same type and Coq
 succeeds to synthesize it. Unfortunately when dealing with dependent
 patterns it often happens that we need to write cases where the types
 of the |rhs| are different instances of the elimination predicate. The