[sphinx] Use arguments of '.. example::' directive as a title

Most existing uses of .. example did not use the first line as a title, so this
commit also adds appropriate blank lines.

12 files changed, 75 insertions, 12 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 32de15ee31..1643baf0e8 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -239,6 +239,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
     http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition
     for more details.
 
+    Optionally, any text immediately following the ``.. example::`` header is
+    used as the example's title.
+
     Example::
 
        .. example:: Adding a hint to a database
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index b6c35d8fa7..0f2d35d044 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -32,6 +32,7 @@ When the proof ends two constants are defined:
   ends with ``Qed``, and transparent if the proof ends with ``Defined``.
 
 .. example::
+
   .. coqtop:: all
 
      Require Coq.derive.Derive.
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 98e81ebc65..6e0c1e1b61 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -723,6 +723,7 @@ each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{
 the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts).
 
 .. example::
+
    The declaration for parameterized lists is:
 
    .. math::
@@ -741,6 +742,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is
       | cons : A -> list A -> list A.
 
 .. example::
+
    The declaration for a mutual inductive definition of tree and forest
    is:
 
@@ -763,6 +765,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is
       | consf : tree -> forest -> forest.
 
 .. example::
+
    The declaration for a mutual inductive definition of even and odd is:
 
    .. math::
@@ -811,6 +814,7 @@ contains an inductive declaration.
    E[Γ] ⊢ c : C
 
 .. example::
+
    Provided that our environment :math:`E` contains inductive definitions we showed before,
    these two inference rules above enable us to conclude that:
 
@@ -919,6 +923,7 @@ condition* for a constant :math:`X` in the following cases:
 
 
 .. example::
+
    For instance, if one considers the following variant of a tree type
    branching over the natural numbers:
 
@@ -985,6 +990,7 @@ the Type hierarchy.
 
 
 .. example::
+
    It is well known that the existential quantifier can be encoded as an
    inductive definition. The following declaration introduces the second-
    order existential quantifier :math:`∃ X.P(X)`.
@@ -1102,6 +1108,7 @@ sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). A
 an example, let us consider the following definition:
 
 .. example::
+
    .. coqtop:: in
 
       Inductive option (A:Type) : Type :=
@@ -1118,6 +1125,7 @@ if :g:`option` is applied to a type in :math:`\Prop`, then, the result is not se
 if set in :math:`\Prop`.
 
 .. example::
+
    .. coqtop:: all
 
       Check (fun A:Set => option A).
@@ -1126,6 +1134,7 @@ if set in :math:`\Prop`.
 Here is another example.
 
 .. example::
+
    .. coqtop:: in
 
       Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
@@ -1136,6 +1145,7 @@ none in :math:`\Type`, and in :math:`\Type` otherwise. In all cases, the three k
 eliminations schemes are allowed.
 
 .. example::
+
    .. coqtop:: all
 
       Check (fun A:Set => prod A).
@@ -1324,6 +1334,7 @@ the extraction mechanism. Assume :math:`A` and :math:`B` are two propositions, a
 logical disjunction :math:`A ∨ B` is defined inductively by:
 
 .. example::
+
    .. coqtop:: in
 
       Inductive or (A B:Prop) : Prop :=
@@ -1334,6 +1345,7 @@ The following definition which computes a boolean value by case over
 the proof of :g:`or A B` is not accepted:
 
 .. example::
+
    .. coqtop:: all
 
       Fail Definition choice (A B: Prop) (x:or A B) :=
@@ -1357,6 +1369,7 @@ property which are provably different, contradicting the proof-
 irrelevance property which is sometimes a useful axiom:
 
 .. example::
+
    .. coqtop:: all
 
       Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
@@ -1390,6 +1403,7 @@ be used for rewriting not only in logical propositions but also in any
 type.
 
 .. example::
+
    .. coqtop:: all
 
       Print eq_rec.
@@ -1421,6 +1435,7 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:
 
 
 .. example::
+
    The following term in concrete syntax::
 
        match t as l return P' with
@@ -1485,6 +1500,7 @@ definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;…;c_n :C_
 
 
 .. example::
+
    Below is a typing rule for the term shown in the previous example:
 
    .. inference:: list example
@@ -1634,6 +1650,7 @@ The following definitions are correct, we enter them using the :cmd:`Fixpoint`
 command and show the internal representation.
 
 .. example::
+
    .. coqtop:: all
 
       Fixpoint plus (n m:nat) {struct n} : nat :=
@@ -1810,6 +1827,7 @@ option ``-impredicative-set``. For example, using the ordinary `coqtop`
 command, the following is rejected,
 
 .. example::
+
    .. coqtop:: all
 
       Fail Definition id: Set := forall X:Set,X->X.
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 52c56d2bd2..9de30e2190 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -848,6 +848,7 @@ Notation          Interpretation        Precedence  Associativity
 
 
 .. example::
