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

2 files changed, 76 insertions, 70 deletions

diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index e80cfb6bb5..6e7ccba63c 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -412,7 +412,7 @@ end of a definition or proof, we check that the only remaining
 universes are the ones declared. In the term and in general in proof
 mode, introduced universe names can be referred to in terms. Note that
 local universe names shadow global universe names. During a proof, one
-can use :ref:`Show Universes <ShowUniverses>` to display the current context of universes.
+can use :cmd:`Show Universes` to display the current context of universes.
 
 Definitions can also be instantiated explicitly, giving their full
 instance:
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index df8ef74f74..45ee52b1e0 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