[sphinx] Improve Case analysis and induction section.

1 files changed, 69 insertions, 62 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 35c974e2e1..a0281fa50b 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1426,94 +1426,101 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
 .. tacn:: destruct @term
    :name: destruct
 
-   This tactic applies to any goal. The argument :n:`@term` must be of
+   This tactic applies to any goal. The argument :token:`term` must be of
    inductive or co-inductive type and the tactic generates subgoals, one
-   for each possible form of :n:`@term`, i.e. one for each constructor of the
-   inductive or co-inductive type. Unlike :n:`induction`, no induction
-   hypothesis is generated by :n:`destruct`.
+   for each possible form of :token:`term`, i.e. one for each constructor of the
+   inductive or co-inductive type. Unlike :tacn:`induction`, no induction
+   hypothesis is generated by :tacn:`destruct`.
+
+   .. tacv:: destruct @ident
 
-   There are special cases:
+      If :token:`ident` denotes a quantified variable of the conclusion
+      of the goal, then :n:`destruct @ident` behaves
+      as :n:`intros until @ident; destruct @ident`. If :token:`ident` is not
+      anymore dependent in the goal after application of :tacn:`destruct`, it
+      is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`).
 
-   + If :n:`@term` is an identifier :n:`@ident` denoting a quantified variable
-     of the conclusion of the goal, then :n:`destruct @ident` behaves as
-     :n:`intros until @ident; destruct @ident`. If :n:`@ident` is not anymore
-     dependent in the goal after application of :n:`destruct`, it is erased
-     (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`).
+      If :token:`ident` is an hypothesis of the context, and :token:`ident`
+      is not anymore dependent in the goal after application
+      of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as
+      in :n:`destruct (@ident)`).
 
-     + If term is a num, then destruct num behaves as intros until num
-       followed by destruct applied to the last introduced hypothesis.
+   .. tacv:: destruct @num
+
+      :n:`destruct @num` behaves as :n:`intros until @num`
+      followed by destruct applied to the last introduced hypothesis.
 
      .. note::