+
   .. coqtop:: all reset
 
     Require Import ZArith.
@@ -887,6 +888,7 @@ Notation          Interpretation
 ===============   ===================
 
 .. example::
+
   .. coqtop:: all reset
 
     Require Import Reals.
@@ -906,6 +908,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
   Proves that two real integer constants are different.
 
 .. example::
+
   .. coqtop:: all reset
 
     Require Import DiscrR.
@@ -919,6 +922,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
   Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions.
 
 .. example::
+
   .. coqtop:: all reset
 
     Require Import Reals.
@@ -933,6 +937,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
   corresponding to the condition on each operand of the product.
 
 .. example::
+
   .. coqtop:: all reset
 
     Require Import Reals.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 394b928ada..7dd0a6e383 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -70,7 +70,9 @@ generates a variant type definition with just one constructor:
 To build an object of type :n:`@ident`, one should provide the constructor
 :n:`@ident₀` with the appropriate number of terms filling the fields of the record.
 
-.. example:: Let us define the rational :math:`1/2`:
+.. example::
+
+   Let us define the rational :math:`1/2`:
 
     .. coqtop:: in
 
@@ -1849,15 +1851,15 @@ are named as expected.
 
 .. example:: (continued)
 
-.. coqtop:: all
+   .. coqtop:: all
 
-   Arguments p [s t] _ [u] _: rename.
+      Arguments p [s t] _ [u] _: rename.
 
-   Check (p r1 (u:=c)).
+      Check (p r1 (u:=c)).
 
-   Check (p (s:=a) (t:=b) r1 (u:=c) r2).
+      Check (p (s:=a) (t:=b) r1 (u:=c) r2).
 
-   Fail Arguments p [s t] _ [w] _ : assert.
+      Fail Arguments p [s t] _ [w] _ : assert.
 
 .. _displaying-implicit-args:
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 8250b4b3d6..da5cd00d72 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -758,6 +758,7 @@ Simple inductive types
       the case of annotated inductive types — cf. next section).
 
    .. example::
+
       The set of natural numbers is defined as:
 
       .. coqtop:: all
@@ -976,6 +977,7 @@ Mutually defined inductive types
       reason, the parameters must be strictly the same for each inductive types.
 
 .. example::
+
    The typical example of a mutual inductive data type is the one for trees and
    forests. We assume given two types :g:`A` and :g:`B` as variables. It can
    be declared the following way.
@@ -1048,6 +1050,7 @@ of the type.
    For co-inductive types, the only elimination principle is case analysis.
 
 .. example::
+
    An example of a co-inductive type is the type of infinite sequences of
    natural numbers, usually called streams.
 
@@ -1067,6 +1070,7 @@ Definition of co-inductive predicates and blocks of mutually
 co-inductive definitions are also allowed.
 
 .. example::
+
    An example of a co-inductive predicate is the extensional equality on
    streams:
 
@@ -1129,6 +1133,7 @@ constructions.
 
 
    .. example::
+
       One can define the addition function as :
 
       .. coqtop:: all
@@ -1201,6 +1206,7 @@ constructions.
       inductive types.
 
       .. example::
+
          The size of trees and forests can be defined the following way:
 
          .. coqtop:: all
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index e15bcb8e2c..59bc2d22aa 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -218,6 +218,7 @@ file timing data:
       On ``Mac OS``, this works best if you’ve installed ``gnu-time``.
 
     .. example::
+
        For example, the output of ``make TIMED=1`` may look like
        this:
 
@@ -295,6 +296,7 @@ file timing data:
        files which take effectively no time to compile.
 
     .. example::
+
         For example, the output table from
         ``make print-pretty-timed-diff`` may look like this:
 
@@ -318,6 +320,7 @@ line timing data:
     line-by-line timing information.
 
     .. example::
+
        For example, running ``make all TIMING=1`` may result in a file like this:
 
        ::
@@ -345,6 +348,7 @@ line timing data:
        This target requires python to build the table.
 
     .. example::
+
        For example, running  ``print-pretty-single-time-diff`` might give a table like this:
 
        ::
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 78719c1ef1..225df8d54c 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -341,8 +341,7 @@ involves conditional rewritings and shows how to deal with them using
 the optional tactic of the ``Hint Rewrite`` command.
 
 
-.. example::
-   Ackermann function
+.. example:: Ackermann function
 
    .. coqtop:: in reset
 
@@ -370,8 +369,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
       autorewrite with base0 using try reflexivity.
 
-.. example::
-   MacCarthy function
+.. example:: MacCarthy function
 
    .. coqtop:: in reset
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 44376080c3..a9d0c16376 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -375,6 +375,7 @@ or focus the next one.
 The following example script illustrates all these features:
 
 .. example::
+
   .. coqtop:: all
 
     Goal (((True /\ True) /\ True) /\ True) /\ True.
