Stronger invariants on the use of the introduction pattern (pat1,...,patn).

The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.

Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.

17 files changed, 177 insertions, 81 deletions

diff --git a/CHANGES b/CHANGES
index cda16d380..e80a3b454 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,9 @@ Tactics
   incompatibilities as soon as the inductive types have dependencies in
   the type of their constructors; "double induction" remains however
   deprecated).
+- In introduction patterns of the form (pat1,...,patn), n should match
+  the exact number of hypotheses introduced (except for local definitions
+  for which pattern can be omitted, as in regular pattern-matching).
 
 Program
 
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 65c7dccf2..889dc5444 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -16,6 +16,8 @@ type patvar = Id.t
 
 (** Introduction patterns *)
 
+type tuple_flag = bool (* tells pattern list should be list of fixed length *)
+
 type 'constr intro_pattern_expr =
   | IntroForthcoming of bool
   | IntroNaming of intro_pattern_naming_expr
@@ -31,7 +33,8 @@ and 'constr intro_pattern_action_expr =
   | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr)
   | IntroRewrite of bool
 and 'constr or_and_intro_pattern_expr =
-  (Loc.t * 'constr intro_pattern_expr) list list
+  | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list
+  | IntroAndPattern of (Loc.t * 'constr intro_pattern_expr) list
 
 (** Move destination for hypothesis *)
 
diff --git a/lib/cList.ml b/lib/cList.ml
index bd3e09b5b..ba592d13f 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -48,6 +48,7 @@ sig
   val filteri :
     (int -> 'a -> bool) -> 'a list -> 'a list
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
+  val extend : bool list -> 'a -> 'a list -> 'a list
   val count : ('a -> bool) -> 'a list -> int
   val index : 'a eq -> 'a -> 'a list -> int
   val index0 : 'a eq -> 'a -> 'a list -> int
@@ -376,6 +377,12 @@ let rec smartfilter f l = match l with
           else h :: tl'
         else tl'
 
+let rec extend l a l' = match l,l' with
+  | true::l, b::l' -> b :: extend l a l'
+  | false::l, l' -> a :: extend l a l'
+  | [], [] -> []
+  | _ -> invalid_arg "extend"
+
 let count f l =
   let rec aux acc = function
     | [] -> acc
diff --git a/lib/cList.mli b/lib/cList.mli
index 1487f67a3..9c7b815c1 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -94,6 +94,9 @@ sig
   (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
     [f ai = true], then [smartfilter f l == l] *)
 
+  val extend : bool list -> 'a -> 'a list -> 'a list
+(** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n];
+    it extends [a1..an] by inserting [a] at the position of [false] in [l] *)
   val count : ('a -> bool) -> 'a list -> int
 
   val index : 'a eq -> 'a -> 'a list -> int
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a7b05dd5e..77d74892d 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -285,18 +285,19 @@ GEXTEND Gram
     [ [ l = LIST1 nonsimple_intropattern -> l ]]
   ;
   or_and_intropattern:
-    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> tc
-      | "()" -> [[]]
-      | "("; si = simple_intropattern; ")" -> [[si]]
+    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> IntroOrPattern tc
+      | "()" -> IntroAndPattern []
+      | "("; si = simple_intropattern; ")" -> IntroAndPattern [si]
       | "("; si = simple_intropattern; ",";
-             tc = LIST1 simple_intropattern SEP "," ; ")" -> [si::tc]
+             tc = LIST1 simple_intropattern SEP "," ; ")" ->
+             IntroAndPattern (si::tc)
       | "("; si = simple_intropattern; "&";
 	     tc = LIST1 simple_intropattern SEP "&" ; ")" ->
 	  (* (A & B & C) is translated into (A,(B,C)) *)
 	  let rec pairify = function
-	    | ([]|[_]|[_;_]) as l -> [l]
-	    | t::q -> [[t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (pairify q)))]]
-	  in pairify (si::tc) ] ]
+	    | ([]|[_]|[_;_]) as l -> l
+	    | t::q -> [t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
+	  in IntroAndPattern (pairify (si::tc)) ] ]
   ;
   equality_intropattern:
     [ [ "->" -> IntroRewrite true
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index d09af6d2a..be3e62574 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -33,9 +33,9 @@ and pr_intro_pattern_action prc = function
   | IntroRewrite false -> str "<-"
 
 and pr_or_and_intro_pattern prc = function
-  | [pl] ->
+  | IntroAndPattern pl ->
       str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")"
-  | pll ->
+  | IntroOrPattern pll ->
       str "[" ++
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
       ++ str "]"
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 3574990f6..01124e867 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -296,17 +296,17 @@ let get_names (allow_conj,issimple) (loc, pat as x) = match pat with
       error "Discarding pattern not allowed for inversion equations."
   | IntroAction (IntroRewrite _) ->
       error "Rewriting pattern not allowed for inversion equations."
-  | IntroAction (IntroOrAndPattern [[]]) when allow_conj -> (None, [])
-  | IntroAction (IntroOrAndPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l])
+  | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, [])
+  | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l)))
       when allow_conj -> (Some id,l)
