Constructor type information uses the expanded form.

It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.

Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.

21 files changed, 109 insertions, 84 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 4329b2d743..b681fb876e 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -89,6 +89,9 @@ let eq_recarg a1 a2 = match a1, a2 with
 
 let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equal (snd x) (snd y))
 
+let eq_in_context (ctx1, t1) (ctx2, t2) =
+  Context.Rel.equal Constr.equal ctx1 ctx2 && Constr.equal t1 t2
+
 let check_packet env mind ind
     { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc;
       mind_nrealargs; mind_nrealdecls; mind_kelim; mind_nf_lc;
@@ -105,7 +108,7 @@ let check_packet env mind ind
   check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls);
   check "mind_kelim" (check_kelim ind.mind_kelim mind_kelim);
 
-  check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc);
+  check "mind_nf_lc" (Array.equal eq_in_context ind.mind_nf_lc mind_nf_lc);
   (* NB: here syntactic equality is not just an optimisation, we also
      care about the shape of the terms *)
 
diff --git a/checker/values.ml b/checker/values.ml
index 66467fa8f5..bcac3014be 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -261,7 +261,7 @@ let v_one_ind = v_tuple "one_inductive_body"
     Int;
     Int;
     List v_sortfam;
-    Array v_constr;
+    Array (v_pair v_rctxt v_constr);
     Array Int;
     Array Int;
     v_wfp;
diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh
new file mode 100644
index 0000000000..1af8b5430d
--- /dev/null
+++ b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then
+
+    quickchick_CI_REF=context-constructor
+    quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
+
+    equations_CI_REF=context-constructor
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 24894fc9f5..7f1dc70d95 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1188,7 +1188,6 @@ let check_constructor_length env loc cstr len_pl pl0 =
       (error_wrong_numarg_constructor ?loc env cstr
          (Inductiveops.constructor_nrealargs cstr)))
 
-open Term
 open Declarations
 
 (* Similar to Cases.adjust_local_defs but on RCPat *)
@@ -1197,16 +1196,15 @@ let insert_local_defs_in_pattern (ind,j) l =
   if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
     (* Optimisation *) l
   else
-    let typi = mip.mind_nf_lc.(j-1) in
-    let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in
-    let (decls,_) = decompose_prod_assum typi in
+    let (ctx, _) = mip.mind_nf_lc.(j-1) in
+    let decls = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in
     let rec aux decls args =
       match decls, args with
       | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args
       | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *)
       | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
       | _ -> assert false in
-    aux (List.rev decls) l
+    aux decls l
 
 let add_local_defs_and_check_length loc env g pl args = match g with
   | ConstructRef cstr ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 6fd52d98dd..2c281af2d2 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -452,9 +452,10 @@ let compute_mib_implicits flags kn =
     let ind = (kn,i) in
     let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in
     ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)),
