Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.

Reviewed-by: jfehrle
Reviewed-by: cpitclaudel

1 files changed, 4 insertions, 4 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 7638fce010..cdd31fcb86 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
@@ -513,7 +513,7 @@ 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.