[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.

The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.

6 files changed, 34 insertions, 34 deletions

diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index f8c0e23696..2460461ede 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -182,7 +182,7 @@ Manual declaration of implicit arguments
 Automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-   The ":n:`default implicits`" :token:`args_modifier` clause tells |Coq| to automatically determine the
+   The ":n:`default implicits`" :token:`args_modifier` clause tells Coq to automatically determine the
    implicit arguments of the object.
 
    Auto-detection is governed by flags specifying whether strict,
@@ -378,7 +378,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
@@ -395,7 +395,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`),
@@ -417,7 +417,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:
 
@@ -432,7 +432,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 38c9fa336d..48120503af 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
@@ -196,7 +196,7 @@ We amend that by equipping ``nat`` with a comparison relation.
    Check 3 == 3.
    Eval compute in 3 == 4.
 
-This last test shows that |Coq| is now not only able to type check ``3 == 3``,
+This last test shows that Coq is now not only able to type check ``3 == 3``,
 but also that the infix relation was bound to the ``nat_eq`` relation.
 This relation is selected whenever ``==`` is used on terms of type nat.
 This can be read in the line declaring the canonical structure
@@ -223,8 +223,8 @@ 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
+The error message is telling that Coq has no idea on how to compare
+pairs of objects. The following construction is telling Coq exactly
 how to do that.
 
 .. coqtop:: all
@@ -241,7 +241,7 @@ how to do that.
 
   Check forall n m : nat, (3, 4) == (n, m).
 
-Thanks to the ``pair_EQty`` declaration, |Coq| is able to build a comparison
+Thanks to the ``pair_EQty`` declaration, Coq is able to build a comparison
 relation for pairs whenever it is able to build a comparison relation
 for each component of the pair. The declaration associates to the key ``*``
 (the type constructor of pairs) the canonical comparison
@@ -290,7 +290,7 @@ As before we register a canonical ``LE`` class for ``nat``.
 
   Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
 
-And we enable |Coq| to relate pair of terms with ``<=``.
+And we enable Coq to relate pair of terms with ``<=``.
 
 .. coqtop:: all
 
@@ -355,10 +355,10 @@ theory of this new class.
 
 
 The problem is that the two classes ``LE`` and ``LEQ`` are not yet related by
-a subclass relation. In other words |Coq| does not see that an object of
+a subclass relation. In other words Coq does not see that an object of
 the ``LEQ`` class is also an object of the ``LE`` class.
 
-The following two constructions tell |Coq| how to canonically build the
+The following two constructions tell Coq how to canonically build the
 ``LE.type`` and ``EQ.type`` structure given an ``LEQ.type`` structure on the same
 type.
 
@@ -413,7 +413,7 @@ setting to any concrete instate of the algebraic structure.
 
   Abort.
 
-Again one has to tell |Coq| that the type ``nat`` is in the ``LEQ`` class, and
+Again one has to tell Coq that the type ``nat`` is in the ``LEQ`` class, and
 how the type constructor ``*`` interacts with the ``LEQ`` class. In the
 following proofs are omitted for brevity.
 
@@ -468,7 +468,7 @@ Note that no direct proof of ``n <= m -> m <= n -> n == m`` is provided by
 the user for ``n`` and m of type ``nat * nat``. What the user provides is a
 proof of this statement for ``n`` and ``m`` of type ``nat`` and a proof that the
 pair constructor preserves this property. The combination of these two
-facts is a simple form of proof search that |Coq| performs automatically
+facts is a simple form of proof search that Coq performs automatically
 while inferring canonical structures.
 
 Compact declaration of Canonical Structures
@@ -507,7 +507,7 @@ instances: ``[find e | EQ.obj e ~ T | "is not an EQ.type" ]``. It should be
 read as: “find a class e such that its objects have type T or fail
 with message "T is not an EQ.type"”.
 
-The other utilities are used to ask |Coq| to solve a specific unification
+The other utilities are used to ask Coq to solve a specific unification
 problem, that will in turn require the inference of some canonical structures.
 They are explained in more details in :cite:`CSwcu`.
 
@@ -532,7 +532,7 @@ The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers al
 the other pieces of the class ``LEQ`` and declares them as canonical
 values associated to the ``T`` key. All in all, the only new piece of
 information we add in the ``LEQ`` class is the mixin, all the rest is
-already canonical for ``T`` and hence can be inferred by |Coq|.
+already canonical for ``T`` and hence can be inferred by Coq.
 
 ``Pack`` is a notation, hence it is not type checked at the time of its
 declaration. It will be type checked when it is used, an in that case ``T`` is
diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
index dc208a63a0..fd9695e270 100644
--- a/doc/sphinx/language/extensions/evars.rst
+++ b/doc/sphinx/language/extensions/evars.rst
@@ -13,7 +13,7 @@ Existential variables
    | ?[ ?@ident ]
    | ?@ident {? @%{ {+; @ident := @term } %} }
 
-|Coq| terms can include existential variables that represent unknown
+Coq terms can include existential variables that represent unknown
 subterms that are eventually replaced with actual subterms.
 
 Existential variables are generated in place of unsolved implicit
@@ -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 9457505feb..23ba5f703a 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`
@@ -146,7 +146,7 @@ by replacing it with `_`.
 .. exn:: Cannot infer a term for this placeholder.
    :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments)
 
