Merge PR #9476: Constructor type information uses the expanded form.

Reviewed-by: SkySkimmer
Reviewed-by: gares

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 d9d824ad98..0d31992e98 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 =