Merge PR #11100: small documentation fixes

Reviewed-by: Zimmi48
Ack-by: cpitclaudel

4 files changed, 7 insertions, 6 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 9f92fc4c56..0754145b39 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -530,7 +530,7 @@ A detailed example: Euclidean division
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The file ``Euclid`` contains the proof of Euclidean division.
-The natural numbers used here are unary, represented by the type``nat``,
+The natural numbers used here are unary, represented by the type ``nat``,
 which is defined by two constructors ``O`` and ``S``.
 This module contains a theorem ``eucl_dev``, whose type is::
 
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 93a1be027c..4feda5e875 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -117,7 +117,7 @@ parameters is any term :math:`f \, t_1 \ldots t_n`.
 .. example:: Morphisms
 
    Continuing the previous example, let ``union: forall (A : Type), list A -> list A -> list A``
-   perform the union of two sets by appending one list to the other. ``union` is a binary
+   perform the union of two sets by appending one list to the other. ``union`` is a binary
    morphism parametric over ``A`` that respects the relation instance
    ``(set_eq A)``. The latter condition is proved by showing:
 
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index db089df395..3d73f9bd6e 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -192,7 +192,7 @@ s},
 
 @InProceedings{Del00,
   author      = {Delahaye, D.},
-  title       = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}},
+  title       = {A {T}actic {L}anguage for the {S}ystem {Coq}},
   booktitle   = {Proceedings of Logic for Programming and Automated Reasoning
                (LPAR), Reunion Island},
   publisher   = SV,
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 4c697be963..853ddfd6dc 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1513,7 +1513,7 @@ In a goal like the following::
   =============
   m < 5 + n
 
-The tactic ``abstract: abs n`` first generalizes the goal with respect ton
+The tactic :g:`abstract: abs n` first generalizes the goal with respect to :g:`n`
 (that is not visible to the abstract constant abs) and then assigns
 abs. The resulting goal is::
 
@@ -4071,6 +4071,7 @@ which the function is supplied:
    :name: congr
 
    This tactic:
+
    + checks that the goal is a Leibniz equality;
    + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints;
    + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal.
@@ -4218,7 +4219,7 @@ in the second column.
        ``ident`` in all the occurrences of ``term2``
    * - ``term1 as ident in term2``
      - ``term 1``
-     - in all the subterms identified by ``ident`
+     - in all the subterms identified by ``ident``
        in all the occurrences of ``term2[term 1 /ident]``
 
 The rewrite tactic supports two more patterns obtained prefixing the
@@ -5023,7 +5024,7 @@ mechanism:
    Coercion is_true (b : bool) := b = true.
 
 This allows any boolean formula ``b`` to be used in a context where |Coq|
-would expect a proposition, e.g., after ``Lemma … : ``. It is then
+would expect a proposition, e.g., after ``Lemma … :``. It is then
 interpreted as ``(is_true b)``, i.e., the proposition ``b = true``. Coercions
 are elided by the pretty-printer, so they are essentially transparent
 to the user.