Add some missing smallcaps.

7 files changed, 23 insertions, 23 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index c2249b8e57..1ca85e7e17 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -16,7 +16,7 @@ Before using any of the commands or options described in this chapter,
 the extraction framework should first be loaded explicitly
 via ``Require Extraction``, or via the more robust
 ``From Coq Require Extraction``.
-Note that in earlier versions of Coq, these commands and options were
+Note that in earlier versions of |Coq|, these commands and options were
 directly available without any preliminary ``Require``.
 
 .. coqtop:: in
@@ -72,10 +72,10 @@ produce one monolithic file or one file per |Coq| library.
    Recursive extraction of all the mentioned objects and all
    their dependencies, just as :n:`Extraction @string {+ @qualid }`,
    but instead of producing one monolithic file, this command splits
-   the produced code in separate ML files, one per corresponding Coq
+   the produced code in separate ML files, one per corresponding |Coq|
    ``.v`` file. This command is hence quite similar to
    :cmd:`Recursive Extraction Library`, except that only the needed
-   parts of Coq libraries are extracted instead of the whole.
+   parts of |Coq| libraries are extracted instead of the whole.
    The naming convention in case of name clash is the same one as
    :cmd:`Extraction Library`: identifiers are here renamed using prefixes
    ``coq_``  or ``Coq_``.
@@ -138,7 +138,7 @@ and commands:
    Default is on. This controls all type-preserving optimizations made on
    the ML terms (mostly reduction of dummy beta/iota redexes, but also
    simplifications on Cases, etc). Turn this flag off if you want a
-   ML term as close as possible to the Coq term.
+   ML term as close as possible to the |Coq| term.
 
 .. flag:: Extraction Conservative Types
 
@@ -434,7 +434,7 @@ Additional settings
 
    Controls which optimizations are used during extraction, providing a finer-grained
    control than :flag:`Extraction Optimize`.  The bits of :token:`natural` are used as a bit mask.
-   Keeping an option off keeps the extracted ML more similar to the Coq term.
+   Keeping an option off keeps the extracted ML more similar to the |Coq| term.
    Values are:
 
    +-----+-------+----------------------------------------------------------------+
@@ -465,7 +465,7 @@ Additional settings
 
 .. flag:: Extraction TypeExpand
 
-   If set, fully expand Coq types in ML.  See the Coq source code to learn more.
+   If set, fully expand |Coq| types in ML.  See the |Coq| source code to learn more.
 
 Differences between |Coq| and ML type systems
 ----------------------------------------------
@@ -515,7 +515,7 @@ In |OCaml|, we must cast any argument of the constructor dummy
 Even with those unsafe castings, you should never get error like
 ``segmentation fault``. In fact even if your program may seem
 ill-typed to the |OCaml| type checker, it can't go wrong : it comes
-from a Coq well-typed terms, so for example inductive types will always 
+from a |Coq| well-typed terms, so for example inductive types will always
 have the correct number of arguments, etc. Of course, when launching
 manually some extracted function, you should apply it to arguments
 of the right shape (from the |Coq| point-of-view).
@@ -524,7 +524,7 @@ More details about the correctness of the extracted programs can be
 found in :cite:`Let02`.
 
 We have to say, though, that in most "realistic" programs, these problems do not
-occur. For example all the programs of Coq library are accepted by the |OCaml|
+occur. For example all the programs of |Coq| library are accepted by the |OCaml|
 type checker without any ``Obj.magic`` (see examples below).
 
 Some examples
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 759f630b85..fdc349e0d8 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -35,7 +35,7 @@ the previous implementation in several ways:
   the new implementation, if one provides the proper morphisms. Again,
   most of the work is handled in the tactics.
 + First-class morphisms and signatures. Signatures and morphisms are
-  ordinary Coq terms, hence they can be manipulated inside Coq, put
+  ordinary |Coq| terms, hence they can be manipulated inside |Coq|, put
   inside structures and lemmas about them can be proved inside the
   system. Higher-order morphisms are also allowed.
 + Performance. The implementation is based on a depth-first search for
@@ -103,7 +103,7 @@ argument.
 Morphisms can also be contravariant in one or more of their arguments.
 A morphism is contravariant on an argument associated to the relation
 instance :math:`R` if it is covariant on the same argument when the inverse
-relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->``
+relation :math:`R^{−1}` (``inverse R`` in |Coq|) is considered. The special arrow ``-->``
 is used in signatures for contravariant morphisms.
 
 Functions having arguments related by symmetric relations instances
@@ -144,7 +144,7 @@ always the intended equality for a given structure.
 
 In the next section we will describe the commands to register terms as
 parametric relations and morphisms. Several tactics that deal with