-     Array.mapi (fun j c ->
+     Array.mapi (fun j (ctx, cty) ->
+      let c = of_constr (Term.it_mkProd_or_LetIn cty ctx) in
        (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c))
-       (Array.map of_constr mip.mind_nf_lc))
+       mip.mind_nf_lc)
   in
   Array.mapi imps_one_inductive mib.mind_packets
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 6777e0c223..567850645e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -166,7 +166,7 @@ type one_inductive_body = {
 
     mind_kelim : Sorts.family list; (** List of allowed elimination sorts *)
 
-    mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
+    mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
 
     mind_consnrealargs : int array;
  (** Number of expected proper arguments of the constructors (w/o params) *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 9e0230c3ba..d56502a095 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -214,7 +214,7 @@ let subst_mind_packet sub mbp =
     mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_consnrealargs = mbp.mind_consnrealargs;
     mind_typename = mbp.mind_typename;
-    mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc;
+    mind_nf_lc = Array.Smart.map (fun (ctx, c) -> Context.Rel.map (subst_mps sub) ctx, subst_mps sub c) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
     mind_arity = subst_ind_arity sub mbp.mind_arity;
     mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc;
@@ -299,9 +299,8 @@ let hcons_ind_arity =
 
 let hcons_mind_packet oib =
   let user = Array.Smart.map Constr.hcons oib.mind_user_lc in
-  let nf = Array.Smart.map Constr.hcons oib.mind_nf_lc in
-  (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *)
-  let nf = if Array.equal (==) user nf then user else nf in
+  let map (ctx, c) = Context.Rel.map Constr.hcons ctx, Constr.hcons c in
+  let nf = Array.Smart.map map oib.mind_nf_lc in
   { oib with
     mind_typename = Names.Id.hcons oib.mind_typename;
     mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8f06e1e4b8..457c17907e 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -416,7 +416,9 @@ let compute_projections (kn, i as ind) mib =
   let pkt = mib.mind_packets.(i) in
   let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
   let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
-  let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
+  let (ctx, cty) = pkt.mind_nf_lc.(0) in
+  let cty = it_mkProd_or_LetIn cty ctx in
+  let rctx, _ = decompose_prod_assum (substl subst cty) in
   let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
   (** We build a substitution smashing the lets in the record parameters so
       that typechecking projections requires just a substitution and not
@@ -475,7 +477,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
   (* Check one inductive *)
   let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg =
     (* Type of constructors in normal form *)
-    let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b (d@paramsctxt)) splayed_lc in
+    let nf_lc = Array.map (fun (d, b) -> (d@paramsctxt, b)) splayed_lc in
     let consnrealdecls =
       Array.map (fun (d,_) -> Context.Rel.length d)
 	splayed_lc in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 848ae65c51..f4c2483c14 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -251,7 +251,11 @@ let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) =
 
 let arities_of_specif (kn,u) (mib,mip) =
   let specif = mip.mind_nf_lc in
-    Array.map (constructor_instantiate kn u mib) specif
+  let map (ctx, c) =
+    let cty = Term.it_mkProd_or_LetIn c ctx in
+    constructor_instantiate kn u mib cty
+  in
+  Array.map map specif
 
 let arities_of_constructors ind specif =
   arities_of_specif (fst (fst ind), snd ind) specif
@@ -342,7 +346,8 @@ let is_correct_arity env c pj ind specif params =
 (* [p] is the predicate, [i] is the constructor number (starting from 0),
    and [cty] is the type of the constructor (params not instantiated) *)
 let build_branches_type (ind,u) (_,mip as specif) params p =
-  let build_one_branch i cty =
+  let build_one_branch i (ctx, c) =
+    let cty = Term.it_mkProd_or_LetIn c ctx in
     let typi = full_constructor_instantiate (ind,u,specif,params) cty in
     let (cstrsign,ccl) = Term.decompose_prod_assum typi in
     let nargs = Context.Rel.length cstrsign in
@@ -597,6 +602,7 @@ let lambda_implicit_lift n a =
 (* This removes global parameters of the inductive types in lc (for
    nested inductive types only ) *)
 let abstract_mind_lc ntyps npars lc =
+  let lc = Array.map (fun (ctx, c) -> Term.it_mkProd_or_LetIn c ctx) lc in
   if Int.equal npars 0 then
     lc
   else
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 3c1464c6c9..ad35c16c22 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -139,4 +139,4 @@ val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
 
 val lambda_implicit_lift : int -> constr -> constr
 
-val abstract_mind_lc : int -> Int.t -> constr array -> constr array
+val abstract_mind_lc : int -> Int.t -> (rel_context * constr) array -> constr array
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 204f889f90..ef6c07bff2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1044,7 +1044,9 @@ let fake_match_projection env p =
   let indu = mkIndU (ind,u) in
   let ctx, paramslet =
     let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in
-    let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in
+    let (ctx, cty) = mip.mind_nf_lc.(0) in
+    let cty = Term.it_mkProd_or_LetIn cty ctx in
+    let rctx, _ = decompose_prod_assum (Vars.substl subst cty) in
     List.chop mip.mind_consnrealdecls.(0) rctx
   in
   let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index a60a966cec..56b3dc97cf 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -13,7 +13,6 @@ open Names
 open Constr
 open EConstr
 open Vars
-open Termops
 open Util
 open Declarations
 open Globnames
@@ -100,9 +99,8 @@ let kind_of_formula env sigma term =
 		      else
 			let has_realargs=(n>0) in
 			let is_trivial=
-			  let is_constant c =
-			    Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
-			    Array.exists is_constant mip.mind_nf_lc in
+                          let is_constant n = Int.equal n 0 in
+                            Array.exists is_constant mip.mind_consnrealargs in
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
 			  then
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index a0b1d784f1..7216849948 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -209,7 +209,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
           let mind,indb = Inductive.lookup_mind_specif env (kn,i) in
           let tys = indb.Declarations.mind_nf_lc in
           let renamed_tys =
-            Array.mapi (fun j t ->
+            Array.mapi (fun j (ctx, cty) ->
+              let t = Term.it_mkProd_or_LetIn cty ctx in
                     ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t));
               let t = Arguments_renaming.rename_type t
                 (GlobRef.ConstructRef((kn,i),j+1)) in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 68626597fc..affed5389f 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -514,12 +514,11 @@ let rec cases_pattern_of_glob_constr na c =
   ) c
 
 open Declarations
-open Term
 open Context
 
 (* Keep only patterns which are not bound to a local definitions *)
-let drop_local_defs typi args =
-    let (decls,_) = decompose_prod_assum typi in
+let drop_local_defs params decls args =
+    let decls = List.skipn (Rel.length params) (List.rev decls) in
     let rec aux decls args =
       match decls, args with
       | [], [] -> []
@@ -531,7 +530,7 @@ let drop_local_defs typi args =
          end
       | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
       | _ -> assert false in
-    aux (List.rev decls) args
+    aux decls args
 
 let add_patterns_for_params_remove_local_defs (ind,j) l =
   let (mib,mip) = Global.lookup_inductive ind in
@@ -540,9 +539,8 @@ let add_patterns_for_params_remove_local_defs (ind,j) l =
     if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
       (* Optimisation *) l
     else
-      let typi = mip.mind_nf_lc.(j-1) in
-      let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in
-      drop_local_defs typi l in
+      let (ctx, _) = mip.mind_nf_lc.(j - 1) in
+      drop_local_defs mib.mind_params_ctxt ctx l in
   Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l
 
 let add_alias ?loc na c =
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 4c02dc0f09..d937456bcb 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -101,7 +101,8 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
   and nconstr = Array.length mip.mind_consnames in
   let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in
   if j > nconstr then user_err Pp.(str "Not enough constructors in the type.");
-    substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1))
+  let (ctx, cty) = specif.(j - 1) in
+  substl (List.init ntypes make_Ik) (subst_instance_constr u (Term.it_mkProd_or_LetIn cty ctx))
 
 (* Number of constructors *)
 
