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

5 files changed, 148 insertions, 148 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 8663ac646b..1cb83465b6 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -8,7 +8,7 @@ This chapter documents the tactic language |Ltac|.
 We start by giving the syntax followed by the informal
 semantics. To learn more about the language and
 especially about its foundations, please refer to :cite:`Del00`.
-(Note the examples in the paper won't work as-is; |Coq| has evolved
+(Note the examples in the paper won't work as-is; Coq has evolved
 since the paper was written.)
 
 .. example:: Basic tactic macros
@@ -41,7 +41,7 @@ higher precedence than `+`.  Usually `a/b/c` is given the :gdef:`left associativ
 interpretation `(a/b)/c` rather than the :gdef:`right associative` interpretation
 `a/(b/c)`.
 
-In |Coq|, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4`
+In Coq, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4`
 is interpreted as :n:`(try (repeat (@tactic__1 || @tactic__2)); @tactic__3); @tactic__4`
 because `||` is part of :token:`ltac_expr2`, which has higher precedence than
 :tacn:`try` and :tacn:`repeat` (at the level of :token:`ltac_expr3`), which
@@ -784,7 +784,7 @@ single success:
 Checking for a single success: exactly_once
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-|Coq| provides an experimental way to check that a tactic has *exactly
+Coq provides an experimental way to check that a tactic has *exactly
 one* success:
 
 .. tacn:: exactly_once @ltac_expr3
@@ -813,7 +813,7 @@ one* success:
 Checking for failure: assert_fails
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*:
+Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*:
 
 .. tacn:: assert_fails @ltac_expr3
    :name: assert_fails
@@ -859,7 +859,7 @@ Checking for failure: assert_fails
 Checking for success: assert_succeeds
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one*
+Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one*
 success:
 
 .. tacn:: assert_succeeds @ltac_expr3
@@ -905,7 +905,7 @@ Failing
 
    See the example for a comparison of the two constructs.
 
-   Note that if |Coq| terms have to be
+   Note that if Coq terms have to be
    printed as part of the failure, term construction always forces the
    tactic into the goals, meaning that if there are no goals when it is
    evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed.
@@ -990,7 +990,7 @@ amount of time:
       timeout with some other tacticals. This tactical is hence proposed only
       for convenience during debugging or other development phases, we strongly
       advise you to not leave any timeout in final scripts. Note also that
-      this tactical isn’t available on the native Windows port of |Coq|.
+      this tactical isn’t available on the native Windows port of Coq.
 
 Timing a tactic
 ~~~~~~~~~~~~~~~
@@ -1523,7 +1523,7 @@ produce subgoals but generates a term to be used in tactic expressions:
 Generating fresh hypothesis names
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Tactics sometimes need to generate new names for hypothesis.  Letting |Coq|
+Tactics sometimes need to generate new names for hypothesis.  Letting Coq
 choose a name with the intro tactic is not so good since it is
 very awkward to retrieve that name. The following
 expression returns an identifier:
@@ -1885,7 +1885,7 @@ Proving that a list is a permutation of a second list
    From Section :ref:`ltac-syntax` we know that Ltac has a primitive
    notion of integers, but they are only used as arguments for
    primitive tactics and we cannot make computations with them. Thus,
-   instead, we use |Coq|'s natural number type :g:`nat`.
+   instead, we use Coq's natural number type :g:`nat`.
 
    .. coqtop:: in
 
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 41f376c43d..b912bcbdf8 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -4,7 +4,7 @@ Ltac2
 =====
 
 The |Ltac| tactic language is probably one of the ingredients of the success of
-|Coq|, yet it is at the same time its Achilles' heel. Indeed, |Ltac|:
+Coq, yet it is at the same time its Achilles' heel. Indeed, |Ltac|:
 
 - has often unclear semantics
 - is very non-uniform due to organic growth
@@ -30,7 +30,7 @@ as Ltac1.
 Current limitations include:
 
 - There are a number of tactics that are not yet supported in Ltac2 because
-  the interface |OCaml| and/or Ltac2 notations haven't been written.  See
+  the interface OCaml and/or Ltac2 notations haven't been written.  See
   :ref:`defining_tactics`.
 
 - Missing usability features such as:
@@ -89,7 +89,7 @@ In particular, Ltac2 is:
   * together with the Hindley-Milner type system
 
 - a language featuring meta-programming facilities for the manipulation of
-  |Coq|-side terms
+  Coq-side terms
 - a language featuring notation facilities to help write palatable scripts
 
 We describe these in more detail in the remainder of this document.
@@ -107,14 +107,14 @@ that ML constitutes a sweet spot in PL design, as it is relatively expressive
 while not being either too lax (unlike dynamic typing) nor too strict
 (unlike, say, dependent types).
 
-The main goal of Ltac2 is to serve as a meta-language for |Coq|. As such, it
+The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it
 naturally fits in the ML lineage, just as the historical ML was designed as
 the tactic language for the LCF prover. It can also be seen as a general-purpose
-language, by simply forgetting about the |Coq|-specific features.
+language, by simply forgetting about the Coq-specific features.
 
 Sticking to a standard ML type system can be considered somewhat weak for a
-meta-language designed to manipulate |Coq| terms. In particular, there is no
-way to statically guarantee that a |Coq| term resulting from an Ltac2
+meta-language designed to manipulate Coq terms. In particular, there is no
+way to statically guarantee that a Coq term resulting from an Ltac2
 computation will be well-typed. This is actually a design choice, motivated
 by backward compatibility with Ltac1. Instead, well-typedness is deferred to
 dynamic checks, allowing many primitive functions to fail whenever they are
@@ -137,7 +137,7 @@ Type Syntax
 ~~~~~~~~~~~
 
 At the level of terms, we simply elaborate on Ltac1 syntax, which is quite
-close to |OCaml|. Types follow the simply-typed syntax of |OCaml|.
+close to OCaml. Types follow the simply-typed syntax of OCaml.
 
 .. insertprodn ltac2_type ltac2_typevar
 
@@ -159,7 +159,7 @@ declarations such as algebraic datatypes and records.
 
 Built-in types include:
 
-- ``int``, machine integers (size not specified, in practice inherited from |OCaml|)
+- ``int``, machine integers (size not specified, in practice inherited from OCaml)
 - ``string``, mutable strings
 - ``'a array``, mutable arrays
 - ``exn``, exceptions
@@ -200,7 +200,7 @@ One can define new types with the following commands.
      :token:`tac2typ_knd` should be in the form :n:`[ {? {? %| } {+| @tac2alg_constructor } } ]`.
 
    Without :n:`{| := | ::= }`
-     Defines an abstract type for use representing data from |OCaml|.  Not for
+     Defines an abstract type for use representing data from OCaml.  Not for
      end users.
 
    :n:`with @tac2typ_def`
@@ -226,9 +226,9 @@ One can define new types with the following commands.
 .. cmd:: Ltac2 @ external @ident : @ltac2_type := @string @string
    :name: Ltac2 external
 
-   Declares abstract terms.  Frequently, these declare |OCaml| functions
-   defined in |Coq| and give their type information.  They can also declare
-   data structures from |OCaml|.  This command has no use for the end user.
+   Declares abstract terms.  Frequently, these declare OCaml functions
+   defined in Coq and give their type information.  They can also declare
+   data structures from OCaml.  This command has no use for the end user.
 
 APIs
 ~~~~
@@ -360,7 +360,7 @@ Reduction
 ~~~~~~~~~
 
 We use the usual ML call-by-value reduction, with an otherwise unspecified
-evaluation order. This is a design choice making it compatible with |OCaml|,
+evaluation order. This is a design choice making it compatible with OCaml,
 if ever we implement native compilation. The expected equations are as follows::
 
   (fun x => t) V ≡ t{x := V} (βv)
@@ -404,7 +404,7 @@ standard IO monad as the ambient effectful world, Ltac2 is has a
 tactic monad.
 
 Note that the order of evaluation of application is *not* specified and is
-implementation-dependent, as in |OCaml|.
+implementation-dependent, as in OCaml.
 
 We recall that the `Proofview.tactic` monad is essentially a IO monad together
 with backtracking state representing the proof state.
@@ -535,7 +535,7 @@ is a proper one or referring to something in the Ltac context.
 
 Likewise, in Ltac1, constr parsing is implicit, so that ``foo 0`` is
 not ``foo`` applied to the Ltac integer expression ``0`` (|Ltac| does have a
-notion of integers, though it is not first-class), but rather the |Coq| term
+notion of integers, though it is not first-class), but rather the Coq term
 :g:`Datatypes.O`.
 
 The implicit parsing is confusing to users and often gives unexpected results.
@@ -567,11 +567,11 @@ Built-in quotations
 The current implementation recognizes the following built-in quotations:
 
 - ``ident``, which parses identifiers (type ``Init.ident``).
-- ``constr``, which parses |Coq| terms and produces an-evar free term at runtime
+- ``constr``, which parses Coq terms and produces an-evar free term at runtime
   (type ``Init.constr``).
-- ``open_constr``, which parses |Coq| terms and produces a term potentially with
+- ``open_constr``, which parses Coq terms and produces a term potentially with
   holes at runtime (type ``Init.constr`` as well).
-- ``pattern``, which parses |Coq| patterns and produces a pattern used for term
+- ``pattern``, which parses Coq patterns and produces a pattern used for term
   matching (type ``Init.pattern``).
 - ``reference``  Qualified names
   are globalized at internalization into the corresponding global reference,
@@ -614,7 +614,7 @@ Term Antiquotations
 Syntax
 ++++++
 
-One can also insert Ltac2 code into |Coq| terms, similar to what is possible in
+One can also insert Ltac2 code into Coq terms, similar to what is possible in
 Ltac1.
 
 .. prodn::
@@ -626,7 +626,7 @@ for their side-effects.
 Semantics
 +++++++++
 
-A quoted |Coq| term is interpreted in two phases, internalization and
+A quoted Coq term is interpreted in two phases, internalization and
 evaluation.
 
 - Internalization is part of the static semantics, that is, it is done at Ltac2
@@ -634,17 +634,17 @@ evaluation.
 - Evaluation is part of the dynamic semantics, that is, it is done when
   a term gets effectively computed by Ltac2.
 
-Note that typing of |Coq| terms is a *dynamic* process occurring at Ltac2
+Note that typing of Coq terms is a *dynamic* process occurring at Ltac2
 evaluation time, and not at Ltac2 typing time.
 
 Static semantics
 ****************
 
-During internalization, |Coq| variables are resolved and antiquotations are
-type checked as Ltac2 terms, effectively producing a ``glob_constr`` in |Coq|
+During internalization, Coq variables are resolved and antiquotations are
+type checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq
 implementation terminology. Note that although it went through the
 type checking of **Ltac2**, the resulting term has not been fully computed and
-is potentially ill-typed as a runtime **|Coq|** term.
+is potentially ill-typed as a runtime **Coq** term.
 
 .. example::
 
@@ -666,7 +666,7 @@ of the corresponding term expression.
       let x := '0 in constr:(1 + ltac2:(exact x))
 
 Beware that the typing environment of antiquotations is **not**
-expanded by the |Coq| binders from the term.
+expanded by the Coq binders from the term.
 
   .. example::
 
@@ -689,17 +689,17 @@ as follows.
 
 `constr:(fun x : nat => ltac2:(exact (hyp @x)))`
 
-This pattern is so common that we provide dedicated Ltac2 and |Coq| term notations
+This pattern is so common that we provide dedicated Ltac2 and Coq term notations
 for it.
 
 - `&x` as an Ltac2 expression expands to `hyp @x`.
-- `&x` as a |Coq| constr expression expands to
+- `&x` as a Coq constr expression expands to
   `ltac2:(Control.refine (fun () => hyp @x))`.
 
-In the special case where Ltac2 antiquotations appear inside a |Coq| term
+In the special case where Ltac2 antiquotations appear inside a Coq term
 notation, the notation variables are systematically bound in the body
 of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents
-untyped syntactic |Coq| expressions, which can by typed in the
+untyped syntactic Coq expressions, which can by typed in the
 current context using the `Ltac2.Constr.pretype` function.
 
 .. example::
@@ -745,9 +745,9 @@ the notation section.
 
 .. prodn:: term += $@lident
 
-In a |Coq| term, writing :g:`$x` is semantically equivalent to
+In a Coq term, writing :g:`$x` is semantically equivalent to
 :g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to
-insert in a concise way an Ltac2 variable of type :n:`constr` into a |Coq| term.
+insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term.
 
 Match over terms
 ~~~~~~~~~~~~~~~~
@@ -1126,7 +1126,7 @@ Match on values
 .. tacn:: match @ltac2_expr5 with {? @ltac2_branches } end
    :name: match (Ltac2)
 
-   Matches a value, akin to the |OCaml| `match` construct.  By itself, it doesn't cause backtracking
+   Matches a value, akin to the OCaml `match` construct.  By itself, it doesn't cause backtracking
    as do the `*match*!` and `*match*! goal` constructs.
 
    .. insertprodn ltac2_branches atomic_tac2pat
@@ -1186,7 +1186,7 @@ Notations
    into the right-hand side.  The right-hand side is typechecked when the notation is used,
    not when it is defined.  In the following example, `x` is the formal parameter name and
    `constr` is its :ref:`syntactic class<syntactic_classes>`.  `print` and `of_constr` are
-   functions provided by |Coq| through `Message.v`.
+   functions provided by Coq through `Message.v`.
 
    .. todo "print" doesn't seem to pay attention to "Set Printing All"
 
@@ -1258,7 +1258,7 @@ Abbreviations
 
    Introduces a special kind of notation, called an abbreviation,
    that does not add any parsing rules. It is similar in
-   spirit to |Coq| abbreviations (see :cmd:`Notation (abbreviation)`,
+   spirit to Coq abbreviations (see :cmd:`Notation (abbreviation)`,
    insofar as its main purpose is to give an
    absolute name to a piece of pure syntax, which can be transparently referred to
    by this name as if it were a proper definition.
@@ -1285,7 +1285,7 @@ Abbreviations
 Defining tactics
 ~~~~~~~~~~~~~~~~
 
-Built-in tactics (those defined in |OCaml| code in the |Coq| executable) and Ltac1 tactics,
+Built-in tactics (those defined in OCaml code in the Coq executable) and Ltac1 tactics,
 which are defined in `.v` files, must be defined through notations.  (Ltac2 tactics can be
 defined with :cmd:`Ltac2`.
 
@@ -1293,7 +1293,7 @@ Notations for many but not all built-in tactics are defined in `Notations.v`, wh
 loaded with Ltac2.  The Ltac2 syntax for these tactics is often identical or very similar to the
 tactic syntax described in other chapters of this documentation.  These notations rely on tactic functions
 declared in `Std.v`.  Functions corresponding to some built-in tactics may not yet be defined in the
-|Coq| executable or declared in `Std.v`.  Adding them may require code changes to |Coq| or defining
+Coq executable or declared in `Std.v`.  Adding them may require code changes to Coq or defining
 workarounds through Ltac1 (described below).
 
 Two examples of syntax differences:
@@ -1325,7 +1325,7 @@ Syntactic classes
 ~~~~~~~~~~~~~~~~~
 
 The simplest syntactic classes in Ltac2 notations represent individual nonterminals
-from the |Coq| grammar.  Only a few selected nonterminals are available as syntactic classes.
+from the Coq grammar.  Only a few selected nonterminals are available as syntactic classes.
 In addition, there are metasyntactic operations for describing
 more complex syntax, such as making an item optional or representing a list of items.
 When parsing, each syntactic class expression returns a value that's bound to a name in the
@@ -1799,7 +1799,7 @@ Transition from Ltac1
 Owing to the use of a lot of notations, the transition should not be too
 difficult. In particular, it should be possible to do it incrementally. That
 said, we do *not* guarantee it will be a blissful walk either.
-Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with |Coq|
+Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq
 will help you.
 
 We list the major changes and the transition strategies hereafter.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index cdbae8ade1..22544b2018 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -13,12 +13,12 @@ Introduction
 This chapter describes a set of tactics known as |SSR| originally
 designed to provide support for the so-called *small scale reflection*
 proof methodology. Despite the original purpose this set of tactic is
-of general interest and is available in |Coq| starting from version 8.7.
+of general interest and is available in Coq starting from version 8.7.
 
 |SSR| was developed independently of the tactics described in
 Chapter :ref:`tactics`. Indeed the scope of the tactics part of |SSR| largely
 overlaps with the standard set of tactics. Eventually the overlap will
-be reduced in future releases of |Coq|.
+be reduced in future releases of Coq.
 
 Proofs written in |SSR| typically look quite different from the
 ones written using only tactics as per Chapter :ref:`tactics`. We try to
@@ -112,7 +112,7 @@ Compatibility issues
 ~~~~~~~~~~~~~~~~~~~~
 
 Requiring the above modules creates an environment which is mostly
-compatible with the rest of |Coq|, up to a few discrepancies:
+compatible with the rest of Coq, up to a few discrepancies:
 
 
 + New keywords (``is``) might clash with variable, constant, tactic or
@@ -124,11 +124,11 @@ compatible with the rest of |Coq|, up to a few discrepancies:
 + Identifiers with both leading and trailing ``_``, such as ``_x_``, are
   reserved by |SSR| and cannot appear in scripts.
 + The extensions to the :tacn:`rewrite` tactic are partly incompatible with those
-  available in current versions of |Coq|; in particular: ``rewrite .. in
+  available in current versions of Coq; in particular: ``rewrite .. in
   (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite`
   will not work, and the |SSR| syntax and semantics for occurrence selection
   and rule chaining is different. Use an explicit rewrite direction
-  (``rewrite <- …`` or ``rewrite -> …``) to access the |Coq| rewrite tactic.
+  (``rewrite <- …`` or ``rewrite -> …``) to access the Coq rewrite tactic.
 + New symbols (``//``, ``/=``, ``//=``) might clash with adjacent
   existing symbols.
   This can be avoided by inserting white spaces.
@@ -158,34 +158,34 @@ compatible with the rest of |Coq|, up to a few discrepancies:
   generalized form, turn off the |SSR| Boolean ``if`` notation using the command:
   ``Close Scope boolean_if_scope``.
 + The following flags can be unset to make |SSR| more compatible with
-  parts of |Coq|:
+  parts of Coq:
 
 .. flag:: SsrRewrite
 
    Controls whether the incompatible rewrite syntax is enabled (the default).
-   Disabling the flag makes the syntax compatible with other parts of |Coq|.
+   Disabling the flag makes the syntax compatible with other parts of Coq.
 
 .. flag:: SsrIdents
 
    Controls whether tactics can refer to |SSR|-generated variables that are
    in the form _xxx_.  Scripts with explicit references to such variables
    are fragile; they are prone to failure if the proof is later modified or
-   if the details of variable name generation change in future releases of |Coq|.
+   if the details of variable name generation change in future releases of Coq.
 
    The default is on, which gives an error message when the user tries to
    create such identifiers.  Disabling the flag generates a warning instead,
-   increasing compatibility with other parts of |Coq|.
+   increasing compatibility with other parts of Coq.
 
-|Gallina| extensions
+Gallina extensions
 --------------------
 
 Small-scale reflection makes an extensive use of the programming
-subset of |Gallina|, |Coq|’s logical specification language. This subset
+subset of Gallina, Coq’s logical specification language. This subset
 is quite suited to the description of functions on representations,
 because it closely follows the well-established design of the ML
 programming language. The |SSR| extension provides three additions
-to |Gallina|, for pattern assignment, pattern testing, and polymorphism;
-these mitigate minor but annoying discrepancies between |Gallina| and
+to Gallina, for pattern assignment, pattern testing, and polymorphism;
+these mitigate minor but annoying discrepancies between Gallina and
 ML.
 
 
@@ -199,7 +199,7 @@ irrefutable pattern matching, that is, destructuring assignment:
    term += let: @pattern := @term in @term
 
 Note the colon ``:`` after the ``let`` keyword, which avoids any ambiguity
-with a function definition or |Coq|’s basic destructuring let. The let:
+with a function definition or Coq’s basic destructuring let. The let:
 construct differs from the latter in that
 
 
@@ -237,7 +237,7 @@ construct differs from the latter in that
 
 
 The ``let:`` construct is just (more legible) notation for the primitive
-|Gallina| expression :n:`match @term with @pattern => @term end`.
+Gallina expression :n:`match @term with @pattern => @term end`.
 
 The |SSR| destructuring assignment supports all the dependent
 match annotations; the full syntax is
@@ -294,10 +294,10 @@ example, the null and all list function(al)s can be defined as follows:
 
 The pattern conditional also provides a notation for destructuring
 assignment with a refutable pattern, adapted to the pure functional
-setting of |Gallina|, which lacks a ``Match_Failure`` exception.
+setting of Gallina, which lacks a ``Match_Failure`` exception.
 
 Like ``let:`` above, the ``if…is`` construct is just (more legible) notation
-for the primitive |Gallina| expression
+for the primitive Gallina expression
 :n:`match @term with @pattern => @term | _ => @term end`.
 
 Similarly, it will always be displayed as the expansion of this form
@@ -355,15 +355,15 @@ Note that :token:`pattern` eventually binds variables in the third
 Parametric polymorphism
 ~~~~~~~~~~~~~~~~~~~~~~~
 
-Unlike ML, polymorphism in core |Gallina| is explicit: the type
+Unlike ML, polymorphism in core Gallina is explicit: the type
 parameters of polymorphic functions must be declared explicitly, and
-supplied at each point of use. However, |Coq| provides two features to
+supplied at each point of use. However, Coq provides two features to
 suppress redundant parameters:
 
 
 + Sections are used to provide (possibly implicit) parameters for a
   set of definitions.
-+ Implicit arguments declarations are used to tell |Coq| to use type
++ Implicit arguments declarations are used to tell Coq to use type
   inference to deduce some parameters from the context at each point of
   call.
 
@@ -392,11 +392,11 @@ expressions such as
       Definition all_null (s : list T) := all (@null T) s.
 
 Unfortunately, such higher-order expressions are quite frequent in
-representation functions, especially those which use |Coq|'s
+representation functions, especially those which use Coq's
 ``Structures`` to emulate Haskell typeclasses.
 
-Therefore, |SSR| provides a variant of |Coq|’s implicit argument
-declaration, which causes |Coq| to fill in some implicit parameters at
+Therefore, |SSR| provides a variant of Coq’s implicit argument
+declaration, which causes Coq to fill in some implicit parameters at
 each point of use, e.g., the above definition can be written:
 
 .. example::
@@ -432,7 +432,7 @@ The syntax of the new declaration is
 
    As these prenex implicit arguments are ubiquitous and have often large
    display strings, it is strongly recommended to change the default
-   display settings of |Coq| so that they are not printed (except after
+   display settings of Coq so that they are not printed (except after
    a ``Set Printing All`` command). All |SSR| library files thus start
    with the incantation
 
@@ -957,7 +957,7 @@ context. This is essential in the context of an interactive
 development environment (IDE), because it facilitates navigating the
 proof, allowing to instantly "jump back" to the point at which a
 questionable assumption was added, and to find relevant assumptions by
-browsing the pruned context. While novice or casual |Coq| users may find
+browsing the pruned context. While novice or casual Coq users may find
 the automatic name selection feature convenient, the usage of such a
 feature severely undermines the readability and maintainability of
 proof scripts, much like automatic variable declaration in programming
@@ -973,7 +973,7 @@ the foundation of the |SSR| proof language.
 Bookkeeping
 ~~~~~~~~~~~
 
-During the course of a proof |Coq| always present the user with a
+During the course of a proof Coq always present the user with a
 *sequent* whose general form is::
 
   ci : Ti
@@ -1015,7 +1015,7 @@ are *ordered*, but *unnamed*: the display names of variables may
 change at any time because of α-conversion.
 
 Similarly, basic deductive steps such as apply can only operate on the
-goal because the |Gallina| terms that control their action (e.g., the
+goal because the Gallina terms that control their action (e.g., the
 type of the lemma used by ``apply``) only provide unnamed bound variables.
 [#2]_ Since the proof script can only refer directly to the context, it
 must constantly shift declarations from the goal to the context and
@@ -1083,7 +1083,7 @@ simultaneously renames ``m`` and ``le_m_n`` into ``p`` and ``le_n_p``,
 respectively, by first turning them into unnamed variables, then
 turning these variables back into constants and facts.
 
-Furthermore, |SSR| redefines the basic |Coq| tactics ``case``, ``elim``,
+Furthermore, |SSR| redefines the basic Coq tactics ``case``, ``elim``,
 and ``apply`` so that they can take better advantage of
 ``:`` and ``=>``. In there
 |SSR| variants, these tactic operate on the first variable or
@@ -1421,7 +1421,7 @@ Therefore this tactic changes any goal ``G`` into
 
    forall n n0 : nat, n = n0 -> G.
 
-where the name ``n0`` is picked by the |Coq| display function, and assuming
+where the name ``n0`` is picked by the Coq display function, and assuming
 ``n`` appeared only in ``G``.
 
 Finally, note that a discharge operation generalizes defined constants
@@ -1927,7 +1927,7 @@ When the top assumption of a goal has an inductive type, two specific
 operations are possible: the case analysis performed by the :tacn:`case`
 tactic, and the application of an induction principle, performed by
 the :tacn:`elim` tactic. When this top assumption has an inductive type, which
-is moreover an instance of a type family, |Coq| may need help from the
+is moreover an instance of a type family, Coq may need help from the
 user to specify which occurrences of the parameters of the type should
 be substituted.
 
@@ -2055,7 +2055,7 @@ Control flow
 Indentation and bullets
 ~~~~~~~~~~~~~~~~~~~~~~~
 
-A linear development of |Coq| scripts gives little information on the
+A linear development of Coq scripts gives little information on the
 structure of the proof. In addition, replaying a proof after some
 changes in the statement to be proved will usually not display
 information to distinguish between the various branches of case
@@ -3391,7 +3391,7 @@ rewrite operations prescribed by the rules on the current goal.
 
   Indeed rule ``eqab`` is the first to apply among the ones
   gathered in the tuple passed to the rewrite tactic. This multirule
-  ``(eqab, eqac)`` is actually a |Coq| term and we can name it with a
+  ``(eqab, eqac)`` is actually a Coq term and we can name it with a
   definition:
 
   .. coqtop:: all
@@ -3529,11 +3529,11 @@ Anyway this tactic is *not* equivalent to
   lemma that was used, while the latter requires you prove the quantified
   form.
 
-When |SSR| rewrite fails on standard |Coq| licit rewrite
+When |SSR| rewrite fails on standard Coq licit rewrite
 ````````````````````````````````````````````````````````
 
 In a few cases, the |SSR| rewrite tactic fails rewriting some
-redexes which standard |Coq| successfully rewrites. There are two main
+redexes which standard Coq successfully rewrites. There are two main
 cases:
 
 
@@ -3550,7 +3550,7 @@ cases:
 
      Lemma fubar (x : unit) : (let u := x in u) = tt.
 
-+ The standard rewrite tactic provided by |Coq| uses a different algorithm
++ The standard rewrite tactic provided by Coq uses a different algorithm
   to find instances of the rewrite rule.
 
   .. example::
@@ -3953,7 +3953,7 @@ together with “term tagging” operations.
 
 The first one uses auxiliary definitions to introduce a provably equal
 copy of any term t. However this copy is (on purpose) *not
-convertible* to t in the |Coq| system [#8]_. The job is done by the
+convertible* to t in the Coq system [#8]_. The job is done by the
 following construction:
 
 .. coqdoc::
@@ -4542,7 +4542,7 @@ is a synonym for:
    elim x using V; clear x; intro y.
 
 where ``x`` is a variable in the context, ``y`` a fresh name and ``V``
-any second order lemma; |SSR| relaxes the syntactic restrictions of the |Coq|
+any second order lemma; |SSR| relaxes the syntactic restrictions of the Coq
 ``elim``. The first pattern following ``:`` can be a ``_`` wildcard if the
 conclusion of the view ``V`` specifies a pattern for its last argument
 (e.g., if ``V`` is a functional induction lemma generated by the
@@ -4590,7 +4590,7 @@ generation (see section :ref:`generation_of_equations_ssr`).
      elim/last_ind_list E : l=> [| u v]; last first.
 
 
-User-provided eliminators (potentially generated with |Coq|’s ``Function``
+User-provided eliminators (potentially generated with Coq’s ``Function``
 command) can be combined with the type family switches described
 in section :ref:`type_families_ssr`.
 Consider an eliminator ``foo_ind`` of type:
@@ -4982,8 +4982,8 @@ distinction between logical propositions and boolean values. On the
 one hand, logical propositions are objects of *sort* ``Prop`` which is
 the carrier of intuitionistic reasoning. Logical connectives in
 ``Prop`` are *types*, which give precise information on the structure
-of their proofs; this information is automatically exploited by |Coq|
-tactics.  For example, |Coq| knows that a proof of ``A \/ B`` is
+of their proofs; this information is automatically exploited by Coq
+tactics.  For example, Coq knows that a proof of ``A \/ B`` is
 either a proof of ``A`` or a proof of ``B``.  The tactics ``left`` and
 ``right`` change the goal ``A \/ B`` to ``A`` and ``B``, respectively;
 dually, the tactic ``case`` reduces the goal ``A \/ B => G`` to two
@@ -5042,7 +5042,7 @@ mechanism:
 
    Coercion is_true (b : bool) := b = true.
 
-This allows any boolean formula ``b`` to be used in a context where |Coq|
+This allows any boolean formula ``b`` to be used in a context where Coq
 would expect a proposition, e.g., after ``Lemma … :``. It is then
 interpreted as ``(is_true b)``, i.e., the proposition ``b = true``. Coercions
 are elided by the pretty-printer, so they are essentially transparent
@@ -5077,9 +5077,9 @@ proposition ``b1 /\ b2`` hides two coercions. The conjunction of
 
 Expressing logical equivalences through this family of inductive types
 makes possible to take benefit from *rewritable equations* associated
-to the case analysis of |Coq|’s inductive types.
+to the case analysis of Coq’s inductive types.
 
-Since the equivalence predicate is defined in |Coq| as:
+Since the equivalence predicate is defined in Coq as:
 
 .. coqdoc::
 
@@ -5573,7 +5573,7 @@ Natural number
 
 .. prodn:: nat_or_ident ::= {| @natural | @ident }
 
-where :token:`ident` is an Ltac variable denoting a standard |Coq| number
+where :token:`ident` is an Ltac variable denoting a standard Coq number
 (should not be the name of a tactic which can be followed by a
 bracket ``[``, like ``do``, ``have``,…)
 
@@ -5823,6 +5823,6 @@ Settings
 .. [#8] This is an implementation feature: there is no such obstruction
   in the metatheory
 .. [#9] The current state of the proof shall be displayed by the Show
-  Proof command of |Coq| proof mode.
+  Proof command of Coq proof mode.
 .. [#10] A simple proof context entry is a naked identifier (i.e. not between
   parentheses) designating a context entry that is not a section variable.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index c665026500..26a56005c1 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -167,11 +167,11 @@ The :n:`eqn:` construct in various tactics uses :n:`@naming_intropattern`.
 Use these elementary patterns to specify a name:
 
 * :n:`@ident` — use the specified name
-* :n:`?` — let |Coq| choose a name
+* :n:`?` — let Coq choose a name
 * :n:`?@ident` — generate a name that begins with :n:`@ident`
 * :n:`_` — discard the matched part (unless it is required for another
   hypothesis)
-* if a disjunction pattern omits a name, such as :g:`[|H2]`, |Coq| will choose a name
+* if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name
 
 **Splitting patterns**
 
@@ -268,7 +268,7 @@ These patterns can be used when the hypothesis is an equality:
 
    For :n:`intros @intropattern_list`, controls how to handle a
    conjunctive pattern that doesn't give enough simple patterns to match
-   all the arguments in the constructor.  If set (the default), |Coq| generates
+   all the arguments in the constructor.  If set (the default), Coq generates
    additional names to match the number of arguments.
    Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more
    similar to |SSR|'s intro patterns.
@@ -843,7 +843,7 @@ Applying theorems
 
 .. flag:: Universal Lemma Under Conjunction
 
-   This flag, which preserves compatibility with versions of |Coq| prior to
+   This flag, which preserves compatibility with versions of Coq prior to
    8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply … in`).
 
 .. tacn:: apply @term in @ident
@@ -1293,7 +1293,7 @@ Managing the local context
    .. tacv:: set @term {? in @goal_occurrences }
 
       This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }`
-      but :token:`ident` is generated by |Coq|.
+      but :token:`ident` is generated by Coq.
 
    .. tacv:: eset (@ident {* @binder } := @term) {? in @goal_occurrences }
              eset @term {? in @goal_occurrences }
@@ -1338,7 +1338,7 @@ Managing the local context
    .. tacv:: pose @term
 
       This behaves as :n:`pose (@ident := @term)` but :token:`ident` is
-      generated by |Coq|.
+      generated by Coq.
 
    .. tacv:: epose (@ident {* @binder } := @term)
              epose @term
@@ -1400,7 +1400,7 @@ Controlling the proof flow
    .. tacv:: assert @type
 
       This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is
-      generated by |Coq|.
+      generated by Coq.
 
    .. tacv:: assert @type by @tactic
 
@@ -1480,7 +1480,7 @@ Controlling the proof flow
 .. tacv:: enough @type
 
    This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of
-   the hypothesis generated by |Coq|.
+   the hypothesis generated by Coq.
 
 .. tacv:: enough @type as @simple_intropattern
 
@@ -1605,7 +1605,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
              must have given the name explicitly (see :ref:`Existential-Variables`).
 
    .. note:: When you are referring to hypotheses which you did not name
-             explicitly, be aware that |Coq| may make a different decision on how to
+             explicitly, be aware that Coq may make a different decision on how to
              name the variable in the current goal and in the context of the
              existential variable. This can lead to surprising behaviors.
 
@@ -1759,7 +1759,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       between :token:`term` and the value that it takes in each of the
       possible cases. The name of the equation is specified
       by :token:`naming_intropattern` (see :tacn:`intros`),
-      in particular ``?`` can be used to let |Coq| generate a fresh name.
+      in particular ``?`` can be used to let Coq generate a fresh name.
 
    .. tacv:: destruct @term with @bindings
 
@@ -2353,7 +2353,7 @@ and an explanation of the underlying technique.
    ``inversion`` generally behaves in a slightly more expectable way than
    ``inversion`` (no artificial duplication of some hypotheses referring to
    other hypotheses). To take benefit of these improvements, it is enough to use
-   ``inversion ... as []``, letting the names being finally chosen by |Coq|.
+   ``inversion ... as []``, letting the names being finally chosen by Coq.
 
    .. example::
 
@@ -2912,14 +2912,14 @@ Proof maintenance
 
 *Experimental.*  Many tactics, such as :tacn:`intros`, can automatically generate names, such
 as "H0" or "H1" for a new hypothesis introduced from a goal.  Subsequent proof steps
-may explicitly refer to these names.  However, future versions of |Coq| may not assign
+may explicitly refer to these names.  However, future versions of Coq may not assign
 names exactly the same way, which could cause the proof to fail because the
 new names don't match the explicit references in the proof.
 
 The following "Mangle Names" settings let users find all the
 places where proofs rely on automatically generated names, which can
 then be named explicitly to avoid any incompatibility.  These
-settings cause |Coq| to generate different names, producing errors for
+settings cause Coq to generate different names, producing errors for
 references to automatically generated names.
 
 .. flag:: Mangle Names
@@ -2941,7 +2941,7 @@ Performance-oriented tactic variants
    For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization,
    it skips checking that :n:`@term` is convertible to the goal.
 
-   Recall that the |Coq| kernel typechecks proofs again when they are concluded to
+   Recall that the Coq kernel typechecks proofs again when they are concluded to
    ensure safety. Hence, using :tacn:`change` checks convertibility twice
    overall, while :tacn:`change_no_check` can produce ill-typed terms,
    but checks convertibility only once.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index dd0b12f8ec..36c722bf9b 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -433,7 +433,7 @@ Requests to the environment
       reference ::= @qualid
       | @string {? % @scope_key }
 
-   Displays the full name of objects from |Coq|'s various qualified namespaces such as terms,
+   Displays the full name of objects from Coq's various qualified namespaces such as terms,
    modules and Ltac, thereby showing the module they are defined in.  It also displays notation definitions.
 
    :n:`@qualid`
@@ -491,7 +491,7 @@ Printing flags
 
 .. flag:: Fast Name Printing
 
-   When turned on, |Coq| uses an asymptotically faster algorithm for the
+   When turned on, Coq uses an asymptotically faster algorithm for the
    generation of unambiguous names of bound variables while printing terms.
    While faster, it is also less clever and results in a typically less elegant
    display, e.g. it will generate more names rather than reusing certain names
@@ -504,12 +504,12 @@ Printing flags
 Loading files
 -----------------
 
-|Coq| offers the possibility of loading different parts of a whole
+Coq offers the possibility of loading different parts of a whole
 development stored in separate files. Their contents will be loaded as
 if they were entered from the keyboard. This means that the loaded
-files are text files containing sequences of commands for |Coq|’s
-toplevel. This kind of file is called a *script* for |Coq|. The standard
-(and default) extension of |Coq|’s script files is .v.
+files are text files containing sequences of commands for Coq’s
+toplevel. This kind of file is called a *script* for Coq. The standard
+(and default) extension of Coq’s script files is .v.
 
 
 .. cmd:: Load {? Verbose } {| @string | @ident }
@@ -521,7 +521,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
 
    If :n:`@string` is specified, it must specify a complete filename.
    `~` and .. abbreviations are
-   allowed as well as shell variables. If no extension is specified, |Coq|
+   allowed as well as shell variables. If no extension is specified, Coq
    will use the default extension ``.v``.
 
    Files loaded this way can't leave proofs open, nor can :cmd:`Load`
@@ -531,7 +531,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
    :cmd:`Require` loads `.vo` files that were previously
    compiled from `.v` files.
 
-   :n:`Verbose` displays the |Coq| output for each command and tactic
+   :n:`Verbose` displays the Coq output for each command and tactic
    in the loaded file, as if the commands and tactics were entered interactively.
 
    .. exn:: Can’t find file @ident on loadpath.
@@ -556,14 +556,14 @@ file is a particular case of a module called a *library file*.
 .. cmd:: Require {? {| Import | Export } } {+ @qualid }
    :name: Require; Require Import; Require Export
 
-   Loads compiled modules into the |Coq| environment.  For each :n:`@qualid`, which has the form
+   Loads compiled modules into the Coq environment.  For each :n:`@qualid`, which has the form
    :n:`{* @ident__prefix . } @ident`, the command searches for the logical name represented
    by the :n:`@ident__prefix`\s and loads the compiled file :n:`@ident.vo` from the associated
    filesystem directory.
 
    The process is applied recursively to all the loaded files;
    if they contain :cmd:`Require` commands, those commands are executed as well.
-   The compiled files must have been compiled with the same version of |Coq|.
+   The compiled files must have been compiled with the same version of Coq.
    The compiled files are neither replayed nor rechecked.
 
    * :n:`Import` - additionally does an :cmd:`Import` on the loaded module, making components defined
@@ -606,15 +606,15 @@ file is a particular case of a module called a *library file*.
 
       The command tried to load library file :n:`@ident`.vo that
       depends on some specific version of library :n:`@qualid` which is not the
-      one already loaded in the current |Coq| session. Probably :n:`@ident.v` was
+      one already loaded in the current Coq session. Probably :n:`@ident.v` was
       not properly recompiled with the last version of the file containing
       module :token:`qualid`.
 
    .. exn:: Bad magic number.
 
       The file :n:`@ident.vo` was found but either it is not a
-      |Coq| compiled module, or it was compiled with an incompatible
-      version of |Coq|.
+      Coq compiled module, or it was compiled with an incompatible
+      version of Coq.
 
    .. exn:: The file @ident.vo contains library @qualid__1 and not library @qualid__2.
 
@@ -633,14 +633,14 @@ file is a particular case of a module called a *library file*.
 .. cmd:: Print Libraries
 
    This command displays the list of library files loaded in the
-   current |Coq| session.
+   current Coq session.
 
 .. cmd:: Declare ML Module {+ @string }
 
-   This commands dynamically loads |OCaml| compiled code from
+   This commands dynamically loads OCaml compiled code from
    a :n:`.mllib` file.
    It is used to load plugins dynamically.  The
-   files must be accessible in the current |OCaml| loadpath (see the
+   files must be accessible in the current OCaml loadpath (see the
    command :cmd:`Add ML Path`).  The :n:`.mllib` suffix may be omitted.
 
    This command is reserved for plugin developers, who should provide
@@ -656,7 +656,7 @@ file is a particular case of a module called a *library file*.
 
 .. cmd:: Print ML Modules
 
-   This prints the name of all |OCaml| modules loaded with :cmd:`Declare ML Module`.
+   This prints the name of all OCaml modules loaded with :cmd:`Declare ML Module`.
    To know from where these module were loaded, the user
    should use the command :cmd:`Locate File`.
 
@@ -666,7 +666,7 @@ file is a particular case of a module called a *library file*.
 Loadpath
 ------------
 
-Loadpaths are preferably managed using |Coq| command line options (see
+Loadpaths are preferably managed using Coq command line options (see
 Section :ref:`libraries-and-filesystem`) but there remain vernacular commands to manage them
 for practical purposes. Such commands are only meant to be issued in
 the toplevel, and using them in source files is discouraged.
@@ -703,29 +703,29 @@ the toplevel, and using them in source files is discouraged.
 
    This command is equivalent to the command line option
    :n:`-R @string @dirpath`. It adds the physical directory string and all its
-   subdirectories to the current |Coq| loadpath.
+   subdirectories to the current Coq loadpath.
 
 
 .. cmd:: Remove LoadPath @string
 
-   This command removes the path :n:`@string` from the current |Coq| loadpath.
+   This command removes the path :n:`@string` from the current Coq loadpath.
 
 
 .. cmd:: Print LoadPath {? @dirpath }
 
-   This command displays the current |Coq| loadpath.  If :n:`@dirpath` is specified,
+   This command displays the current Coq loadpath.  If :n:`@dirpath` is specified,
    displays only the paths that extend that prefix.
 
 
 .. cmd:: Add ML Path @string
 
-   This command adds the path :n:`@string` to the current |OCaml|
+   This command adds the path :n:`@string` to the current OCaml
    loadpath (cf. :cmd:`Declare ML Module`).
 
 
 .. cmd:: Print ML Path
 
-   This command displays the current |OCaml| loadpath. This
+   This command displays the current OCaml loadpath. This
    command makes sense only under the bytecode version of ``coqtop``, i.e.
    using option ``-byte``
    (cf. :cmd:`Declare ML Module`).
@@ -789,25 +789,25 @@ Quitting and debugging
 
 .. cmd:: Quit
 
-   Causes |Coq| to exit.  Valid only in coqtop.
+   Causes Coq to exit.  Valid only in coqtop.
 
 
 .. cmd:: Drop
 
-   This command temporarily enters the |OCaml| toplevel.
-   It is a debug facility used by |Coq|’s implementers.  Valid only in the
+   This command temporarily enters the OCaml toplevel.
+   It is a debug facility used by Coq’s implementers.  Valid only in the
    bytecode version of coqtop.
-   The |OCaml| command:
+   The OCaml command:
 
    ::
 
       #use "include";;
 
    adds the right loadpaths and loads some toplevel printers for all
-   abstract types of |Coq|- section_path, identifiers, terms, judgments, ….
+   abstract types of Coq- section_path, identifiers, terms, judgments, ….
    You can also use the file base_include instead, that loads only the
    pretty-printers for section_paths and identifiers. You can return back
-   to |Coq| with the command:
+   to Coq with the command:
 
    ::
 
@@ -815,9 +815,9 @@ Quitting and debugging
 
    .. warning::
 
-      #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`,
+      #. It only works with the bytecode version of Coq (i.e. `coqtop.byte`,
          see Section `interactive-use`).
-      #. You must have compiled |Coq| from the source package and set the
+      #. You must have compiled Coq from the source package and set the
          environment variable COQTOP to the root of your copy of the sources
          (see Section `customization-by-environment-variables`).
 
@@ -961,7 +961,7 @@ Controlling the reduction strategies and the conversion algorithm
 ----------------------------------------------------------------------
 
 
-|Coq| provides reduction strategies that the tactics can invoke and two
+Coq provides reduction strategies that the tactics can invoke and two
 different algorithms to check the convertibility of types. The first
 conversion algorithm lazily compares applicative terms while the other
 is a brute-force but efficient algorithm that first normalizes the
@@ -985,8 +985,8 @@ described first.
    constants in the :n:`@reference` sequence in tactics using δ-conversion (unfolding
    a constant is replacing it by its definition).
 
-   :cmd:`Opaque` has also an effect on the conversion algorithm of |Coq|, telling
-   it to delay the unfolding of a constant as much as possible when |Coq|
+   :cmd:`Opaque` has also an effect on the conversion algorithm of Coq, telling
+   it to delay the unfolding of a constant as much as possible when Coq
    has to check the conversion (see Section :ref:`conversion-rules`) of two distinct
    applied constants.
 
@@ -1222,15 +1222,15 @@ in support libraries of plug-ins.
 
 .. _exposing-constants-to-ocaml-libraries:
 
-Exposing constants to |OCaml| libraries
+Exposing constants to OCaml libraries
 ```````````````````````````````````````
 
 .. cmd:: Register @qualid__1 as @qualid__2
 
-   Makes the constant :n:`@qualid__1` accessible to |OCaml| libraries under
+   Makes the constant :n:`@qualid__1` accessible to OCaml libraries under
    the name :n:`@qualid__2`.  The constant can then be dynamically located
-   in |OCaml| code by
-   calling :n:`Coqlib.lib_ref "@qualid__2"`.  The |OCaml| code doesn't need
+   in OCaml code by
+   calling :n:`Coqlib.lib_ref "@qualid__2"`.  The OCaml code doesn't need
    to know where the constant is defined (what file, module, library, etc.).
 
    As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`,
@@ -1259,9 +1259,9 @@ Registering primitive operations
 
 .. cmd:: Primitive @ident_decl {? : @term } := #@ident
 
-   Makes the primitive type or primitive operator :n:`#@ident` defined in |OCaml|
-   accessible in |Coq| commands and tactics.
-   For internal use by implementors of |Coq|'s standard library or standard library
+   Makes the primitive type or primitive operator :n:`#@ident` defined in OCaml
+   accessible in Coq commands and tactics.
+   For internal use by implementors of Coq's standard library or standard library
    replacements.  No space is allowed after the `#`.  Invalid values give a syntax
    error.