-equality in Coq can also work with the registered relations. The exact
+equality in |Coq| can also work with the registered relations. The exact
 list of tactics will be given :ref:`in this section <tactics-enabled-on-user-provided-relations>`.
 For instance, the tactic reflexivity can be used to solve a goal ``R n n`` whenever ``R``
 is an instance of a registered reflexive relation. However, the
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index ba5bac6489..d184eafac9 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -260,7 +260,7 @@ proof by abstracting monomials by variables.
    that might miss a refutation.
 
    To illustrate the working of the tactic, consider we wish to prove the
-   following Coq goal:
+   following |Coq| goal:
 
 .. needs csdp
 .. coqdoc::
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index e1b1ee8e8d..35f087d47d 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -9,7 +9,7 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic
 
    The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia`
    tactic.  The goal is to consolidate the arithmetic solving
-   capabilities of Coq into a single engine; moreover, :tacn:`lia` is
+   capabilities of |Coq| into a single engine; moreover, :tacn:`lia` is
    in general more powerful than :tacn:`omega` (it is a complete
    Presburger arithmetic solver while :tacn:`omega` was known to be
    incomplete).
@@ -143,7 +143,7 @@ Options
 
    .. deprecated:: 8.5
 
-   This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It
+   This deprecated flag (on by default) is for compatibility with |Coq| pre 8.5. It
    resets internal name counters to make executions of :tacn:`omega` independent.
 
 .. flag:: Omega UseLocalDefs
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index c6a4b4fe1a..0fd66d07db 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -22,7 +22,7 @@ complete |Coq| term. |Program| replaces the |Program| tactic by Catherine
 Parent :cite:`Parent95b` which had a similar goal but is no longer maintained.
 
 The languages available as input are currently restricted to |Coq|’s
-term language, but may be extended to OCaml, Haskell and
+term language, but may be extended to |OCaml|, Haskell and
 others in the future. We use the same syntax as |Coq| and permit to use
 implicit arguments and the existing coercion mechanism. Input terms
 and types are typed in an extended system (Russell) and interpreted
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index cda8a1b679..9f839364b6 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -99,7 +99,7 @@ Yes, building the variables map and doing the substitution after
 normalizing is automatically done by the tactic. So you can just
 forget this paragraph and use the tactic according to your intuition.
 
-Concrete usage in Coq
+Concrete usage in |Coq|
 --------------------------
 
 .. tacn:: ring {? [ {+ @term } ] }
@@ -433,10 +433,10 @@ How does it work?
 
 The code of ``ring`` is a good example of a tactic written using *reflection*.
 What is reflection? Basically, using it means that a part of a tactic is written
-in Gallina, Coq's language of terms, rather than |Ltac| or |OCaml|. From the
+in Gallina, |Coq|'s language of terms, rather than |Ltac| or |OCaml|. From the
 philosophical point of view, reflection is using the ability of the Calculus of
 Constructions to speak and reason about itself. For the ``ring`` tactic we used
-Coq as a programming language and also as a proof environment to build a tactic
+|Coq| as a programming language and also as a proof environment to build a tactic
 and to prove its correctness.
 
 The interested reader is strongly advised to have a look at the
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index d533470f22..8cbc436ab7 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -13,7 +13,7 @@ Class and Instance declarations
 -------------------------------
 
 The syntax for class and instance declarations is the same as the record
-syntax of Coq:
+syntax of |Coq|:
 
 .. coqdoc::
 
@@ -61,7 +61,7 @@ Note that if you finish the proof with :cmd:`Qed` the entire instance
 will be opaque, including the fields given in the initial term.
 
 Alternatively, in :flag:`Program Mode` if one does not give all the
-members in the Instance declaration, Coq generates obligations for the
+members in the Instance declaration, |Coq| generates obligations for the
 remaining fields, e.g.:
 
 .. coqtop:: in
@@ -242,7 +242,7 @@ binders. For example:
    Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y).
 
 The ``!`` modifier switches the way a binder is parsed back to the usual
-interpretation of Coq. In particular, it uses the implicit arguments
+interpretation of |Coq|. In particular, it uses the implicit arguments
 mechanism if available, as shown in the example.
 
 Substructures
@@ -511,13 +511,13 @@ Settings
    This flag (off by default) respects the dependency order
    between subgoals, meaning that subgoals on which other subgoals depend
    come first, while the non-dependent subgoals were put before
-   the dependent ones previously (Coq 8.5 and below). This can result in
+   the dependent ones previously (|Coq| 8.5 and below). This can result in
    quite different performance behaviors of proof search.
 
 
 .. flag:: Typeclasses Filtered Unification
 
-   This flag, available since Coq 8.6 and off by default, switches the
+   This flag, available since |Coq| 8.6 and off by default, switches the
    hint application procedure to a filter-then-unify strategy. To apply a
    hint, we first check that the goal *matches* syntactically the
    inferred or specified pattern of the hint, and only then try to