Merge PR #11924: Add style for smallcaps.

Reviewed-by: jfehrle

1 files changed, 8 insertions, 8 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index f18569c7fd..37d12e8ce5 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -8,7 +8,7 @@ This chapter documents the tactic language |Ltac|.
 We start by giving the syntax followed by the informal
 semantics. To learn more about the language and
 especially about its foundations, please refer to :cite:`Del00`.
-(Note the examples in the paper won't work as-is; Coq has evolved
+(Note the examples in the paper won't work as-is; |Coq| has evolved
 since the paper was written.)
 
 .. example:: Basic tactic macros
@@ -41,7 +41,7 @@ higher precedence than `+`.  Usually `a/b/c` is given the :gdef:`left associativ
 interpretation `(a/b)/c` rather than the :gdef:`right associative` interpretation
 `a/(b/c)`.
 
-In Coq, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4`
+In |Coq|, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4`
 is interpreted as :n:`(try (repeat (@tactic__1 || @tactic__2)); @tactic__3); @tactic__4`
 because `||` is part of :token:`ltac_expr2`, which has higher precedence than
 :tacn:`try` and :tacn:`repeat` (at the level of :token:`ltac_expr3`), which
@@ -784,7 +784,7 @@ single success:
 Checking for a single success: exactly_once
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Coq provides an experimental way to check that a tactic has *exactly
+|Coq| provides an experimental way to check that a tactic has *exactly
 one* success:
 
 .. tacn:: exactly_once @ltac_expr3
@@ -813,7 +813,7 @@ one* success:
 Checking for failure: assert_fails
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*:
+|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*:
 
 .. tacn:: assert_fails @ltac_expr3
    :name: assert_fails
@@ -859,7 +859,7 @@ Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*:
 Checking for success: assert_succeeds
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one*
+|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one*
 success:
 
 .. tacn:: assert_succeeds @ltac_expr3
@@ -904,7 +904,7 @@ Failing
 
    See the example for a comparison of the two constructs.
 
-   Note that if Coq terms have to be
+   Note that if |Coq| terms have to be
    printed as part of the failure, term construction always forces the
    tactic into the goals, meaning that if there are no goals when it is
    evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed.
@@ -989,7 +989,7 @@ amount of time:
       timeout with some other tacticals. This tactical is hence proposed only
       for convenience during debugging or other development phases, we strongly
       advise you to not leave any timeout in final scripts. Note also that
-      this tactical isn’t available on the native Windows port of Coq.
+      this tactical isn’t available on the native Windows port of |Coq|.
 
 Timing a tactic
 ~~~~~~~~~~~~~~~
@@ -1884,7 +1884,7 @@ Proving that a list is a permutation of a second list
    From Section :ref:`ltac-syntax` we know that Ltac has a primitive
    notion of integers, but they are only used as arguments for
    primitive tactics and we cannot make computations with them. Thus,
-   instead, we use Coq's natural number type :g:`nat`.
+   instead, we use |Coq|'s natural number type :g:`nat`.
 
    .. coqtop:: in