@@ -511,6 +512,7 @@ Requesting information
       :token:`ident`
 
       .. example::
+
          .. coqtop:: all
 
             Show Match nat.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 6fb73a030f..8a2fc3996a 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -4632,6 +4632,7 @@ bookkeeping steps.
 
 
 .. example::
+
    The following example use the ``~~`` prenex notation for boolean negation:
 
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index e6bc84365c..fdb04bf9a0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -207,6 +207,7 @@ Applying theorems
    useful to advanced users.
 
    .. example::
+
       .. coqtop:: reset all
 
          Inductive Option : Set :=
@@ -366,6 +367,7 @@ Applying theorems
       .. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product.
 
 .. example::
+
    Assume we have a transitive relation ``R`` on ``nat``:
 
    .. coqtop:: reset in
@@ -837,6 +839,7 @@ quantified variables or hypotheses until the goal is not any more a
 quantification or an implication.
 
 .. example::
+
    .. coqtop:: all
 
       Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
@@ -958,6 +961,7 @@ quantification or an implication.
 .. exn:: Cannot move @ident after @ident : it depends on @ident.
 
 .. example::
+
    .. coqtop:: all
 
       Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x.
@@ -1082,6 +1086,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
    obtain atomic ones.
 
 .. example::
+
    .. coqtop:: all
 
       Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
@@ -1252,6 +1257,7 @@ Controlling the proof flow
    respect to some term.
 
 .. example::
+
    .. coqtop:: reset none
 
       Goal forall x y:nat, 0 <= x + y + y.
@@ -1567,6 +1573,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
      performs induction using this subterm.
 
 .. example::
+
    .. coqtop:: reset all
 
       Lemma induction_test : forall n:nat, n = n -> n <= n.
@@ -1636,6 +1643,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    those are generalized as well in the statement to prove.
 
    .. example::
+
       .. coqtop:: reset all
 
          Lemma comm x y : x + y = y + x.
@@ -1744,6 +1752,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    still get enough information in the proofs.
 
 .. example::
+
    .. coqtop:: reset all
 
       Lemma le_minus : forall n:nat, n < 1 -> n = 0.
@@ -1809,6 +1818,7 @@ and an explanation of the underlying technique.
    Note that this tactic is only available after a ``Require Import FunInd``.
 
 .. example::
+
    .. coqtop:: reset all
 
       Require Import FunInd.
@@ -2856,6 +2866,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    + A constant can be marked to be never unfolded by ``cbn`` or ``simpl``:
 
      .. example::
+
         .. coqtop:: all
 
            Arguments minus n m : simpl never.
@@ -2868,6 +2879,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
      ``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command.
 
      .. example::
+
         .. coqtop:: all
 
            Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
@@ -2880,6 +2892,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
      always unfolded.
 
      .. example::
+
         .. coqtop:: all
 
            Definition volatile := fun x : nat => x.
@@ -2890,6 +2903,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
      such arguments.
 
      .. example::
+
         .. coqtop:: all
 
            Arguments minus !n !m.
@@ -3180,6 +3194,7 @@ where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto`
 can solve such a goal:
 
 .. example::
+
    .. coqtop:: all
 
       Hint Resolve ex_intro.
@@ -3748,6 +3763,7 @@ The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would
 fail:
 
 .. example::
+
    .. coqtop:: reset all
 
       Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
@@ -3904,6 +3920,7 @@ equality must contain all the quantified variables in order for congruence to
 match against it.
 
 .. example::
+
    .. coqtop:: reset all
 
       Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
@@ -4315,6 +4332,7 @@ declare new field structures. All declared field structures can be
 printed with the Print Fields command.
 
 .. example::
+
    .. coqtop:: reset all
 
       Require Import Reals.
@@ -4426,6 +4444,7 @@ Simple tactic macros
 A simple example has more value than a long explanation:
 
 .. example::
+
    .. coqtop:: reset all
 
       Ltac Solve := simpl; intros; auto.
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index c9487abf03..e6b71a8293 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -571,6 +571,9 @@ class ExampleDirective(BaseAdmonition):
     http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition
     for more details.
 
+    Optionally, any text immediately following the ``.. example::`` header is
+    used as the example's title.
+
     Example::
 
        .. example:: Adding a hint to a database
@@ -583,13 +586,14 @@ class ExampleDirective(BaseAdmonition):
     """
     node_class = nodes.admonition
     directive_name = "example"
+    optional_arguments = 1
 
     def run(self):
         # ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’,
         # and uses arguments[0] as the title in that case (in other cases, the
         # title is unset, and it is instead set in the HTML visitor).
-        assert not self.arguments # Arguments have been parsed as content
-        self.arguments = ['Example']
+        assert len(self.arguments) <= 1
+        self.arguments = [": ".join(['Example'] + self.arguments)]
         self.options['classes'] = ['admonition', 'note']
         return super().run()