-  | IntroAction (IntroOrAndPattern [_]) ->
+  | IntroAction (IntroOrAndPattern (IntroAndPattern _)) ->
       if issimple then
         error"Conjunctive patterns not allowed for simple inversion equations."
       else
         error"Nested conjunctive patterns not allowed for inversion equations."
   | IntroAction (IntroInjection l) ->
       error "Injection patterns not allowed for inversion equations."
-  | IntroAction (IntroOrAndPattern l) ->
+  | IntroAction (IntroOrAndPattern (IntroOrPattern _)) ->
       error "Disjunctive patterns not allowed for inversion equations."
   | IntroAction (IntroApplyOn (c,pat)) ->
       error "Apply patterns not allowed for inversion equations."
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 14e0fed31..f92213da8 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -258,8 +258,11 @@ and intern_intro_pattern_action lf ist = function
   | IntroApplyOn (c,pat) ->
       IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat)
 
-and intern_or_and_intro_pattern lf ist =
-  List.map (List.map (intern_intro_pattern lf ist))
+and intern_or_and_intro_pattern lf ist = function
+   | IntroAndPattern l ->
+      IntroAndPattern (List.map (intern_intro_pattern lf ist) l)
+  | IntroOrPattern ll ->
+      IntroOrPattern (List.map (List.map (intern_intro_pattern lf ist)) ll)
 
 let intern_or_and_intro_pattern_loc lf ist = function
   | ArgVar (_,id) as x ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8db91c07f..a6991691f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -511,7 +511,9 @@ let extract_ltac_constr_values ist env =
 (* Extract the identifier list from lfun: join all branches (what to do else?)*)
 let rec intropattern_ids (loc,pat) = match pat with
   | IntroNaming (IntroIdentifier id) -> [id]
-  | IntroAction (IntroOrAndPattern ll) ->
+  | IntroAction (IntroOrAndPattern (IntroAndPattern l)) ->
+      List.flatten (List.map intropattern_ids l)
+  | IntroAction (IntroOrAndPattern (IntroOrPattern ll)) ->
       List.flatten (List.map intropattern_ids (List.flatten ll))
   | IntroAction (IntroInjection l) ->
       List.flatten (List.map intropattern_ids l)
@@ -940,8 +942,13 @@ and interp_intro_pattern_action ist env sigma = function
       sigma, IntroApplyOn (c,ipat)
   | IntroWildcard | IntroRewrite _ as x -> sigma, x
 
-and interp_or_and_intro_pattern ist env sigma =
-  List.fold_map (interp_intro_pattern_list_as_list ist env) sigma
+and interp_or_and_intro_pattern ist env sigma = function
+  | IntroAndPattern l ->
+      let sigma, l = List.fold_map (interp_intro_pattern ist env) sigma l in
+      sigma, IntroAndPattern l
+  | IntroOrPattern ll ->
+      let sigma, ll = List.fold_map (interp_intro_pattern_list_as_list ist env) sigma ll in
+      sigma, IntroOrPattern ll
 
 and interp_intro_pattern_list_as_list ist env sigma = function
   | [loc,IntroNaming (IntroIdentifier id)] as l ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index c74f6093a..e09360a6a 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -54,10 +54,16 @@ and subst_intro_pattern_action subst = function
   | IntroApplyOn (t,pat) ->
       IntroApplyOn (subst_glob_constr subst t,subst_intro_pattern subst pat)
   | IntroOrAndPattern l ->
-      IntroOrAndPattern (List.map (List.map (subst_intro_pattern subst)) l)
+      IntroOrAndPattern (subst_intro_or_and_pattern subst l)
   | IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l)
   | IntroWildcard | IntroRewrite _ as x -> x
 
