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

21 files changed, 122 insertions, 114 deletions

diff --git a/CHANGES b/CHANGES
index 0819cdeed..91e5a33b0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -25,6 +25,9 @@ Tactics
   version of "tauto".
 - Similarly, "intuition" has been made more uniform and, where it now
   fails, "dintuition" can be used.
+- An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
+  or "induction" to make it generate equations in the spirit of "case_eq".
+  The former syntax "_eqn" is discontinued.
 
 Program
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 465ee925e..505db64d0 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}
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index c202664e2..3c646c03a 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -359,13 +359,15 @@ let rec mlexpr_of_atomic_tactic = function
                   $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacInductionDestruct (isrec,ev,l) ->
       <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$
-	$mlexpr_of_pair (mlexpr_of_list (mlexpr_of_triple
-	  (mlexpr_of_list mlexpr_of_induction_arg)
-	  (mlexpr_of_option mlexpr_of_constr_with_binding)
-	  (mlexpr_of_pair
-	    (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))
-	    (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)))))
-	  (mlexpr_of_option mlexpr_of_clause) l$ >>
+	$mlexpr_of_triple
+	(mlexpr_of_list
+	   (mlexpr_of_pair
+	      mlexpr_of_induction_arg
+	      (mlexpr_of_pair
+		 (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))
+		 (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)))))
+	(mlexpr_of_option mlexpr_of_constr_with_binding)
+	(mlexpr_of_option mlexpr_of_clause) l$ >>
 
   (* Context management *)
   | Tacexpr.TacClear (b,l) ->
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index ccf682a48..a70ed47d4 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -58,11 +58,14 @@ type 'id message_token =
   | MsgIdent of 'id
 
 type 'constr induction_clause =
-  ('constr with_bindings induction_arg list * 'constr with_bindings option *
-   (intro_pattern_expr located option * intro_pattern_expr located option))
+    'constr with_bindings induction_arg *
+    (intro_pattern_expr located option (* eqn:... *)
+    * intro_pattern_expr located option) (* as ... *)
 
 type ('constr,'id) induction_clause_list =
-    'constr induction_clause list * 'id clause_expr option
+    'constr induction_clause list
+    * 'constr with_bindings option (* using ... *)
+    * 'id clause_expr option (* in ... *)
 
 type multi =
   | Precisely of int
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 462aa2b46..202512a41 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -134,21 +134,19 @@ let induction_arg_of_constr (c,lbind as clbind) =
   else ElimOnConstr clbind
 
 let mkTacCase with_evar = function
-  | [([ElimOnConstr cl],None,(None,None))],None ->
+  | [ElimOnConstr cl,(None,None)],None,None ->
       TacCase (with_evar,cl)
   (* Reinterpret numbers as a notation for terms *)
-  | [([(ElimOnAnonHyp n)],None,(None,None))],None ->
+  | [ElimOnAnonHyp n,(None,None)],None,None ->
       TacCase (with_evar,
         (CPrim (Loc.ghost, Numeral (Bigint.of_string (string_of_int n))),
 	 NoBindings))
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
-  | [([ElimOnIdent id],None,(None,None))],None ->
+  | [ElimOnIdent id,(None,None)],None,None ->
       TacCase (with_evar,(CRef (Ident id),NoBindings))
   | ic ->
-      if List.exists (fun (cl,a,b) ->
-           List.exists (function ElimOnAnonHyp _ -> true | _ -> false) cl)
-           (fst ic)
+      if List.exists (function (ElimOnAnonHyp _,_) -> true | _ -> false) (pi1 ic)
       then
 	error "Use of numbers as direct arguments of 'case' is not supported.";
       TacInductionDestruct (false,with_evar,ic)
@@ -283,11 +281,6 @@ GEXTEND Gram
       | "*" -> loc, IntroForthcoming true
       | "**" -> loc, IntroForthcoming false ] ]
   ;
