doc fixes

4 files changed, 7 insertions, 6 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 3dc8707a34..574b91664d 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -529,7 +529,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 2ea0861e47..73d9b93482 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 85b02013d8..d40fe7f583 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 75897fec45..e08e121276 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::
 
@@ -4061,6 +4061,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.
@@ -4208,7 +4209,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
@@ -5013,7 +5014,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.