+and subst_intro_or_and_pattern subst = function
+  | IntroAndPattern l ->
+      IntroAndPattern (List.map (subst_intro_pattern subst) l)
+  | IntroOrPattern ll ->
+      IntroOrPattern (List.map (List.map (subst_intro_pattern subst)) ll)
+
 let subst_induction_arg subst = function
   | clear,ElimOnConstr c -> clear,ElimOnConstr (subst_glob_with_bindings subst c)
   | clear,ElimOnAnonHyp n as x -> x
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 061c05b9b..4029d1fcc 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -147,51 +147,85 @@ type branch_args = {
   largs      : constr list; (* its arguments *)
   branchnum  : int;         (* the branch number *)
   pred       : constr;      (* the predicate we used *)
-  nassums    : int;         (* the number of assumptions to be introduced *)
+  nassums    : int;         (* number of assumptions/letin to be introduced *)
   branchsign : bool list;   (* the signature of the branch.
-                               true=recursive argument, false=constant *)
+                               true=assumption, false=let-in *)
   branchnames : Tacexpr.intro_patterns}
 
 type branch_assumptions = {
   ba        : branch_args;       (* the branch args *)
   assums    : Context.Named.t}   (* the list of assumptions introduced *)
 
+open Misctypes
+
 let fix_empty_or_and_pattern nv l =
   (* 1- The syntax does not distinguish between "[ ]" for one clause with no
      names and "[ ]" for no clause at all *)
   (* 2- More generally, we admit "[ ]" for any disjunctive pattern of
      arbitrary length *)
   match l with
-  | [[]] -> List.make nv []
+  | IntroOrPattern [[]] -> IntroOrPattern (List.make nv [])
   | _ -> l
 