@@ -280,8 +281,7 @@ let make_case_info env ind style =
   let ind_tags =
     Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
   let cstr_tags =
-    Array.map2 (fun c n ->
-      let d,_ = decompose_prod_assum c in
+    Array.map2 (fun (d, _) n ->
       Context.Rel.to_tags (List.firstn n d))
       mip.mind_nf_lc mip.mind_consnrealdecls in
   let print_info = { ind_tags; cstr_tags; style } in
@@ -462,7 +462,8 @@ let compute_projections env (kn, i as ind) =
   let pkt = mib.mind_packets.(i) in
   let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
   let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
-  let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
+  let ctx, cty = pkt.mind_nf_lc.(0) in
+  let rctx, _ = decompose_prod_assum (substl subst (Term.it_mkProd_or_LetIn cty ctx)) in
   let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
   (* We build a substitution smashing the lets in the record parameters so
      that typechecking projections requires just a substitution and not
@@ -622,9 +623,7 @@ let set_pattern_names env sigma ind brv =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let arities =
     Array.map
-      (fun c ->
-        Context.Rel.length ((prod_assum c)) -
-        mib.mind_nparams)
+      (fun (d, _) -> List.length d - mib.mind_nparams)
       mip.mind_nf_lc in
   Array.map2 (set_names env sigma) arities brv
 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index b7090e69da..77ae09ee6f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -107,7 +107,8 @@ let find_rectype_a env c =
 
 (* Instantiate inductives and parameters in constructor type *)
 
-let type_constructor mind mib u typ params =
+let type_constructor mind mib u (ctx, typ) params =
+  let typ = it_mkProd_or_LetIn typ ctx in
   let s = ind_subst mind mib u in
   let ctyp = substl s typ in
   let nparams = Array.length params in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 083661a64b..ff528bd2cf 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -61,7 +61,8 @@ let find_rectype_a env c =
 
 (* Instantiate inductives and parameters in constructor type *)
 
-let type_constructor mind mib u typ params =
+let type_constructor mind mib u (ctx, typ) params =
+  let typ = it_mkProd_or_LetIn typ ctx in
   let s = ind_subst mind mib u in
   let ctyp = substl s typ in
   let ctyp = subst_instance_constr u ctyp in
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index b12018cd66..3c1115d056 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -138,7 +138,7 @@ let get_sym_eq_data env (ind,u) =
   let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
   if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported.";
-  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let constrsign,ccl = mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments"; (* This can be relaxed... *)
@@ -173,7 +173,7 @@ let get_non_sym_eq_data env (ind,u) =
   let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
   if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported";
-  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let constrsign,ccl = mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
@@ -776,7 +776,7 @@ let build_congr env (eq,refl,ctx) ind =
     error "Inductive equalities with local definitions in arity not supported.";
   let env_with_arity = push_rel_context arityctxt env in
   let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
-  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let constrsign,ccl = mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 708412720a..395b4928ce 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -106,22 +106,24 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
         && (Int.equal mip.mind_nrealargs 0)
       then
 	if is_strict_conjunction style (* strict conjunction *) then
-	  let ctx =
-	    (prod_assum sigma (snd
-	      (decompose_prod_n_assum sigma mib.mind_nparams (EConstr.of_constr mip.mind_nf_lc.(0))))) in
+          let (ctx, _) = mip.mind_nf_lc.(0) in
+          let ctx = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in
 	  if
+            (* Constructor has a type of the form
+              c : forall (a_0 ... a_n : Type) (x_0 : A_0) ... (x_n : A_n). T **)
 	    List.for_all
 	      (fun decl -> let c = RelDecl.get_type decl in
 	                   is_local_assum decl &&
-			   isRel sigma c &&
-                           Int.equal (destRel sigma c) mib.mind_nparams) ctx
+                           Constr.isRel c &&
+                           Int.equal (Constr.destRel c) mib.mind_nparams) ctx
 	  then
 	    Some (hdapp,args)
 	  else None
 	else
+          let ctx, cty = mip.mind_nf_lc.(0) in
+          let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
           let ctyp = whd_beta_prod sigma
-            (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt)
-                       (EConstr.of_constr mip.mind_nf_lc.(0)) args) in
+            (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in
 	  let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
 	  if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then
 	    (* Record or non strict conjunction *)
@@ -165,12 +167,13 @@ let is_tuple sigma t =
    it is strict if it has the form
    "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
 
-let test_strict_disjunction n lc =
-  let open Term in
-  Array.for_all_i (fun i c ->
-    match (prod_assum (snd (decompose_prod_n_assum n c))) with
-    | [LocalAssum (_,c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i)
-    | _ -> false) 0 lc
+let test_strict_disjunction (mib, mip) =
+  let n = List.length mib.mind_params_ctxt in
+  let check i (ctx, _) = match List.skipn n (List.rev ctx) with
+  | [LocalAssum (_, c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i)
+  | _ -> false
+  in
+  Array.for_all_i check 0 mip.mind_nf_lc
 
 let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
   let (hdapp,args) = decompose_app sigma t in
@@ -183,14 +186,16 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
         && (Int.equal mip.mind_nrealargs 0)
       then
 	if strict then
-	  if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then
+          if test_strict_disjunction (mib, mip) then
 	    Some (hdapp,args)
 	  else
 	    None
 	else
-	  let cargs =
-	    Array.map (fun ar -> pi2 (destProd sigma (prod_applist sigma (EConstr.of_constr ar) args)))
-	      mip.mind_nf_lc in
+          let map (ctx, cty) =
+            let ar = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+            pi2 (destProd sigma (prod_applist sigma ar args))
+          in
+          let cargs = Array.map map mip.mind_nf_lc in
 	  Some (hdapp,Array.to_list cargs)
       else
 	None
@@ -225,10 +230,8 @@ let match_with_unit_or_eq_type sigma t =
   match EConstr.kind sigma hdapp with
     | Ind (ind , _) ->
         let (mib,mip) = Global.lookup_inductive ind in
-        let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
-        let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
-	if Int.equal nconstr 1 && zero_args constr_types.(0) then
+        if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then
 	  Some hdapp
 	else
 	  None
@@ -308,11 +311,13 @@ let match_with_equation env sigma t =
         let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
 	if Int.equal nconstr 1 then
-          if is_matching env sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then
+          let (ctx, cty) = constr_types.(0) in
+          let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+          if is_matching env sigma coq_refl_leibniz1_pattern cty then
 	    None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
-	  else if is_matching env sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then
+          else if is_matching env sigma coq_refl_leibniz2_pattern cty then
 	    None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-	  else if is_matching env sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then
+          else if is_matching env sigma coq_refl_jm_pattern cty then
 	    None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
 	  else raise NoEquationFound
         else raise NoEquationFound
@@ -378,8 +383,9 @@ let match_with_nodep_ind sigma t =
   | Ind (ind, _)  ->
      let (mib,mip) = Global.lookup_inductive ind in
      if Array.length (mib.mind_packets)>1 then None else
-       let nodep_constr c =
-         has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma (EConstr.of_constr c) in
+       let nodep_constr (ctx, cty) =
+        let c = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+         has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma c in
        if Array.for_all nodep_constr mip.mind_nf_lc then
          let params=
            if Int.equal mip.mind_nrealargs 0 then args else
@@ -400,7 +406,7 @@ let match_with_sigma_type sigma t =
         && (Int.equal mip.mind_nrealargs 0)
         && (Int.equal (Array.length mip.mind_consnames)1)
         && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma
-             (EConstr.of_constr mip.mind_nf_lc.(0))
+             (let (ctx, cty) = mip.mind_nf_lc.(0) in EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx))
      then
        (*allowing only 1 existential*)
        Some (hdapp,args)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bfbce8f6eb..ec8d4d0e14 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -20,6 +20,7 @@ open Tacmach
 open Clenv
 open Tactypes
 
+module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 (************************************************************************)
@@ -223,8 +224,8 @@ let compute_induction_names = compute_induction_names_gen true
 (* Compute the let-in signature of case analysis or standard induction scheme *)
 let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
   let rec analrec c recargs =
-    match Constr.kind c, recargs with
-    | Prod (_,_,c), recarg::rest ->
+    match c, recargs with
+    | RelDecl.LocalAssum _ :: c, recarg::rest ->
         let rest = analrec c rest in
         begin match Declareops.dest_recarg recarg with
         | Norec | Imbr _  -> true :: rest
@@ -232,14 +233,13 @@ let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
             if rec_flag && Int.equal j k then true :: true :: rest
             else true :: rest
         end
-    | LetIn (_,_,_,c), rest -> false :: analrec c rest
-    | _, [] -> []
+    | RelDecl.LocalDef _ :: c, rest -> false :: analrec c rest
+    | [], [] -> []
     | _ -> anomaly (Pp.str "compute_constructor_signatures.")
   in
   let (mib,mip) = Global.lookup_inductive ity in
-  let n = mib.mind_nparams in
-  let lc =
-    Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in
+  let map (ctx, _) = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in
+  let lc = Array.map map mip.mind_nf_lc in
   let lrecargs = Declareops.dest_subterms mip.mind_recargs in
   Array.map2 analrec lc lrecargs
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 11b64a5247..a173e5a125 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -16,7 +16,6 @@ open CAst
 open Util
 open Names
 open Nameops
-open Term
 open Tacmach
 open Constrintern
 open Prettyp
@@ -32,6 +31,7 @@ open Lemmas
 open Locality
 open Attributes
 
+module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 (** TODO: make this function independent of Ltac *)
@@ -133,22 +133,23 @@ let show_intro all =
 *)
     
 let make_cases_aux glob_ref =
+  let open Declarations in
   match glob_ref with
     | Globnames.IndRef ind ->
-	let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in
+      let mib, mip = Global.lookup_inductive ind in
 	Util.Array.fold_right_i
-	  (fun i typ l ->
-	     let al = List.rev (fst (decompose_prod typ)) in
-	     let al = Util.List.skipn np al in
+          (fun i (ctx, _) l ->
+             let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in
 	     let rec rename avoid = function
 	       | [] -> []
-	       | (n,_)::l ->
+               | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l
+               | RelDecl.LocalAssum (n, _)::l ->
 		   let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
 		   Id.to_string n' :: rename (Id.Set.add n' avoid) l in
 	     let al' = rename Id.Set.empty al in
 	     let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
 	     (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
-	  tarr []
+          mip.mind_nf_lc []
     | _ -> raise Not_found
 
 let make_cases s =