induction/destruct : nicer syntax for generating equations (solves #2741)

 The ugly syntax "destruct x as [ ]_eqn:H" is replaced by:

  destruct x eqn:H
  destruct x as [ ] eqn:H

 Some with induction. Of course, the pattern behind "as" is arbitrary.
 For an anonymous version, H could be replaced by ?. The old syntax
 with "_eqn" still works for the moment, by triggers a warning.

 For making this new syntax work, we had to change the seldom-used
 "induction x y z using foo" into "induction x, y, z using foo".
 Now, only one "using" can be used per command instead of one per
 comma-separated group earlier, but I doubt this will bother anyone.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 21 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 465ee925ee..505db64d08 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1765,7 +1765,7 @@ induction n.
   {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
   {\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}.
 
-\item{\tt induction {\term} as {\namingintropattern}}
+\item{\tt induction {\term} eqn:{\namingintropattern}}
 
   This behaves as {\tt induction {\term}} but adds an equation between
   {\term} and the value that {\term} takes in each of the induction
@@ -1773,7 +1773,7 @@ induction n.
   {\namingintropattern} which can be an identifier, a ``?'', etc, as
   indicated in Section~\ref{intros-pattern}.
 
-\item{\tt induction {\term} as {\namingintropattern} {\disjconjintropattern}}
+\item{\tt induction {\term} as {\disjconjintropattern} eqn:{\namingintropattern}}
 
   This combines the two previous forms.
 
@@ -1802,7 +1802,7 @@ induction n.
   This behaves as {\tt induction {\term$_1$} using {\term$_2$}} but
   also providing instances for the premises of the type of {\term$_2$}.
 
-\item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}}
+\item \texttt{induction {\term}$_1$, $\ldots$, {\term}$_n$ using {\qualid}}
 
   This syntax is used for the case {\qualid} denotes an induction principle
   with complex predicates as the induction principles generated by
@@ -1818,14 +1818,14 @@ induction n.
   When an occurrence clause is given, an equation between {\term} and
   the value it gets in each case of the induction is added to the
   context of the subgoals corresponding to the induction cases (even
-  if no clause {\tt as {\namingintropattern}} is given).
+  if no clause {\tt eqn:{\namingintropattern}} is given).
 
-\item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
-     {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+\item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+     {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
 
   These are the most general forms of {\tt induction} and {\tt
   einduction}.  It combines the effects of the {\tt with}, {\tt as},
-  {\tt using}, and {\tt in} clauses.
+  {\tt eqn:}, {\tt using}, and {\tt in} clauses.
 
 \item {\tt elim \term}\label{elim}
   
@@ -1946,6 +1946,10 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
 \end{itemize}
 
 \begin{Variants}
+\item{\tt destruct \term$_1$, \ldots, \term$_n$}
+
+  This is a shortcut for {\tt destruct \term$_1$; \ldots; destruct \term$_n$}.
+
 \item{\tt destruct {\term} as {\disjconjintropattern}}
   
   This behaves as {\tt destruct {\term}} but uses the names in
@@ -1964,20 +1968,13 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
 %  It is recommended to use this variant of {\tt destruct} for 
 %  robust proof scripts.
 
-\item{\tt destruct {\term} as {\disjconjintropattern} \_eqn}
+\item{\tt destruct {\term} eqn:{\namingintropattern}}
 
   This behaves as {\tt destruct {\term}} but adds an equation between
   {\term} and the value that {\term} takes in each of the possible
-  cases.  The name of the equation is chosen by Coq. If  
-  {\disjconjintropattern} is simply {\tt []}, it is automatically considered
-  as a disjunctive pattern of the appropriate size.
-
-\item{\tt destruct {\term} as {\disjconjintropattern} \_eqn: {\namingintropattern}}
-
-  This behaves as {\tt destruct {\term} as
-    {\disjconjintropattern} \_eqn} but use {\namingintropattern} to
-  name the equation (see Section~\ref{intros-pattern}). Note that spaces 
-  can generally be removed around {\tt \_eqn}.
+  cases.  The name of the equation is specified by {\namingintropattern}
+  (see Section~\ref{intros-pattern}), in particular {\tt ?} can be
+  used to let Coq generate a fresh name.
 
 \item{\tt destruct {\term} with \bindinglist}
 
@@ -2011,11 +2008,11 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
   context of the subgoals corresponding to the cases (even
   if no clause {\tt as {\namingintropattern}} is given).
 
-\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} \_eqn: {\namingintropattern}  using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
-     {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} \_eqn: {\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern}  using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+     {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
 
   These are the general forms of {\tt destruct} and {\tt edestruct}.
-  They combine the effects of the {\tt with}, {\tt as}, {\tt using},
+  They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
   and {\tt in} clauses.
 
 \item{\tt case \term}\label{case}\tacindex{case}