Add some missing smallcaps.

2 files changed, 30 insertions, 30 deletions

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 8e23e61018..19c7c659e0 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -128,7 +128,7 @@ Automatic declaration of schemes
 
 .. warning::
 
-   You have to be careful with these flags since Coq may now reject well-defined
+   You have to be careful with these flags since |Coq| may now reject well-defined
    inductive types because it cannot compute a Boolean equality for them.
 
 .. flag:: Rewriting Schemes
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index d6db305300..1791c53aa8 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -3,7 +3,7 @@
 Syntax extensions and notation scopes
 =====================================
 
-In this chapter, we introduce advanced commands to modify the way Coq
+In this chapter, we introduce advanced commands to modify the way |Coq|
 parses and prints objects, i.e. the translations between the concrete
 and internal representations of terms and commands.
 
@@ -71,7 +71,7 @@ least 3 characters and starting with a simple quote must be quoted
    Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3).
 
 A notation binds a syntactic expression to a term. Unless the parser
-and pretty-printer of Coq already know how to deal with the syntactic
+and pretty-printer of |Coq| already know how to deal with the syntactic
 expression (such as through :cmd:`Reserved Notation` or for notations
 that contain only literals), explicit precedences and
 associativity rules have to be given.
@@ -88,7 +88,7 @@ Precedences and associativity
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Mixing different symbolic notations in the same text may cause serious
-parsing ambiguity. To deal with the ambiguity of notations, Coq uses
+parsing ambiguity. To deal with the ambiguity of notations, |Coq| uses
 precedence levels ranging from 0 to 100 (plus one extra level numbered
 200) and associativity rules.
 
@@ -99,7 +99,7 @@ Consider for example the new notation
    Notation "A \/ B" := (or A B).
 
 Clearly, an expression such as :g:`forall A:Prop, True /\ A \/ A \/ False`
-is ambiguous. To tell the Coq parser how to interpret the
+is ambiguous. To tell the |Coq| parser how to interpret the
 expression, a priority between the symbols ``/\`` and ``\/`` has to be
 given. Assume for instance that we want conjunction to bind more than
 disjunction. This is expressed by assigning a precedence level to each
@@ -117,7 +117,7 @@ defaults to :g:`True /\ (False /\ False)` (right associativity) or to
 expression is not well-formed and that parentheses are mandatory (this is a “no
 associativity”) [#no_associativity]_. We do not know of a special convention for
 the associativity of disjunction and conjunction, so let us apply
-right associativity (which is the choice of Coq).
+right associativity (which is the choice of |Coq|).
 
 Precedence levels and associativity rules of notations are specified with a list of
 parenthesized :n:`@syntax_modifier`\s.  Here is how the previous examples refine:
@@ -187,7 +187,7 @@ left. See the next section for more about factorization.
 Simple factorization rules
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Coq extensible parsing is performed by *Camlp5* which is essentially a LL1
+|Coq| extensible parsing is performed by *Camlp5* which is essentially a LL1
 parser: it decides which notation to parse by looking at tokens from left to right.
 Hence, some care has to be taken not to hide already existing rules by new
 rules. Some simple left factorization work has to be done. Here is an example.
@@ -209,16 +209,16 @@ need to force the parsing level of ``y``, as follows.
    Notation "x < y" := (lt x y) (at level 70).
    Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level).
 
-For the sake of factorization with Coq predefined rules, simple rules
+For the sake of factorization with |Coq| predefined rules, simple rules
 have to be observed for notations starting with a symbol, e.g., rules
 starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list