-        For destruction of a numeral, use syntax destruct (num) (not
+        For destruction of a numeral, use syntax :n:`destruct (@num)` (not
         very interesting anyway).
 
-   + In case term is an hypothesis :n:`@ident` of the context, and :n:`@ident`
-     is not anymore dependent in the goal after application of :n:`destruct`, it
-     is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`).
+   .. tacv:: destruct @pattern
 
-   + The argument :n:`@term` can also be a pattern of which holes are denoted
-     by “_”. In this case, the tactic checks that all subterms matching the
-     pattern in the conclusion and the hypotheses are compatible and
-     performs case analysis using this subterm.
+      The argument of :tacn:`destruct` can also be a pattern of which holes are
+      denoted by “_”. In this case, the tactic checks that all subterms
+      matching the pattern in the conclusion and the hypotheses are compatible
+      and performs case analysis using this subterm.
 
-.. tacv:: destruct {+, @term}
+   .. tacv:: destruct {+, @term}
 
-   This is a shortcut for :n:`destruct term; ...; destruct term`.
+      This is a shortcut for :n:`destruct @term; ...; destruct @term`.
 
-.. tacv:: destruct @term as @disj_conj_intro_pattern
+   .. tacv:: destruct @term as @disj_conj_intro_pattern
 
-   This behaves as :n:`destruct @term` but uses the names in :n:`@intro_pattern`
-   to name the variables introduced in the context. The :n:`@intro_pattern` must
-   have the form :n:`[p11 ... p1n | ... | pm1 ... pmn ]` with `m` being the
-   number of constructors of the type of :n:`@term`. Each variable introduced
-   by :n:`destruct` in the context of the `i`-th goal gets its name from the
-   list :n:`pi1 ... pin` in order. If there are not enough names,
-   :n:`@destruct` invents names for the remaining variables to introduce. More
-   generally, the :n:`pij` can be any introduction pattern (see
-   :tacn:`intros`). This provides a concise notation for chaining destruction of
-   an hypothesis.
+      This behaves as :n:`destruct @term` but uses the names
+      in :token:`disj_conj_intro_pattern` to name the variables introduced in the
+      context. The :token:`disj_conj_intro_pattern` must have the
+      form :n:`[p11 ... p1n | ... | pm1 ... pmn ]` with ``m`` being the
+      number of constructors of the type of :token:`term`. Each variable
+      introduced by :tacn:`destruct` in the context of the ``i``-th goal
+      gets its name from the list :n:`pi1 ... pin` in order. If there are not
+      enough names, :tacn:`destruct` invents names for the remaining variables
+      to introduce. More generally, the :n:`pij` can be any introduction
+      pattern (see :tacn:`intros`). This provides a concise notation for
+      chaining destruction of an hypothesis.
 
-.. tacv:: destruct @term eqn:@naming_intro_pattern
+   .. tacv:: destruct @term eqn:@naming_intro_pattern
+      :name: destruct ... eqn:
 
-   This behaves as :n:`destruct @term` but adds an equation between :n:`@term`
-   and the value that :n:`@term` takes in each of the possible cases. The name
-   of the equation is specified by :n:`@naming_intro_pattern` (see
-   :tacn:`intros`), in particular `?` can be used to let Coq generate a fresh
-   name.
+      This behaves as :n:`destruct @term` but adds an equation
+      between :token:`term` and the value that it takes in each of the
+      possible cases. The name of the equation is specified
+      by :token:`naming_intro_pattern` (see :tacn:`intros`),
+      in particular ``?`` can be used to let Coq generate a fresh name.
 
-.. tacv:: destruct @term with @bindings_list
+   .. tacv:: destruct @term with @bindings_list
 
-   This behaves like :n:`destruct @term` providing explicit instances for the
-   dependent premises of the type of :n:`@term` (see :ref:`syntax of bindings <bindingslist>`).
+      This behaves like :n:`destruct @term` providing explicit instances for
+      the dependent premises of the type of :token:`term`.
 
-.. tacv:: edestruct @term
-   :name: edestruct
+   .. tacv:: edestruct @term
+      :name: edestruct
 
-   This tactic behaves like :n:`destruct @term` except that it does not fail if
-   the instance of a dependent premises of the type of :n:`@term` is not
-   inferable. Instead, the unresolved instances are left as existential
-   variables to be inferred later, in the same way as :tacn:`eapply` does.
+      This tactic behaves like :n:`destruct @term` except that it does not
+      fail if the instance of a dependent premises of the type
+      of :token:`term` is not inferable. Instead, the unresolved instances
+      are left as existential variables to be inferred later, in the same way
+      as :tacn:`eapply` does.
 
-.. tacv:: destruct @term using @term
-.. tacv:: destruct @term using @term with @bindings_list
+   .. tacv:: destruct @term using @term {? with @bindings_list }
 
-   These are synonyms of :n:`induction @term using @term` and
-   :n:`induction @term using @term with @bindings_list`.
+      This is synonym of :n:`induction @term using @term {? with @bindings_list }`.
 
-.. tacv:: destruct @term in @goal_occurrences
+   .. tacv:: destruct @term in @goal_occurrences
 
-   This syntax is used for selecting which occurrences of :n:`@term` the case
-   analysis has to be done on. The :n:`in @goal_occurrences` clause is an
-   occurrence clause whose syntax and behavior is described in
-   :ref:`occurences sets <occurencessets>`.
+      This syntax is used for selecting which occurrences of :token:`term`
+      the case analysis has to be done on. The :n:`in @goal_occurrences`
+      clause is an occurrence clause whose syntax and behavior is described
+      in :ref:`occurences sets <occurencessets>`.
 
-.. tacv:: destruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences
-.. tacv:: edestruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences
+   .. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences }
+             edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences }
 
-   These are the general forms of :n:`destruct` and :n:`edestruct`. They combine
-   the effects of the `with`, `as`, `eqn:`, `using`, and `in` clauses.
+      These are the general forms of :tacn:`destruct` and :tacn:`edestruct`.
+      They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``,
+      and ``in`` clauses.
 
-.. tacv:: case term
+.. tacn:: case term
    :name: case
 
    The tactic :n:`case` is a more basic tactic to perform case analysis without