-  intropattern_modifier:
-    [ [ IDENT "_eqn";
-        id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ]
-        -> id ] ]
-  ;
   simple_intropattern:
     [ [ pat = disjunctive_intropattern -> pat
       | pat = naming_intropattern -> pat
@@ -459,10 +452,12 @@ GEXTEND Gram
     [ [ "as"; ipat = simple_intropattern -> Some ipat
       | -> None ] ]
   ;
-  with_induction_names:
-    [ [ "as"; ipat = simple_intropattern; eq = OPT intropattern_modifier
-        -> (eq,Some ipat)
-      | -> (None,None) ] ]
+  eqn_ipat:
+    [ [ IDENT "eqn"; ":"; id = naming_intropattern -> Some id
+      | IDENT "_eqn"; ":"; id = naming_intropattern ->
+        let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn\"" in
+        msg_warning (strbrk msg); Some id
+      | -> None ] ]
   ;
   as_name:
     [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
@@ -491,14 +486,11 @@ GEXTEND Gram
     [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
   ;
   induction_clause:
-    [ [ lc = LIST1 induction_arg; ipats = with_induction_names;
-        el = OPT eliminator -> (lc,el,ipats) ] ]
-  ;
-  one_induction_clause:
-    [ [ ic = induction_clause; cl = opt_clause -> ([ic],cl) ] ]
+    [ [ c = induction_arg; pat = as_ipat; eq = eqn_ipat -> (c,(eq,pat)) ] ]
   ;
   induction_clause_list:
-    [ [ ic = LIST1 induction_clause SEP ","; cl = opt_clause -> (ic,cl) ] ]
+    [ [ ic = LIST1 induction_clause SEP ",";
+	el = OPT eliminator; cl = opt_clause -> (ic,el,cl) ] ]
   ;
   move_location:
     [ [ IDENT "after"; id = id_or_meta -> MoveAfter id
@@ -592,9 +584,9 @@ GEXTEND Gram
       (* Derived basic tactics *)
       | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
           TacSimpleInductionDestruct (true,h)
-      | IDENT "induction"; ic = one_induction_clause ->
+      | IDENT "induction"; ic = induction_clause_list ->
 	  TacInductionDestruct (true,false,ic)
-      | IDENT "einduction"; ic = one_induction_clause ->
+      | IDENT "einduction"; ic = induction_clause_list ->
 	  TacInductionDestruct(true,true,ic)
       | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 815ee6e5c..e1575eab7 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -338,11 +338,15 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc
 let pr_with_bindings prlc prc (c,bl) =
   hov 1 (prc c ++ pr_bindings prlc prc bl)
 
+let pr_as_ipat pat = str "as " ++ pr_intro_pattern pat
+let pr_eqn_ipat pat = str "eqn:" ++ pr_intro_pattern pat
+
 let pr_with_induction_names = function
   | None, None -> mt ()
-  | eqpat, ipat ->
-      spc () ++ hov 1 (str "as" ++ pr_opt pr_intro_pattern eqpat ++
-                       pr_opt pr_intro_pattern ipat)
+  | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
+  | None, Some ipat -> spc () ++ hov 1 (pr_as_ipat ipat)
+  | Some eqpat, Some ipat ->
+    spc () ++ hov 1 (pr_as_ipat ipat ++ spc () ++ pr_eqn_ipat eqpat)
 
 let pr_as_intro_pattern ipat =
   spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
@@ -714,14 +718,14 @@ and pr_atom1 = function
   | TacSimpleInductionDestruct (isrec,h) ->
       hov 1 (str "simple " ++ str (if isrec then "induction" else "destruct")
              ++ pr_arg pr_quantified_hypothesis h)
-  | TacInductionDestruct (isrec,ev,(l,cl)) ->
+  | TacInductionDestruct (isrec,ev,(l,el,cl)) ->
       hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
              spc () ++
-             prlist_with_sep pr_comma (fun (h,e,ids) ->
-	       prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
-	       pr_with_induction_names ids ++
-               pr_opt pr_eliminator e) l ++
-               pr_opt_no_spc (pr_clauses None pr_ident) cl)
+             prlist_with_sep pr_comma (fun (h,ids) ->
+	       pr_induction_arg pr_lconstr pr_constr h ++
+	       pr_with_induction_names ids) l ++
+             pr_opt pr_eliminator el ++
+	     pr_opt_no_spc (pr_clauses None pr_ident) cl)
   | TacDoubleInduction (h1,h2) ->
       hov 1
         (str "double induction" ++
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index d5ee78fea..20b70cef4 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -84,12 +84,12 @@ let out_indarg = function
   | ElimOnAnonHyp n -> ElimOnAnonHyp n
 
 let h_induction_destruct isrec ev lcl =
-  let lcl' = on_fst (List.map (fun (a,b,c) ->(List.map out_indarg a,b,c))) lcl in
+  let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in
   abstract_tactic (TacInductionDestruct (isrec,ev,lcl'))
     (induction_destruct isrec ev lcl)
-let h_new_induction ev c e idl cl =
-  h_induction_destruct true ev ([c,e,idl],cl)
-let h_new_destruct ev c e idl cl = h_induction_destruct false ev ([c,e,idl],cl)
+let h_new_induction ev c idl e cl =
+  h_induction_destruct true ev ([c,idl],e,cl)
+let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl)
 
 let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d)
 let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index cffe84252..3028d3a1e 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -68,19 +68,19 @@ val h_simple_induction   : quantified_hypothesis -> tactic
 val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic
 val h_new_induction   : evars_flag ->
-  (evar_map * constr with_bindings) induction_arg list ->
-  constr with_bindings option ->
+  (evar_map * constr with_bindings) induction_arg ->
   intro_pattern_expr located option * intro_pattern_expr located option ->
+  constr with_bindings option ->
   Locus.clause option -> tactic
 val h_new_destruct    : evars_flag ->
-  (evar_map * constr with_bindings) induction_arg list ->
-  constr with_bindings option ->
+  (evar_map * constr with_bindings) induction_arg ->
   intro_pattern_expr located option * intro_pattern_expr located option ->
+  constr with_bindings option ->
   Locus.clause option -> tactic
 val h_induction_destruct : rec_flag -> evars_flag ->
-  ((evar_map * constr with_bindings) induction_arg list *
-   constr with_bindings option *
+  ((evar_map * constr with_bindings) induction_arg *
    (intro_pattern_expr located option * intro_pattern_expr located option)) list
+    * constr with_bindings option
     * Locus.clause option -> tactic
 
 val h_specialize      : int option -> constr with_bindings -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2beba9888..3eddb1aae 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -732,12 +732,12 @@ let rec intern_atomic lf ist x =
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) ->
       TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h)
-  | TacInductionDestruct (ev,isrec,(l,cls)) ->
-      TacInductionDestruct (ev,isrec,(List.map (fun (lc,cbo,(ipato,ipats)) ->
-	      (List.map (intern_induction_arg ist) lc,
-               Option.map (intern_constr_with_bindings ist) cbo,
+  | TacInductionDestruct (ev,isrec,(l,el,cls)) ->
+      TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats)) ->
+	      (intern_induction_arg ist c,
                (Option.map (intern_intro_pattern lf ist) ipato,
 	        Option.map (intern_intro_pattern lf ist) ipats))) l,
+               Option.map (intern_constr_with_bindings ist) el,
                Option.map (clause_app (intern_hyp_location ist)) cls))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
@@ -2424,17 +2424,17 @@ and interp_atomic ist gl tac =
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) ->
       h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
-  | TacInductionDestruct (isrec,ev,(l,cls)) ->
+  | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
       let sigma, l =
-        list_fold_map (fun sigma (lc,cbo,(ipato,ipats)) ->
-          let lc = List.map (interp_induction_arg ist gl) lc in
-	  let sigma,cbo =
-            Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
-          (sigma,(lc,cbo,
+        list_fold_map (fun sigma (c,(ipato,ipats)) ->
+          let c = interp_induction_arg ist gl c in
+          (sigma,(c,
             (Option.map (interp_intro_pattern ist gl) ipato,
 	     Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in
+      let sigma,el =
+        Option.fold_map (interp_constr_with_bindings ist env) sigma el in
       let cls = Option.map (interp_clause ist gl) cls in
-      tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,cls)
+      tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
       let h2 = interp_quantified_hypothesis ist h2 in
@@ -2862,10 +2862,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) as x -> x
-  | TacInductionDestruct (isrec,ev,(l,cls)) ->
-      TacInductionDestruct (isrec,ev,(List.map (fun (lc,cbo,ids) ->
-	List.map (subst_induction_arg subst) lc,
-        Option.map (subst_glob_with_bindings subst) cbo, ids) l, cls))
+  | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
+      let l' = List.map (fun (c,ids) -> subst_induction_arg subst c, ids) l in
+      let el' = Option.map (subst_glob_with_bindings subst) el in
+      TacInductionDestruct (isrec,ev,(l',el',cls))
   | TacDoubleInduction (h1,h2) as x -> x
   | TacDecomposeAnd c -> TacDecomposeAnd (subst_glob_constr subst c)
   | TacDecomposeOr c -> TacDecomposeOr (subst_glob_constr subst c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ad44171da..44bda9aac 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3207,12 +3207,19 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
   end
 
 let induction_destruct isrec with_evars = function
-  | [],_ -> tclIDTAC
-  | [a,b,c],cl -> induct_destruct isrec with_evars (a,b,c,cl)
-  | (a,b,c)::l,cl ->
+  | [],_,_ -> tclIDTAC
+  | [a,b],el,cl -> induct_destruct isrec with_evars ([a],el,b,cl)
+  | (a,b)::l,None,cl ->
       tclTHEN
-        (induct_destruct isrec with_evars (a,b,c,cl))
-        (tclMAP (fun (a,b,c) -> induct_destruct false with_evars (a,b,c,cl)) l)
+        (induct_destruct isrec with_evars ([a],None,b,cl))
+        (tclMAP (fun (a,b) -> induct_destruct false with_evars ([a],None,b,cl)) l)
+  | l,Some el,cl ->
+      let check_basic_using = function
+        | a,(None,None) -> a
+	| _ -> error "Unsupported syntax for \"using\"."
+      in
+      let l' = List.map check_basic_using l in
+      induct_destruct isrec with_evars (l', Some el, (None,None), cl)
 
 let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls)
 let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6cdac9d55..b1abb67a9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -295,10 +295,10 @@ val new_destruct : evars_flag ->
 (** {6 Generic case analysis / induction tactics. } *)
 
 val induction_destruct : rec_flag -> evars_flag ->
-  ((evar_map * constr with_bindings) induction_arg list *
-  constr with_bindings option *
+  ((evar_map * constr with_bindings) induction_arg *
   (intro_pattern_expr located option * intro_pattern_expr located option))
   list *
+  constr with_bindings option *
   clause option -> tactic
 
 (** {6 Eliminations giving the type instead of the proof. } *)
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index f6801da20..d7dd987fb 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -202,7 +202,7 @@ Lemma nat_compare_spec :
   forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y).
 Proof.
  intros.
- destruct (nat_compare x y) as [ ]_eqn; constructor.
+ destruct (nat_compare x y) eqn:?; constructor.
  apply nat_compare_eq; auto.
  apply <- nat_compare_lt; auto.
  apply <- nat_compare_gt; auto.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 0c44cfaf1..f779e0772 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -73,7 +73,7 @@ Qed.
 
 Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
 Proof.
-  intros; induction n m using nat_double_ind; simpl; auto with arith.
+  intros; induction n, m using nat_double_ind; simpl; auto with arith.
   rewrite <- minus_plus_simpl_l_reverse; auto with arith.
 Qed.
 Hint Resolve mult_minus_distr_r: arith v62.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 9b2a026c2..ad332a947 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -84,13 +84,13 @@ Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)).
 (* Similar variants of destruct *)
 
 Tactic Notation "destruct_with_eqn" constr(x) :=
-  destruct x as []_eqn.
+  destruct x eqn:?.
 Tactic Notation "destruct_with_eqn" ident(n) :=
-  try intros until n; destruct n as []_eqn.
+  try intros until n; destruct n eqn:?.
 Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=
-  destruct x as []_eqn:H.
+  destruct x eqn:H.
 Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=
-  try intros until n; destruct n as []_eqn:H.
+  try intros until n; destruct n eqn:H.
 
 (** Break every hypothesis of a certain type *)
 
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index f2b908af0..6778deffa 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -480,7 +480,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
  Proof.
   intros (s,Hs) (s',Hs').
   change ({M.Equal s s'}+{~M.Equal s s'}).
-  destruct (M.equal s s') as [ ]_eqn:H; [left|right];
+  destruct (M.equal s s') eqn:H; [left|right];
    rewrite <- M.equal_spec; congruence.
  Defined.
 
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index bcf68f1d4..d9b1fd9bb 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -662,7 +662,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction s; simpl; intros.
   split; intuition; inv.
-  destruct (f a) as [ ]_eqn:F; rewrite !InA_cons, ?IHs; intuition.
+  destruct (f a) eqn:F; rewrite !InA_cons, ?IHs; intuition.
   setoid_replace x with a; auto.
   setoid_replace a with x in F; auto; congruence.
   Qed.
@@ -674,7 +674,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   unfold For_all; induction s; simpl; intros.
   split; intros; auto. inv.
-  destruct (f a) as [ ]_eqn:F.
+  destruct (f a) eqn:F.
   rewrite IHs; auto. firstorder. inv; auto.
   setoid_replace x with a; auto.
   split; intros H'. discriminate.
@@ -688,7 +688,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   unfold Exists; induction s; simpl; intros.
   firstorder. discriminate. inv.
-  destruct (f a) as [ ]_eqn:F.
+  destruct (f a) eqn:F.
   firstorder.
   rewrite IHs; auto.
   firstorder.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 76f09c76e..fd4114cd4 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -396,7 +396,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   induction s; simpl.
   intuition; inv.
   intros.
-  destruct (f a) as [ ]_eqn:E; rewrite ?InA_cons, IHs; intuition.
+  destruct (f a) eqn:E; rewrite ?InA_cons, IHs; intuition.
   setoid_replace x with a; auto.
   setoid_replace a with x in E; auto. congruence.
   Qed.
@@ -420,7 +420,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   unfold For_all; induction s; simpl.
   intuition. inv.
   intros; inv.
-  destruct (f a) as [ ]_eqn:F.
+  destruct (f a) eqn:F.
   rewrite IHs; intuition. inv; auto.
   setoid_replace x with a; auto.
   split; intros H'; try discriminate.
@@ -436,7 +436,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   unfold Exists; induction s; simpl.
   split; [discriminate| intros (x & Hx & _); inv].
   intros.
-  destruct (f a) as [ ]_eqn:F.
+  destruct (f a) eqn:F.
   split; auto.
   exists a; auto.
   rewrite IHs; firstorder.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index d1c817f54..6b4e154c0 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -416,7 +416,7 @@ Module Make (NN:NType) <: ZType.
  Ltac break_nonneg x px EQx :=
   let H := fresh "H" in
   assert (H:=NN.spec_pos x);
-  destruct (NN.to_Z x) as [|px|px]_eqn:EQx;
+  destruct (NN.to_Z x) as [|px|px] eqn:EQx;
    [clear H|clear H|elim H; reflexivity].
 
  Theorem spec_div_eucl: forall x y,
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index ad7a9f3ae..cabba1131 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -376,7 +376,7 @@ Lemma log_good_step : forall n h1 h2,
   (if n << 2 then 0 else S (h2 (half n))).
 Proof.
 intros n h1 h2 E.
-destruct (n<<2) as [ ]_eqn:H.
+destruct (n<<2) eqn:H.
 auto with *.
 f_equiv. apply E, half_decrease.
 rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index 7124cd536..695291b8c 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -131,7 +131,7 @@ Theorem Sorted_merge : forall l1 l2,
   Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2).
 Proof.
 induction l1; induction l2; intros; simpl; auto.
-  destruct (a <=? a0) as ()_eqn:Heq1.
+  destruct (a <=? a0) eqn:Heq1.
     invert H.
       simpl. constructor; trivial; rewrite Heq1; constructor.
       assert (Sorted (merge (b::l) (a0::l2))) by (apply IHl1; auto).
diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v
index 85e7fb176..5dd917a71 100644
--- a/theories/Structures/OrdersAlt.v
+++ b/theories/Structures/OrdersAlt.v
@@ -140,7 +140,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
  Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
  Proof.
   unfold lt, eq; intros x y z Hxy Hyz.
-  destruct (compare x z) as [ ]_eqn:Hxz; auto.
+  destruct (compare x z) eqn:Hxz; auto.
   rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
   rewrite (compare_trans Hxz Hyz) in Hxy; discriminate.
   rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
@@ -150,7 +150,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
  Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
  Proof.
   unfold lt, eq; intros x y z Hxy Hyz.
-  destruct (compare x z) as [ ]_eqn:Hxz; auto.
+  destruct (compare x z) eqn:Hxz; auto.
   rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
   rewrite (compare_trans Hxy Hxz) in Hyz; discriminate.
   rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
@@ -169,7 +169,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
  Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
  Proof.
   unfold eq, lt, compare; intros.
-  destruct (O.compare x y) as [ ]_eqn:H; auto.
+  destruct (O.compare x y) eqn:H; auto.
   apply CompGt.
   rewrite compare_sym, H; auto.
  Qed.