Merge PR #11924: Add style for smallcaps.

Reviewed-by: jfehrle

15 files changed, 44 insertions, 44 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`.
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 0ae9fab7ab..29877e1b32 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -377,7 +377,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
@@ -394,7 +394,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`),
@@ -416,7 +416,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:
 
@@ -431,7 +431,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 bfda8befff..38c9fa336d 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
@@ -224,7 +224,7 @@ 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
+pairs of objects. The following construction is telling |Coq| exactly
 how to do that.
 
 .. coqtop:: all
diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
index 20f4310d13..dc208a63a0 100644
--- a/doc/sphinx/language/extensions/evars.rst
+++ b/doc/sphinx/language/extensions/evars.rst
@@ -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 f8375e93ce..9457505feb 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`
diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst
index ed207ca743..ea7271179e 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 c36b9deef3..561262262b 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -639,7 +639,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