-   |Coq| was not able to deduce an instantiation of a “_”.
+   Coq was not able to deduce an instantiation of a “_”.
 
 .. _declare-implicit-args:
 
@@ -290,8 +290,8 @@ Controlling contextual implicit arguments
 
 .. flag:: Contextual Implicit
 
-   By default, |Coq| does not automatically set implicit the contextual
-   implicit arguments. You can turn this flag on to tell |Coq| to also
+   By default, Coq does not automatically set implicit the contextual
+   implicit arguments. You can turn this flag on to tell Coq to also
    infer contextual implicit argument.
 
 .. _controlling-rev-pattern-implicit-args:
@@ -301,8 +301,8 @@ Controlling reversible-pattern implicit arguments
 
 .. flag:: Reversible Pattern Implicit
 
-   By default, |Coq| does not automatically set implicit the reversible-pattern
-   implicit arguments. You can turn this flag on to tell |Coq| to also infer
+   By default, Coq does not automatically set implicit the reversible-pattern
+   implicit arguments. You can turn this flag on to tell Coq to also infer
    reversible-pattern implicit argument.
 
 .. _controlling-insertion-implicit-args:
diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst
index ea7271179e..ed207ca743 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 3c1983ee97..23389eba3b 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -5,7 +5,7 @@ Extended pattern matching
 
 :Authors: Cristina Cornes and Hugo Herbelin
 
-This section describes the full form of pattern matching in |Coq| terms.
+This section describes the full form of pattern matching in Coq terms.
 
 .. |rhs| replace:: right hand sides
 
@@ -187,10 +187,10 @@ Printing nested patterns
    pattern matching into a single pattern matching over a nested
    pattern.
 
-   When this flag is on (default), |Coq|’s printer tries to do such
+   When this flag is on (default), Coq’s printer tries to do such
    limited re-factorization.
-   Turning it off tells |Coq| to print only simple pattern matching problems
-   in the same way as the |Coq| kernel handles them.
+   Turning it off tells Coq to print only simple pattern matching problems
+   in the same way as the Coq kernel handles them.
 
 
 Factorization of clauses with same right-hand side
@@ -200,7 +200,7 @@ Factorization of clauses with same right-hand side
 
    When several patterns share the same right-hand side, it is additionally
    possible to share the clauses using disjunctive patterns. Assuming that the
-   printing matching mode is on, this flag (on by default) tells |Coq|'s
+   printing matching mode is on, this flag (on by default) tells Coq's
    printer to try to do this kind of factorization.
 
 Use of a default clause
@@ -212,7 +212,7 @@ Use of a default clause
    arguments of the patterns, yet an extra factorization is possible: the
    disjunction of patterns can be replaced with a `_` default clause. Assuming that
    the printing matching mode and the factorization mode are on, this flag (on by
-   default) tells |Coq|'s printer to use a default clause when relevant.
+   default) tells Coq's printer to use a default clause when relevant.
 
 Printing of wildcard patterns
 ++++++++++++++++++++++++++++++
@@ -234,7 +234,7 @@ Printing of the elimination predicate
    In most of the cases, the type of the result of a matched term is
    mechanically synthesizable. Especially, if the result type does not
    depend of the matched term. When this flag is on (default),
-   the result type is not printed when |Coq| knows that it can re-
+   the result type is not printed when Coq knows that it can re-
    synthesize it.
 
 
@@ -676,7 +676,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