Add some missing smallcaps.

9 files changed, 34 insertions, 34 deletions

diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 41e1c30f0d..6cdc272fd4 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 45bdc019ac..3cc3fe231a 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -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)::
 
     ! #[ % & ' ( () ) * + , - ->
     . .( .. ... / : ::= := :> :>> ; < <+ <- <:
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index c034b7f302..0520afd600 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/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 42203d9d65..592b16a72f 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` and
    :attr:`canonical` 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.
@@ -172,7 +172,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 de780db267..c7b1df28db 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 39b154de8d..0b18c9dcf1 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``,
@@ -405,7 +405,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`.
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 866104d5d1..1309a47ff4 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -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
 line options.
diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst
index 48647deeff..17f569ca2a 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. 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:`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 df50dbafe3..c70f7a347b 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`.