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

5 files changed, 39 insertions, 32 deletions

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. } *)