Only one "in" clause in "destruct" even for a multiple "destruct".

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

5 files changed, 28 insertions, 28 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 73aeec501..d642a38db 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -83,12 +83,12 @@ let h_simple_induction_destruct isrec h =
 let h_simple_induction = h_simple_induction_destruct true
 let h_simple_destruct = h_simple_induction_destruct false
 
-let h_induction_destruct isrec ev l =
-  abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) ->
-    List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l))
-    (induction_destruct ev isrec l)
-let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl]
-let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl]
+let h_induction_destruct isrec ev (l,cl) =
+  abstract_tactic (TacInductionDestruct (isrec,ev,(List.map (fun (c,e,idl) ->
+    List.map inj_ia c,Option.map inj_open_wb e,idl) l,cl)))
+    (induction_destruct ev isrec (l,cl))
+let h_new_induction ev c e idl cl = h_induction_destruct ev true ([c,e,idl],cl)
+let h_new_destruct ev c e idl cl = h_induction_destruct ev false ([c,e,idl],cl)
 
 let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d)
 let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index f4da57144..86a337678 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -78,8 +78,8 @@ val h_new_destruct    : evars_flag ->
   Tacticals.clause option -> tactic
 val h_induction_destruct : rec_flag -> evars_flag ->
   (constr with_ebindings induction_arg list * constr with_ebindings option *
-   (intro_pattern_expr located option * intro_pattern_expr located option) *
-   Tacticals.clause option) list -> tactic
+   (intro_pattern_expr located option * intro_pattern_expr located option)) list
+    * Tacticals.clause option -> tactic
 
 val h_specialize      : int option -> constr with_ebindings -> tactic
 val h_lapply          : constr -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8d8b94c6c..427a6eaa6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -736,13 +736,13 @@ let rec intern_atomic lf ist x =
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) ->
       TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h)
-  | TacInductionDestruct (ev,isrec,l) ->
-      TacInductionDestruct (ev,isrec,List.map (fun (lc,cbo,(ipato,ipats),cls) ->
+  | 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,
                (Option.map (intern_intro_pattern lf ist) ipato,
-	        Option.map (intern_intro_pattern lf ist) ipats),
-               Option.map (clause_app (intern_hyp_location ist)) cls)) l)
+	        Option.map (intern_intro_pattern lf ist) ipats))) l,
+               Option.map (clause_app (intern_hyp_location ist)) cls))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
       let h2 = intern_quantified_hypothesis ist h2 in
@@ -2281,14 +2281,14 @@ and interp_atomic ist gl = function
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) ->
       h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
-  | TacInductionDestruct (isrec,ev,l) ->
+  | TacInductionDestruct (isrec,ev,(l,cls)) ->
       h_induction_destruct ev isrec
-      (List.map (fun (lc,cbo,(ipato,ipats),cls) ->
+      (List.map (fun (lc,cbo,(ipato,ipats)) ->
 	(List.map (interp_induction_arg ist gl) lc,
          Option.map (interp_constr_with_bindings ist gl) cbo,
          (Option.map (interp_intro_pattern ist gl) ipato,
-	  Option.map (interp_intro_pattern ist gl) ipats),
-         Option.map (interp_clause ist gl) cls)) l)
+	  Option.map (interp_intro_pattern ist gl) ipats))) l,
+         Option.map (interp_clause ist gl) cls)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
       let h2 = interp_quantified_hypothesis ist h2 in
@@ -2617,10 +2617,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) ->
-      TacInductionDestruct (isrec,ev,List.map (fun (lc,cbo,ids,cls) ->
+  | TacInductionDestruct (isrec,ev,(l,cls)) ->
+      TacInductionDestruct (isrec,ev,(List.map (fun (lc,cbo,ids) ->
 	List.map (subst_induction_arg subst) lc,
-        Option.map (subst_raw_with_bindings subst) cbo, ids, cls) l)
+        Option.map (subst_raw_with_bindings subst) cbo, ids) l, cls))
   | TacDoubleInduction (h1,h2) as x -> x
   | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
   | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8e920ef64..35f3b40d4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2919,12 +2919,12 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) =
   else induct_destruct_l isrec with_evars lc elim names cls
 
 let induction_destruct isrec with_evars = function
-  | [] -> tclIDTAC
-  | [a] -> induct_destruct isrec with_evars a
-  | a::l ->
+  | [],_ -> tclIDTAC
+  | [a,b,c],cl -> induct_destruct isrec with_evars (a,b,c,cl)
+  | (a,b,c)::l,cl ->
       tclTHEN
-        (induct_destruct isrec with_evars a)
-        (tclMAP (induct_destruct false with_evars) l)
+        (induct_destruct isrec with_evars (a,b,c,cl))
+        (tclMAP (fun (a,b,c) -> induct_destruct false with_evars (a,b,c,cl)) l)
 
 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 40ff0b688..cedcbf7ca 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -289,12 +289,12 @@ val new_destruct : evars_flag -> constr with_ebindings induction_arg list ->
 
 (*s Generic case analysis / induction tactics. *)
 
-val induction_destruct : evars_flag -> rec_flag ->
+val induction_destruct : rec_flag -> evars_flag ->
   (constr with_ebindings induction_arg list *
   constr with_ebindings option *
-  (intro_pattern_expr located option * intro_pattern_expr located option) *
-  clause option) list ->
-    tactic
+  (intro_pattern_expr located option * intro_pattern_expr located option))
+  list *
+  clause option -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)