Add some missing smallcaps.

6 files changed, 10 insertions, 10 deletions

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