-let check_or_and_pattern_size loc names n =
-  if not (Int.equal (List.length names) n) then
-    if Int.equal n 1 then
-      user_err_loc (loc,"",str "Expects a conjunctive pattern.")
-    else
-      user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n
-	++ str " branches.")
-
-let compute_induction_names n = function
+let check_or_and_pattern_size loc names branchsigns =
+  let n = Array.length branchsigns in
+  let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in
+  let err1 p1 p2 =
+    user_err_loc (loc,"",str "Expects " ++ msg p1 p2 ++ str ".") in
+  let errn n =
+    user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n
+	++ str " branches.") in
+  let err1' p1 p2 =
+    user_err_loc (loc,"",strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
+  match names with
+  | IntroAndPattern l ->
+      if not (Int.equal n 1) then errn n;
+      let p1 = List.count (fun x -> x) branchsigns.(0) in
+      let p2 = List.length branchsigns.(0) in
+      let p = List.length l in
+      if not (Int.equal p p1 || Int.equal p p2) ||
+         not (List.for_all (function _,IntroNaming _ | _,IntroAction _ -> true | _,IntroForthcoming _ -> false) l) then err1 p1 p2;
+      if Int.equal p p1 then
+        IntroAndPattern
+          (List.extend branchsigns.(0) (Loc.ghost,IntroNaming IntroAnonymous) l)
+      else
+        names
+  | IntroOrPattern ll ->
+      if not (Int.equal n (List.length ll)) then
+        if Int.equal n 1 then
+          let p1 = List.count (fun x -> x) branchsigns.(0) in
+          let p2 = List.length branchsigns.(0) in
+          err1' p1 p2 else errn n;
+      names
+
+let get_and_check_or_and_pattern loc names branchsigns =
+  let names = check_or_and_pattern_size loc names branchsigns in
+  match names with
+  | IntroAndPattern l -> [|l|]
+  | IntroOrPattern l -> Array.of_list l
+
+let compute_induction_names branchletsigns = function
   | None ->
-      Array.make n []
+      Array.make (Array.length branchletsigns) []
   | Some (loc,names) ->
-      let names = fix_empty_or_and_pattern n names in
-      check_or_and_pattern_size loc names n;
-      Array.of_list names
+      let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in
+      get_and_check_or_and_pattern loc names branchletsigns
 
-let compute_construtor_signatures isrec ((_,k as ity),u) =
+(* Compute the let-in signature of case analysis or standard induction scheme *)
+let compute_constructor_signatures isrec ((_,k as ity),u) =
   let rec analrec c recargs =
     match kind_of_term c, recargs with
     | Prod (_,_,c), recarg::rest ->
-	let b = match Declareops.dest_recarg recarg with
-	  | Norec | Imbr _  -> false
-	  | Mrec (_,j)  -> isrec && Int.equal j k
-	in b :: (analrec c rest)
-    | LetIn (_,_,_,c), rest -> false :: (analrec c rest)
+        let rest = analrec c rest in
+        begin match Declareops.dest_recarg recarg with
+        | Norec | Imbr _  -> true :: rest
+        | Mrec (_,j)  ->
+            if isrec && Int.equal j k then true :: true :: rest
+            else true :: rest
+        end
+    | LetIn (_,_,_,c), rest -> false :: analrec c rest
     | _, [] -> []
-    | _ -> anomaly (Pp.str "compute_construtor_signatures")
+    | _ -> anomaly (Pp.str "compute_constructor_signatures")
   in
   let (mib,mip) = Global.lookup_inductive ity in
   let n = mib.mind_nparams in
@@ -596,8 +630,8 @@ module New = struct
             (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
-    let branchsigns = compute_construtor_signatures isrec ind in
-    let brnames = compute_induction_names (Array.length branchsigns) allnames in
+    let branchsigns = compute_constructor_signatures isrec ind in
+    let brnames = compute_induction_names branchsigns allnames in
     let flags = Unification.elim_flags () in
     let elimclause' =
       match predicate with
@@ -609,10 +643,7 @@ module New = struct
       let (hd,largs) = decompose_app clenv'.templtyp.Evd.rebus in
       let ba = { branchsign = branchsigns.(i);
                  branchnames = brnames.(i);
-                 nassums =
-          List.fold_left
-            (fun acc b -> if b then acc+2 else acc+1)
-            0 branchsigns.(i);
+                 nassums = List.length branchsigns.(i);
                  branchnum = i+1;
                  ity = ind;
                  largs = List.map (clenv_nf_meta clenv') largs;
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 147f1f0f2..4f6f87f69 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -102,28 +102,32 @@ type branch_args = {
   largs      : constr list; (** its arguments *)
   branchnum  : int;         (** the branch number *)
   pred       : constr;      (** the predicate we used *)
-  nassums    : int;         (** the number of assumptions to be introduced *)
+  nassums    : int;         (** number of assumptions/letin to be introduced *)
   branchsign : bool list;   (** the signature of the branch.
-                                true=recursive argument, false=constant *)
+                                true=assumption, false=let-in *)
   branchnames : intro_patterns}
 
 type branch_assumptions = {
   ba        : branch_args;       (** the branch args *)
   assums    : Context.Named.t}   (** the list of assumptions introduced *)
 
-(** [check_disjunctive_pattern_size loc pats n] returns an appropriate 
-   error message if |pats| <> n *)
-val check_or_and_pattern_size :
-  Loc.t -> delayed_open_constr or_and_intro_pattern_expr -> int -> unit
+(** [check_disjunctive_pattern_size loc pats n] returns an appropriate
+   error message if |pats| <> n; extends them if no pattern is given
+   for let-ins in the case of a conjunctive pattern *)
+val get_and_check_or_and_pattern : 
+  Loc.t -> delayed_open_constr or_and_intro_pattern_expr ->
+  bool list array -> intro_patterns array
 
 (** Tolerate "[]" to mean a disjunctive pattern of any length *)
 val fix_empty_or_and_pattern : int -> 
   delayed_open_constr or_and_intro_pattern_expr ->
   delayed_open_constr or_and_intro_pattern_expr
 
+val compute_constructor_signatures : rec_flag -> pinductive -> bool list array
+
 (** Useful for [as intro_pattern] modifier *)
 val compute_induction_names :
-  int -> or_and_intro_pattern option -> intro_patterns array
+  bool list array -> or_and_intro_pattern option -> intro_patterns array
 
 val elimination_sort_of_goal : goal sigma -> sorts_family
 val elimination_sort_of_hyp  : Id.t -> goal sigma -> sorts_family
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f0f46c14d..796cea98f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2089,14 +2089,15 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
   Proofview.Goal.enter { enter = begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
-  let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
-  let nv = constructors_nrealdecls ind in
-  let ll = fix_empty_or_and_pattern (Array.length nv) ll in
-  check_or_and_pattern_size loc ll (Array.length nv);
+  let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
+  let branchsigns = compute_constructor_signatures false ind in
+  let nv_with_let = Array.map List.length branchsigns in
+  let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
+  let ll = get_and_check_or_and_pattern loc ll branchsigns in
   Tacticals.New.tclTHENLASTn
     (Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id])))
     (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
-       nv (Array.of_list ll))
+       nv_with_let ll)
   end }
 
 let rewrite_hyp assert_style l2r id =