-of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`.
+of |Coq| predefined notations can be found in the chapter on :ref:`thecoqlibrary`.
 
 Displaying symbolic notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The command :cmd:`Notation` has an effect both on the Coq parser and on the
-Coq printer. For example:
+The command :cmd:`Notation` has an effect both on the |Coq| parser and on the
+|Coq| printer. For example:
 
 .. coqtop:: all
 
@@ -226,7 +226,7 @@ Coq printer. For example:
 
 However, printing, especially pretty-printing, also requires some
 care. We may want specific indentations, line breaks, alignment if on
-several lines, etc. For pretty-printing, |Coq| relies on |ocaml|
+several lines, etc. For pretty-printing, |Coq| relies on |OCaml|
 formatting library, which provides indentation and automatic line
 breaks depending on page width by means of *formatting boxes*.
 
@@ -349,12 +349,12 @@ Reserving notations
 
 .. cmd:: Reserved Notation @string {? ( {+, @syntax_modifier } ) }
 
-   A given notation may be used in different contexts. Coq expects all
+   A given notation may be used in different contexts. |Coq| expects all
    uses of the notation to be defined at the same precedence and with the
    same associativity. To avoid giving the precedence and associativity
    every time, this command declares a parsing rule (:token:`string`) in advance
    without giving its interpretation. Here is an example from the initial
-   state of Coq.
+   state of |Coq|.
 
    .. coqtop:: in
 
@@ -762,7 +762,7 @@ recursive patterns. The basic example is:
    Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
 
 On the right-hand side, an extra construction of the form ``.. t ..`` can
-be used. Notice that ``..`` is part of the Coq syntax and it must not be
+be used. Notice that ``..`` is part of the |Coq| syntax and it must not be
 confused with the three-dots notation “``…``” used in this manual to denote
 a sequence of arbitrary size.
 
@@ -942,7 +942,7 @@ Custom entries
 Custom entries have levels, like the main grammar of terms and grammar
 of patterns have. The lower level is 0 and this is the level used by
 default to put rules delimited with tokens on both ends. The level is
-left to be inferred by Coq when using :n:`in custom @ident`. The
+left to be inferred by |Coq| when using :n:`in custom @ident`. The
 level is otherwise given explicitly by using the syntax
 :n:`in custom @ident at level @natural`, where :n:`@natural` refers to the level.
 
@@ -996,7 +996,7 @@ associated to the custom entry ``expr``. The level can be omitted, as in
 
    Notation "[ e ]" := e (e custom expr).
 
-in which case Coq infer it. If the sub-expression is at a border of
+in which case |Coq| infer it. If the sub-expression is at a border of
 the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is
 determined by the associativity. If the sub-expression is not at the
 border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is
@@ -1097,7 +1097,7 @@ Here are the syntax elements used by the various notation commands.
           time. Type checking is done only at the time of use of the notation.
 
 .. note:: Some examples of Notation may be found in the files composing
-          the initial state of Coq (see directory :file:`$COQLIB/theories/Init`).
+          the initial state of |Coq| (see directory :file:`$COQLIB/theories/Init`).
 
 .. note:: The notation ``"{ x }"`` has a special status in the main grammars of
           terms and patterns so that
@@ -1122,7 +1122,7 @@ Here are the syntax elements used by the various notation commands.
           .. warn:: Use of @string Notation is deprecated as it is inconsistent with pattern syntax.
 
              This warning is disabled by default to avoid spurious diagnostics
-             due to legacy notation in the Coq standard library.
+             due to legacy notation in the |Coq| standard library.
              It can be turned on with the ``-w disj-pattern-notation`` flag.
 
 .. _Scopes:
@@ -1156,7 +1156,7 @@ Most commands use :token:`scope_name`; :token:`scope_key`\s are used within :tok
 .. cmd:: Declare Scope @scope_name
 
    Declares a new notation scope. Note that the initial
-   state of Coq declares the following notation scopes:
+   state of |Coq| declares the following notation scopes:
    ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``,
    ``bool_scope``, ``list_scope``, ``int_scope``, ``uint_scope``.
 
@@ -1308,10 +1308,10 @@ recognized to be a ``Funclass`` instance, i.e., of type :g:`forall x:A, B` or
 
 .. _notation-scopes:
 
-Notation scopes used in the standard library of Coq
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Notation scopes used in the standard library of |Coq|
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-We give an overview of the scopes used in the standard library of Coq.
+We give an overview of the scopes used in the standard library of |Coq|.
 For a complete list of notations in each scope, use the commands :cmd:`Print
 Scopes` or :cmd:`Print Scope`.
 
@@ -1377,7 +1377,7 @@ Scopes` or :cmd:`Print Scope`.
 
 ``string_scope``
   This scope includes notation for strings as elements of the type string.
-  Special characters and escaping follow Coq conventions on strings (see
+  Special characters and escaping follow |Coq| conventions on strings (see
   :ref:`lexical-conventions`). Especially, there is no convention to visualize non
   printable characters of a string. The file :file:`String.v` shows an example
   that contains quotes, a newline and a beep (i.e. the ASCII character
@@ -1478,7 +1478,7 @@ Abbreviations
 
    An abbreviation expects no precedence nor associativity, since it
    is parsed as an usual application. Abbreviations are used as
-   much as possible by the Coq printers unless the modifier ``(only
+   much as possible by the |Coq| printers unless the modifier ``(only
    parsing)`` is given.
 
    An abbreviation is bound to an absolute name as an ordinary definition is
@@ -1634,7 +1634,7 @@ Number notations
             with :n:`(abstract after @bignat)`, this warning is emitted when
             parsing a number greater than or equal to :token:`bignat`.
             Typically, this indicates that the fully computed representation
-            of numbers can be so large that non-tail-recursive OCaml
+            of numbers can be so large that non-tail-recursive |OCaml|
             functions run out of stack space when trying to walk them.
 
          .. warn:: The 'abstract after' directive has no effect when the parsing function (@qualid__parse) targets an option type.
@@ -1978,9 +1978,9 @@ Tactic notations allow customizing the syntax of tactics.
 .. rubric:: Footnotes
 
 .. [#and_or_levels] which are the levels effectively chosen in the current
-   implementation of Coq
+   implementation of |Coq|
 
-.. [#no_associativity] Coq accepts notations declared as nonassociative but the parser on
-   which Coq is built, namely Camlp5, currently does not implement ``no associativity`` and
-   replaces it with ``left associativity``; hence it is the same for Coq: ``no associativity``
+.. [#no_associativity] |Coq| accepts notations declared as nonassociative but the parser on
+   which |Coq| is built, namely Camlp5, currently does not implement ``no associativity`` and
+   replaces it with ``left associativity``; hence it is the same for |Coq|: ``no associativity``
    is in fact ``left associativity`` for the purposes of parsing