[sphinx] Improvements around the Show commands, including missing indices and indentation.

1 files changed, 75 insertions, 69 deletions

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index df8ef74f7..45ee52b1e 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -440,110 +440,116 @@ Requesting information
 
 .. cmd:: Show
 
-This command displays the current goals.
+   This command displays the current goals.
 
+   .. exn:: No focused proof.
 
-.. cmdv:: Show @num
+   .. cmdv:: Show @num
 
-Displays only the :n:`@num`-th subgoal.
+      Displays only the :token:`num` th subgoal.
 
-.. exn:: No such goal.
-.. exn:: No focused proof.
+      .. exn:: No such goal.
 
-.. cmdv:: Show @ident
 
-Displays the named goal :n:`@ident`. This is useful in
-particular to display a shelved goal but only works if the
-corresponding existential variable has been named by the user
-(see :ref:`existential-variables`) as in the following example.
+   .. cmdv:: Show @ident
 
-.. example::
+      Displays the named goal :token:`ident`. This is useful in
+      particular to display a shelved goal but only works if the
+      corresponding existential variable has been named by the user
+      (see :ref:`existential-variables`) as in the following example.
 
-  .. coqtop:: all
+      .. example::
 
-    Goal exists n, n = 0.
-    eexists ?[n].
-    Show n.
+         .. coqtop:: all
 
-.. cmdv:: Show Script
+            Goal exists n, n = 0.
+            eexists ?[n].
+            Show n.
 
-Displays the whole list of tactics applied from the
-beginning of the current proof. This tactics script may contain some
-holes (subgoals not yet proved). They are printed under the form
+   .. cmdv:: Show Script
+      :name: Show Script
 
-``<Your Tactic Text here>``.
+      Displays the whole list of tactics applied from the
+      beginning of the current proof. This tactics script may contain some
+      holes (subgoals not yet proved). They are printed under the form
 
-.. cmdv:: Show Proof
+      ``<Your Tactic Text here>``.
 
-It displays the proof term generated by the tactics
-that have been applied. If the proof is not completed, this term
-contain holes, which correspond to the sub-terms which are still to be
-constructed. These holes appear as a question mark indexed by an
-integer, and applied to the list of variables in the context, since it
-may depend on them. The types obtained by abstracting away the context
-from the type of each hole-placer are also printed.
+   .. cmdv:: Show Proof
+      :name: Show Proof
 
-.. cmdv:: Show Conjectures
+      It displays the proof term generated by the tactics
+      that have been applied. If the proof is not completed, this term
+      contain holes, which correspond to the sub-terms which are still to be
+      constructed. These holes appear as a question mark indexed by an
+      integer, and applied to the list of variables in the context, since it
+      may depend on them. The types obtained by abstracting away the context
+      from the type of each hole-placer are also printed.
 
-It prints the list of the names of all the
-theorems that are currently being proved. As it is possible to start
-proving a previous lemma during the proof of a theorem, this list may
-contain several names.
+   .. cmdv:: Show Conjectures
+      :name: Show Conjectures
 
-.. cmdv:: Show Intro
+      It prints the list of the names of all the
+      theorems that are currently being proved. As it is possible to start
+      proving a previous lemma during the proof of a theorem, this list may
+      contain several names.
 
-If the current goal begins by at least one product,
-this command prints the name of the first product, as it would be
-generated by an anonymous ``intro``. The aim of this command is to ease
-the writing of more robust scripts. For example, with an appropriate
-Proof General macro, it is possible to transform any anonymous ``intro``
-into a qualified one such as ``intro y13``. In the case of a non-product
-goal, it prints nothing.
+   .. cmdv:: Show Intro
+      :name: Show Intro
 
-.. cmdv:: Show Intros
+      If the current goal begins by at least one product,
+      this command prints the name of the first product, as it would be
+      generated by an anonymous :tacn:`intro`. The aim of this command is to ease
+      the writing of more robust scripts. For example, with an appropriate
+      Proof General macro, it is possible to transform any anonymous :tacn:`intro`
+      into a qualified one such as ``intro y13``. In the case of a non-product
+      goal, it prints nothing.
 
-This command is similar to the previous one, it
-simulates the naming process of an intros.
+   .. cmdv:: Show Intros
+      :name: Show Intros
 
-.. cmdv:: Show Existentials
+      This command is similar to the previous one, it
+      simulates the naming process of an :tacn:`intros`.
 
-It displays the set of all uninstantiated
-existential variables in the current proof tree, along with the type
-and the context of each variable.
+   .. cmdv:: Show Existentials
+      :name: Show Existentials
 
-.. cmdv:: Show Match @ident
+      It displays the set of all uninstantiated
+      existential variables in the current proof tree, along with the type
+      and the context of each variable.
 
-This variant displays a template of the Gallina
-``match`` construct with a branch for each constructor of the type
-:n:`@ident`
+   .. cmdv:: Show Match @ident
 
-.. example::
-  .. coqtop:: all
+      This variant displays a template of the Gallina
+      ``match`` construct with a branch for each constructor of the type
+      :token:`ident`
 
-     Show Match nat.
+      .. example::
+         .. coqtop:: all
 
-.. exn:: Unknown inductive type.
+            Show Match nat.
 
-.. _ShowUniverses:
+      .. exn:: Unknown inductive type.
 
-.. cmdv:: Show Universes
+   .. cmdv:: Show Universes
+      :name: Show Universes
 
-It displays the set of all universe constraints and
-its normalized form at the current stage of the proof, useful for
-debugging universe inconsistencies.
+      It displays the set of all universe constraints and
+      its normalized form at the current stage of the proof, useful for
+      debugging universe inconsistencies.
 
 
 .. cmd:: Guarded
 
-Some tactics (e.g. :tacn:`refine`) allow to build proofs using
-fixpoint or co-fixpoint constructions. Due to the incremental nature
-of interactive proof construction, the check of the termination (or
-guardedness) of the recursive calls in the fixpoint or cofixpoint
-constructions is postponed to the time of the completion of the proof.
+   Some tactics (e.g. :tacn:`refine`) allow to build proofs using
+   fixpoint or co-fixpoint constructions. Due to the incremental nature
+   of interactive proof construction, the check of the termination (or
+   guardedness) of the recursive calls in the fixpoint or cofixpoint
+   constructions is postponed to the time of the completion of the proof.
 
-The command :cmd:`Guarded` allows checking if the guard condition for
-fixpoint and cofixpoint is violated at some time of the construction
-of the proof without having to wait the completion of the proof.
+   The command :cmd:`Guarded` allows checking if the guard condition for
+   fixpoint and cofixpoint is violated at some time of the construction
+   of the proof without having to wait the completion of the proof.
 
 
 Controlling the effect of proof editing commands