@@ -2137,7 +2138,8 @@ let prepare_naming loc = function
 let rec explicit_intro_names = function
 | (_, IntroForthcoming _) :: l -> explicit_intro_names l
 | (_, IntroNaming (IntroIdentifier id)) :: l -> id :: explicit_intro_names l
-| (_, IntroAction (IntroOrAndPattern ll)) :: l' ->
+| (_, IntroAction (IntroOrAndPattern l)) :: l' ->
+    let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in
     List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
 | (_, IntroAction (IntroInjection l)) :: l' ->
     explicit_intro_names (l@l')
@@ -2842,8 +2844,8 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
   let avoid = avoid @ avoid' in
   let rec peel_tac ra dests names thin =
     match ra with
-    | (RecArg,deprec,recvarname) ::
-        (IndArg,depind,hyprecname) :: ra' ->
+    | (RecArg,_,deprec,recvarname) ::
+        (IndArg,_,depind,hyprecname) :: ra' ->
         Proofview.Goal.enter { enter = begin fun gl ->
         let (recpat,names) = match names with
           | [loc,IntroNaming (IntroIdentifier id) as pat] ->
@@ -2860,7 +2862,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 	    peel_tac ra' (update_dest dests ids') names thin)
         end })
         end }
-    | (IndArg,dep,hyprecname) :: ra' ->
+    | (IndArg,_,dep,hyprecname) :: ra' ->
         Proofview.Goal.enter { enter = begin fun gl ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
         let pat,names =
@@ -2868,7 +2870,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 	dest_intro_patterns avoid thin MoveLast [pat] (fun ids thin ->
         peel_tac ra' (update_dest dests ids) names thin)
         end }
-    | (RecArg,dep,recvarname) :: ra' ->
+    | (RecArg,_,dep,recvarname) :: ra' ->
         Proofview.Goal.enter { enter = begin fun gl ->
         let (pat,names) =
           consume_pattern avoid (Name recvarname) dep gl names in
@@ -2876,7 +2878,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 	dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
         peel_tac ra' dests names thin)
         end }
-    | (OtherArg,dep,_) :: ra' ->
+    | (OtherArg,_,dep,_) :: ra' ->
         Proofview.Goal.enter { enter = begin fun gl ->
         let (pat,names) = consume_pattern avoid Anonymous dep gl names in
         let dest = get_recarg_dest dests in
@@ -3682,9 +3684,9 @@ let compute_scheme_signature scheme names_info ind_type_guess =
   let rec check_branch p c =
     match kind_of_term c with
       | Prod (_,t,c) ->
-	(is_pred p t, dependent (mkRel 1) c) :: check_branch (p+1) c
+	(is_pred p t, true, dependent (mkRel 1) c) :: check_branch (p+1) c
       | LetIn (_,_,_,c) ->
-	(OtherArg, dependent (mkRel 1) c) :: check_branch (p+1) c
+	(OtherArg, false, dependent (mkRel 1) c) :: check_branch (p+1) c
       | _ when is_pred p c == IndArg -> []
       | _ -> raise Exit
   in
@@ -3694,12 +3696,12 @@ let compute_scheme_signature scheme names_info ind_type_guess =
 	(try
 	   let lchck_brch = check_branch p t in
 	   let n = List.fold_left
-	     (fun n (b,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in
+	     (fun n (b,_,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in
 	   let recvarname, hyprecname, avoid =
 	     make_up_names n scheme.indref names_info in
 	   let namesign =
-	     List.map (fun (b,dep) ->
-	       (b, dep, if b == IndArg then hyprecname else recvarname))
+	     List.map (fun (b,is_assum,dep) ->
+	       (b,is_assum,dep,if b == IndArg then hyprecname else recvarname))
 	       lchck_brch in
 	   (avoid,namesign) :: find_branches (p+1) brs
 	 with Exit-> error_ind_scheme "the branches of")
@@ -3744,7 +3746,7 @@ let given_elim hyp0 (elimc,lbind as e) gl =
   Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
 
 type scheme_signature =
-    (Id.t list * (elim_arg_kind * bool * Id.t) list) array
+    (Id.t list * (elim_arg_kind * bool * bool * Id.t) list) array
 
 type eliminator_source =
   | ElimUsing of (eliminator * types) * scheme_signature
@@ -3865,7 +3867,10 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
       List.fold_left
         (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in
     let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in
-    let names = compute_induction_names (Array.length indsign) names in
+    let branchletsigns =
+      let f (_,is_not_let,_,_) = is_not_let in
+      Array.map (fun (_,l) -> List.map f l) indsign in
+    let names = compute_induction_names branchletsigns names in
     let tac =
     (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
       (Tacticals.New.tclTHENLIST [
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index af5f99401..ee69df977 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -105,3 +105,26 @@ Inductive I := C : let x:=1 in x=1 -> I.
 Goal I -> True.
 intros [x H]. (* Was failing in 8.5 *)
 Abort.
+
+(* Ensuring that the (pat1,...,patn) intropatterns has the expected size, up
+   to skipping let-ins *)
+
+Goal I -> 1=1.
+intros (H).  (* This skips x *)
+exact H.
+Qed.
+
+Goal I -> 1=1.
+Fail intros (x,H,H').
+Fail intros [|].
+intros (x,H).
+exact H.
+Qed.
+
+Goal Acc le 0 -> True.
+Fail induction 1 as (n,H). (* Induction hypothesis is missing *)
+induction 1 as (n,H,IH).
+exact Logic.I.
+Qed.
+
+
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index fcb4e7876..ba7da256d 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -321,7 +321,7 @@ Proof.
   induction H; intros; try (injection Heqm; intros; subst; clear Heqm);
     discriminate || (try tauto).
   apply Permutation_length_1_inv in H as ->; left; auto.
-  apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as ();
+  apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as [];
     auto.
 Qed.
 
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index b8b9e929c..e05dab7a4 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -75,7 +75,7 @@ Section Wf_Lexicographic_Exponentiation.
   Proof.
     intros.
     inversion H.
-    - apply app_cons_not_nil in H1 as ().
+    - apply app_cons_not_nil in H1 as [].
     - assert (x ++ [a] = [x0]) by auto with sets.
       apply app_eq_unit in H0 as [(->, _)| (_, [=])].
       auto using d_nil.
@@ -98,7 +98,7 @@ Section Wf_Lexicographic_Exponentiation.
       destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)%app_inj_tail, <-).
       inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ].
     - inversion H0.
-      + apply app_cons_not_nil in H3 as ().
+      + apply app_cons_not_nil in H3 as [].
       + rewrite app_comm_cons in H0, H1. apply desc_prefix in H0.
         pose proof (H x0 b H0).
         apply rt_trans with (y := x0); auto with sets.
@@ -145,7 +145,7 @@ Section Wf_Lexicographic_Exponentiation.
           pose proof H0 as H0'.
           apply app_inj_tail in H0' as (_, ->).
           rewrite app_assoc_reverse in H0.
-          apply Hind in H0 as ().
+          apply Hind in H0 as [].
           split.
           assumption.
           apply d_conc; auto with sets.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 56106928e..2f206bfc8 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -85,7 +85,7 @@ let destruct_on c = destruct false None c None None
 
 let destruct_on_using c id =
   destruct false None c
-    (Some (dl,[[dl,IntroNaming IntroAnonymous];
+    (Some (dl,IntroOrPattern [[dl,IntroNaming IntroAnonymous];
                [dl,IntroNaming (IntroIdentifier id)]]))
     None
 
@@ -589,8 +589,8 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                          Simple.apply_in freshz (andb_prop());
                          Proofview.Goal.nf_enter { enter = begin fun gl ->
                            let fresht = fresh_id (Id.of_string "Z") gl in
-                            (destruct_on_as (mkVar freshz)
-                                  [[dl,IntroNaming (IntroIdentifier fresht);
+                            destruct_on_as (mkVar freshz)
+                                  (IntroOrPattern [[dl,IntroNaming (IntroIdentifier fresht);
                                     dl,IntroNaming (IntroIdentifier freshz)]])
                          end }
                         ]);