Change the representation of kernel case.

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.

72 files changed, 1210 insertions, 631 deletions

diff --git a/checker/values.ml b/checker/values.ml
index 4e99d087df..b94173429d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -147,7 +147,7 @@ let rec v_constr =
     [|v_puniverses v_cst|]; (* Const *)
     [|v_puniverses v_ind|]; (* Ind *)
     [|v_puniverses v_cons|]; (* Construct *)
-    [|v_caseinfo;v_constr;v_case_invert;v_constr;Array v_constr|]; (* Case *)
+    [|v_caseinfo;v_instance; Array v_constr; v_case_return; v_case_invert; v_constr; Array v_case_branch|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
     [|v_proj;v_constr|]; (* Proj *)
@@ -162,6 +162,10 @@ and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
 and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
 and v_case_invert = Sum ("case_inversion", 1, [|[|v_instance;Array v_constr|]|])
 
+and v_case_branch = Tuple ("case_branch", [|Array (v_binder_annot v_name); v_constr|])
+
+and v_case_return = Tuple ("case_return", [|Array (v_binder_annot v_name); v_constr|])
+
 let v_rdecl = v_sum "rel_declaration" 0
     [| [|v_binder_annot v_name; v_constr|];               (* LocalAssum *)
        [|v_binder_annot v_name; v_constr; v_constr|] |]   (* LocalDef *)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6ce347ad59..c4eed5756f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -307,9 +307,9 @@ let constr_display csr =
       "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^"),"
       ^","^(universes_display u)^(string_of_int j)^")"
   | Proj (p, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")"
-  | Case (ci,p,iv,c,bl) ->
+  | Case (ci,u,pms,(_,p),iv,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
-      ^(array_display bl)^")"
+      ^(array_display (Array.map snd bl))^")"
   | Fix ((t,i),(lna,tl,bl)) ->
       "Fix(([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="")
         then (";"^i) else "")) t "")^"|],"^(string_of_int i)^"),"
@@ -420,13 +420,25 @@ let print_pure_constr csr =
       print_int i; print_string ","; print_int j;
       print_string ","; universes_display u;
       print_string ")"
-  | Case (ci,p,iv,c,bl) ->
+  | Case (ci,u,pms,p,iv,c,bl) ->
+      let pr_ctx (nas, c) =
+        Array.iter (fun na -> print_cut (); name_display na) nas;
+        print_string " |- ";
+        box_display c
+      in
       open_vbox 0;
-      print_string "<"; box_display p; print_string ">";
       print_cut(); print_string "Case";
-      print_space(); box_display c; print_space (); print_string "of";
+      print_space(); box_display c; print_space ();
+      print_cut(); print_string "in";
+      print_cut(); print_string "Ind(";
+      sp_display (fst ci.ci_ind);
+      print_string ","; print_int (snd ci.ci_ind); print_string ")";
+      print_string "@{"; universes_display u; print_string "}";
+      Array.iter (fun x -> print_space (); box_display x) pms;
+      print_cut(); print_string "return <"; pr_ctx p; print_string ">";
+      print_cut(); print_string "with";
       open_vbox 0;
-      Array.iter (fun x ->  print_cut();  box_display x) bl;
+      Array.iter (fun x ->  print_cut();  pr_ctx x) bl;
       close_box();
       print_cut();
       print_string "end";
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c29de27efb..ec255aad03 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -35,6 +35,10 @@ include (Evd.MiniEConstr : module type of Evd.MiniEConstr
 type types = t
 type constr = t
 type existential = t pexistential
+type case_return = t pcase_return
+type case_branch = t pcase_branch
+type case_invert = (t, EInstance.t) pcase_invert
+type case = (t, t, EInstance.t) pcase
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
@@ -69,7 +73,7 @@ let mkInd i = of_kind (Ind (in_punivs i))
 let mkConstructU pc = of_kind (Construct pc)
 let mkConstruct c = of_kind (Construct (in_punivs c))
 let mkConstructUi ((ind,u),i) = of_kind (Construct ((ind,i),u))
-let mkCase (ci, c, iv, r, p) = of_kind (Case (ci, c, iv, r, p))
+let mkCase (ci, u, pms, c, iv, r, p) = of_kind (Case (ci, u, pms, c, iv, r, p))
 let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
@@ -195,7 +199,7 @@ let destCoFix sigma c = match kind sigma c with
 | _ -> raise DestKO
 
 let destCase sigma c = match kind sigma c with
-| Case (ci, t, iv, c, p) -> (ci, t, iv, c, p)
+| Case (ci, u, pms, t, iv, c, p) -> (ci, u, pms, t, iv, c, p)
 | _ -> raise DestKO
 
 let destProj sigma c = match kind sigma c with
@@ -320,19 +324,28 @@ let existential_type = Evd.existential_type
 
 let lift n c = of_constr (Vars.lift n (unsafe_to_constr c))
 
-let map_under_context f n c =
-  let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr (Constr.map_under_context f n (unsafe_to_constr c))
-let map_branches f ci br =
-  let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr_array (Constr.map_branches f ci (unsafe_to_constr_array br))
-let map_return_predicate f ci p =
-  let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p))
+let of_branches : Constr.case_branch array -> case_branch array =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
+
+let unsafe_to_branches : case_branch array -> Constr.case_branch array =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
+
+let of_return : Constr.case_return -> case_return =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
 
-let map_user_view sigma f c =
+let unsafe_to_return : case_return -> Constr.case_return =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
+
+let map_branches f br =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_branches (Constr.map_branches f (unsafe_to_branches br))
+let map_return_predicate f p =
   let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr (Constr.map_user_view f (unsafe_to_constr (whd_evar sigma c)))
+  of_return (Constr.map_return_predicate f (unsafe_to_return p))
 
 let map sigma f c =
   let f c = unsafe_to_constr (f (of_constr c)) in
@@ -346,7 +359,49 @@ let iter sigma f c =
   let f c = f (of_constr c) in
   Constr.iter f (unsafe_to_constr (whd_evar sigma c))
 
-let iter_with_full_binders sigma g f n c =
+let expand_case env _sigma (ci, u, pms, p, iv, c, bl) =
+  let u = EInstance.unsafe_to_instance u in
+  let pms = unsafe_to_constr_array pms in
+  let p = unsafe_to_return p in
+  let iv = unsafe_to_case_invert iv in
+  let c = unsafe_to_constr c in
+  let bl = unsafe_to_branches bl in
+  let (ci, p, iv, c, bl) = Inductive.expand_case env (ci, u, pms, p, iv, c, bl) in
+  let p = of_constr p in
+  let c = of_constr c in
+  let iv = of_case_invert iv in
+  let bl = of_constr_array bl in
+  (ci, p, iv, c, bl)
+
+let expand_branch env _sigma u pms (ind, i) (nas, _br) =
+  let open Declarations in
+  let u = EInstance.unsafe_to_instance u in
+  let pms = unsafe_to_constr_array pms in
+  let (mib, mip) = Inductive.lookup_mind_specif env ind in
+  let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list pms) in
+  let subst = paramsubst @ Inductive.ind_subst (fst ind) mib u in
+  let (ctx, _) = mip.mind_nf_lc.(i - 1) in
+  let (ctx, _) = List.chop mip.mind_consnrealdecls.(i - 1) ctx in
+  let ans = Inductive.instantiate_context u subst nas ctx in
+  let ans : rel_context = match Evd.MiniEConstr.unsafe_eq with Refl -> ans in
+  ans
+
+let contract_case env _sigma (ci, p, iv, c, bl) =
+  let p = unsafe_to_constr p in
+  let iv = unsafe_to_case_invert iv in
+  let c = unsafe_to_constr c in
+  let bl = unsafe_to_constr_array bl in
+  let (ci, u, pms, p, iv, c, bl) = Inductive.contract_case env (ci, p, iv, c, bl) in
+  let u = EInstance.make u in
+  let pms = of_constr_array pms in
+  let p = of_return p in
+  let iv = of_case_invert iv in
+  let c = of_constr c in
+  let bl = of_branches bl in
+  (ci, u, pms, p, iv, c, bl)
+
+let iter_with_full_binders env sigma g f n c =
   let open Context.Rel.Declaration in
   match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -357,7 +412,10 @@ let iter_with_full_binders sigma g f n c =
   | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
   | App (c,l) -> f n c; Array.Fun1.iter f n l
   | Evar (_,l) -> List.iter (fun c -> f n c) l
-  | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
+  | Case (ci,u,pms,p,iv,c,bl) ->
+    (* FIXME: skip the type annotations *)
+    let (ci, p, iv, c, bl) = expand_case env sigma (ci, u, pms, p, iv, c, bl) in
+    f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
@@ -566,9 +624,13 @@ let universes_of_constr sigma c =
     | Array (u,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
       fold sigma aux s c
-    | Case (_,_,CaseInvert {univs;args=_},_,_) ->
+    | Case (_,u,_,_,CaseInvert {univs;args=_},_,_) ->
+      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
       let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma univs)) s in
       fold sigma aux s c
+    | Case (_, u, _, _, NoInvert, _, _) ->
+      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
+      fold sigma aux s c
     | _ -> fold sigma aux s c
   in aux LSet.empty c
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 882dfe2848..2add7b0b5e 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -20,6 +20,8 @@ type t = Evd.econstr
 type types = t
 type constr = t
 type existential = t pexistential
+type case_return = t pcase_return
+type case_branch = t pcase_branch
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
@@ -58,6 +60,9 @@ sig
   val is_empty : t -> bool
 end
 
+type case_invert = (t, EInstance.t) pcase_invert
+type case = (t, t, EInstance.t) pcase
+
 type 'a puniverses = 'a * EInstance.t
 
 (** {5 Destructors} *)
@@ -128,7 +133,7 @@ val mkIndU : inductive * EInstance.t -> t
 val mkConstruct : constructor -> t
 val mkConstructU : constructor * EInstance.t -> t
 val mkConstructUi : (inductive * EInstance.t) * int -> t
-val mkCase : case_info * t * (t,EInstance.t) case_invert * t * t array -> t
+val mkCase : case -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> Sorts.relevance  -> t -> t
@@ -199,7 +204,7 @@ val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
 val destEvar : Evd.evar_map -> t -> t pexistential
 val destInd : Evd.evar_map -> t -> inductive * EInstance.t
 val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
-val destCase : Evd.evar_map -> t -> case_info * t * (t,EInstance.t) case_invert * t * t array
+val destCase : Evd.evar_map -> t -> case
 val destProj : Evd.evar_map -> t -> Projection.t * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
 val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
@@ -250,14 +255,12 @@ val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 (** {6 Iterators} *)
 
 val map : Evd.evar_map -> (t -> t) -> t -> t
-val map_user_view : Evd.evar_map -> (t -> t) -> t -> t
 val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
-val map_under_context : (t -> t) -> int -> t -> t
-val map_branches : (t -> t) -> case_info -> t array -> t array
-val map_return_predicate : (t -> t) -> case_info -> t -> t
+val map_branches : (t -> t) -> case_branch array -> case_branch array
+val map_return_predicate : (t -> t) -> case_return -> case_return
 val iter : Evd.evar_map -> (t -> unit) -> t -> unit
 val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
-val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
+val iter_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
 val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
 (** Gather the universes transitively used in the term, including in the
@@ -337,6 +340,17 @@ val fresh_global :
 val is_global : Evd.evar_map -> GlobRef.t -> t -> bool
 [@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
 
+val expand_case : Environ.env -> Evd.evar_map ->
+  case -> (case_info * t * case_invert * t * t array)
+
+val expand_branch : Environ.env -> Evd.evar_map ->
+  EInstance.t -> t array -> constructor -> case_branch -> rel_context
+(** Given a universe instance and parameters for the inductive type,
+    constructs the typed context in which the branch lives. *)
+
+val contract_case : Environ.env -> Evd.evar_map ->
+  (case_info * t * case_invert * t * t array) -> case
+
 (** {5 Extra} *)
 
 val of_existential : Constr.existential -> existential
@@ -345,7 +359,7 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, typ
 
 val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
 
-val of_case_invert : (Constr.t,Univ.Instance.t) case_invert -> (t,EInstance.t) case_invert
+val of_case_invert : Constr.case_invert -> case_invert
 
 (** {5 Unsafe operations} *)
 
@@ -371,7 +385,7 @@ sig
   val to_instance : EInstance.t -> Univ.Instance.t
   (** Physical identity. Does not care for normalization. *)
 
-  val to_case_invert : (t,EInstance.t) case_invert -> (Constr.t,Univ.Instance.t) case_invert
+  val to_case_invert : case_invert -> Constr.case_invert
 
   val eq : (t, Constr.t) eq
   (** Use for transparent cast between types. *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index ba6a9ea6d9..f9f8268507 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -144,7 +144,7 @@ let head_evar sigma c =
   let c = EConstr.Unsafe.to_constr c in
   let rec hrec c = match kind c with
     | Evar (evk,_)   -> evk
-    | Case (_,_,_,c,_) -> hrec c
+    | Case (_, _, _, _, _, c, _) -> hrec c
     | App (c,_)      -> hrec c
     | Cast (c,_,_)   -> hrec c
     | Proj (p, c)    -> hrec c
diff --git a/engine/evd.mli b/engine/evd.mli
index a6d55c2615..ec9ae6fca9 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -772,8 +772,8 @@ module MiniEConstr : sig
     (Constr.t, Constr.types) Context.Named.Declaration.pt
   val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt ->
     (Constr.t, Constr.types) Context.Rel.Declaration.pt
-  val of_case_invert : (constr,Univ.Instance.t) case_invert -> (econstr,EInstance.t) case_invert
-  val unsafe_to_case_invert : (econstr,EInstance.t) case_invert -> (constr,Univ.Instance.t) case_invert
+  val of_case_invert : (constr,Univ.Instance.t) pcase_invert -> (econstr,EInstance.t) pcase_invert
+  val unsafe_to_case_invert : (econstr,EInstance.t) pcase_invert -> (constr,Univ.Instance.t) pcase_invert
   val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt ->
     (t, t) Context.Rel.Declaration.pt
   val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt ->
diff --git a/engine/termops.ml b/engine/termops.ml
index 66131e1a8f..d331ecc458 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -606,7 +606,7 @@ let map_left2 f a g b =
     r, s
   end
 
-let map_constr_with_binders_left_to_right sigma g f l c =
+let map_constr_with_binders_left_to_right env sigma g f l c =
   let open RelDecl in
   let open EConstr in
   match EConstr.kind sigma c with
@@ -650,14 +650,16 @@ let map_constr_with_binders_left_to_right sigma g f l c =
     let al' = List.map_left (f l) al in
       if List.for_all2 (==) al' al then c
       else mkEvar (e, al')
-  | Case (ci,p,iv,b,bl) ->
+  | Case (ci,u,pms,p,iv,b,bl) ->
+      (* FIXME: skip annotations? *)
+      let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, b, bl) in
       (* In v8 concrete syntax, predicate is after the term to match! *)
       let b' = f l b in
       let iv' = map_invert (f l) iv in
       let p' = f l p in
       let bl' = Array.map_left (f l) bl in
       if b' == b && p' == p && iv' == iv && bl' == bl then c
-      else mkCase (ci, p', iv', b', bl')
+      else mkCase (EConstr.contract_case env sigma (ci, p', iv', b', bl'))
   | Fix (ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
       let (tl', bl') = map_left2 (f l) tl (f l') bl in
@@ -677,34 +679,8 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       if def' == def && t' == t && ty' == ty then c
       else mkArray(u,t',def',ty')
 
-let rec map_under_context_with_full_binders sigma g f l n d =
-  if n = 0 then f l d else
-    match EConstr.kind sigma d with
-    | LetIn (na,b,t,c) ->
-       let b' = f l b in
-       let t' = f l t in
-       let c' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in
-       if b' == b && t' == t && c' == c then d
-       else EConstr.mkLetIn (na,b',t',c')
-    | Lambda (na,t,b) ->
-       let t' = f l t in
-       let b' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in
-       if t' == t && b' == b then d
-       else EConstr.mkLambda (na,t',b')
-    | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
-
-let map_branches_with_full_binders sigma g f l ci bl =
-  let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
-  let bl' = Array.map2 (map_under_context_with_full_binders sigma g f l) tags bl in
-  if Array.for_all2 (==) bl' bl then bl else bl'
-
-let map_return_predicate_with_full_binders sigma g f l ci p =
-  let n = List.length ci.ci_pp_info.ind_tags in
-  let p' = map_under_context_with_full_binders sigma g f l n p in
-  if p' == p then p else p'
-
 (* strong *)
-let map_constr_with_full_binders_gen userview sigma g f l cstr =
+let map_constr_with_full_binders env sigma g f l cstr =
   let open EConstr in
   match EConstr.kind sigma cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -736,20 +712,14 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
   | Evar (e,al) ->
       let al' = List.map (f l) al in
       if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
-  | Case (ci,p,iv,c,bl) when userview ->
-      let p' = map_return_predicate_with_full_binders sigma g f l ci p in
-      let iv' = map_invert (f l) iv in
-      let c' = f l c in
-      let bl' = map_branches_with_full_binders sigma g f l ci bl in
-      if p==p' && iv'==iv && c==c' && bl'==bl then cstr else
-        mkCase (ci, p', iv', c', bl')
-  | Case (ci,p,iv,c,bl) ->
+  | Case (ci, u, pms, p, iv, c, bl) ->
+      let (ci, p, iv, c, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in
       let p' = f l p in
       let iv' = map_invert (f l) iv in
       let c' = f l c in
       let bl' = Array.map (f l) bl in
       if p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
-        mkCase (ci, p', iv', c', bl')
+        mkCase (EConstr.contract_case env sigma (ci, p', iv', c', bl'))
   | Fix (ln,(lna,tl,bl as fx)) ->
       let tl' = Array.map (f l) tl in
       let l' = fold_rec_types g fx l in
@@ -770,12 +740,6 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
       let ty' = f l ty in
       if def==def' && t == t' && ty==ty' then cstr else mkArray (u,t', def',ty')
 
-let map_constr_with_full_binders sigma g f =
-  map_constr_with_full_binders_gen false sigma g f
-
-let map_constr_with_full_binders_user_view sigma g f =
-  map_constr_with_full_binders_gen true sigma g f
-
 (* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
    subterms of [c] starting from [acc] and proceeding from left to
    right according to the usual representation of the constructions as
@@ -783,7 +747,7 @@ let map_constr_with_full_binders_user_view sigma g f =
    index) which is processed by [g] (which typically add 1 to [n]) at
    each binder traversal; it is not recursive *)
 
-let fold_constr_with_full_binders sigma g f n acc c =
+let fold_constr_with_full_binders env sigma g f n acc c =
   let open EConstr.Vars in
   let open Context.Rel.Declaration in
   match EConstr.kind sigma c with
@@ -795,7 +759,9 @@ let fold_constr_with_full_binders sigma g f n acc c =
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_,c) -> f n acc c
   | Evar (_,l) -> List.fold_left (f n) acc l
-  | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+  | Case (ci, u, pms, p, iv, c, bl) ->
+    let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in
+    Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
   | Fix (_,(lna,tl,bl)) ->
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
diff --git a/engine/termops.mli b/engine/termops.mli
index 709fa361a9..12df61e4c8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -50,16 +50,12 @@ val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context ->
 (** {6 Generic iterators on constr} *)
 
 val map_constr_with_binders_left_to_right :
-  Evd.evar_map ->
+  Environ.env -> Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> constr) ->
     'a -> constr -> constr
 val map_constr_with_full_binders :
-  Evd.evar_map ->
-  (rel_declaration -> 'a -> 'a) ->
-  ('a -> constr -> constr) -> 'a -> constr -> constr
-val map_constr_with_full_binders_user_view :
-  Evd.evar_map ->
+  Environ.env -> Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 
@@ -73,7 +69,7 @@ val map_constr_with_full_binders_user_view :
 val fold_constr_with_binders : Evd.evar_map ->
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
-val fold_constr_with_full_binders : Evd.evar_map ->
+val fold_constr_with_full_binders : Environ.env -> Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->
   ('a -> 'b -> constr -> 'b) ->
   'a -> 'b -> constr -> 'b
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 335c2e5e68..e2721b4822 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -68,6 +68,15 @@ let subst_univs_fn_constr f c =
       let u' = fi u in
         if u' == u then t
         else (changed := true; mkConstructU (c, u'))
+    | Case (ci, u, pms, p, NoInvert, c, br) ->
+      let u' = fi u in
+      if u' == u then map aux t
+      else (changed := true; map aux (mkCase (ci, u', pms, p, NoInvert, c, br)))
+    | Case (ci, u, pms, p, CaseInvert{univs;args}, c, br) ->
+      let u' = fi u in
+      let univs' = fi univs in
+      if u' == u && univs' == univs then map aux t
+      else (changed := true; map aux (mkCase (ci, u', pms, p, CaseInvert {univs = univs'; args}, c, br)))
     | _ -> map aux t
   in
   let c' = aux c in
@@ -147,10 +156,15 @@ let nf_evars_and_universes_opt_subst f subst =
     | Sort (Type u) ->
       let u' = Univ.subst_univs_universe subst u in
       if u' == u then c else mkSort (sort_of_univ u')
-    | Case (ci,p,CaseInvert {univs;args},t,br) ->
+    | Case (ci, u, pms, p, NoInvert, t, br) ->
+      let u' = Instance.subst_fn lsubst u in
+      if u' == u then map aux c
+      else Constr.map aux (mkCase (ci, u', pms, p, NoInvert, t, br))
+    | Case (ci,u,pms,p,CaseInvert {univs;args},t,br) ->
+      let u' = Instance.subst_fn lsubst u in
       let univs' = Instance.subst_fn lsubst univs in
-      if univs' == univs then Constr.map aux c
-      else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br))
+      if u' == u && univs' == univs then Constr.map aux c
+      else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},t,br))
     | Array (u,elems,def,ty) ->
       let u' = Univ.Instance.subst_fn lsubst u in
       let elems' = CArray.Smart.map aux elems in
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 7742f985de..1e85fadce5 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -209,16 +209,16 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
         acc.(i) <- update pos rig acc.(i)
     | App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
         if strict then () else
-          iter_with_full_binders sigma push_lift (frec false) ed c
+          iter_with_full_binders env sigma push_lift (frec false) ed c
     | Proj (p, _) when rig ->
       if strict then () else
-        iter_with_full_binders sigma push_lift (frec false) ed c
+        iter_with_full_binders env sigma push_lift (frec false) ed c
     | Case _ when rig ->
         if strict then () else
-          iter_with_full_binders sigma push_lift (frec false) ed c
+          iter_with_full_binders env sigma push_lift (frec false) ed c
     | Evar _ -> ()
     | _ ->
-        iter_with_full_binders sigma push_lift (frec rig) ed c
+        iter_with_full_binders env sigma push_lift (frec rig) ed c
   in
   let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in
   acc
@@ -228,7 +228,7 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
 let rec is_rigid_head sigma t = match kind sigma t with
   | Rel _ | Evar _ -> false
   | Ind _ | Const _ | Var _ | Sort _ -> true
-  | Case (_,_,_,f,_) -> is_rigid_head sigma f
+  | Case (_,_,_,_,_,f,_) -> is_rigid_head sigma f
   | Proj (p,c) -> true
   | App (f,args) ->
       (match kind sigma f with
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index d2256720c4..5613bf645e 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -34,6 +34,8 @@ open Environ
 open Vars
 open Esubst
 
+module RelDecl = Context.Rel.Declaration
+
 let stats = ref false
 
 (* Profiling *)
@@ -342,8 +344,8 @@ and fterm =
   | FProj of Projection.t * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
-  | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs
+  | FCaseT of case_info * Univ.Instance.t * constr array * case_return * fconstr * case_branch array * fconstr subs (* predicate and branches are closures *)
+  | FCaseInvert of case_info * Univ.Instance.t * constr array * case_return * finvert * fconstr * case_branch array * fconstr subs
   | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs
   | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs
   | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
@@ -410,7 +412,7 @@ type 'a next_native_args = (CPrimitives.arg_kind * 'a) list
 
 type stack_member =
   | Zapp of fconstr array
-  | ZcaseT of case_info * constr * constr array * fconstr subs
+  | ZcaseT of case_info * Univ.Instance.t * constr array * case_return * case_branch array * fconstr subs
   | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zprimitive of CPrimitives.t * pconstant * fconstr list * fconstr next_native_args
@@ -578,10 +580,11 @@ let rec to_constr lfts v =
     | FFlex (ConstKey op) -> mkConstU op
     | FInd op -> mkIndU op
     | FConstruct op -> mkConstructU op
-    | FCaseT (ci,p,c,ve,env) -> to_constr_case lfts ci p NoInvert c ve env
-    | FCaseInvert (ci,p,(univs,args),c,ve,env) ->
+    | FCaseT (ci, u, pms, p, c, ve, env) ->
+      to_constr_case lfts ci u pms p NoInvert c ve env
+    | FCaseInvert (ci, u, pms, p, (univs, args), c, ve, env) ->
       let iv = CaseInvert {univs;args=Array.map (to_constr lfts) args} in
-       to_constr_case lfts ci p iv c ve env
+      to_constr_case lfts ci u pms p iv c ve env
     | FFix ((op,(lna,tys,bds)) as fx, e) ->
       if is_subs_id e && is_lift_id lfts then
         mkFix fx
@@ -649,14 +652,20 @@ let rec to_constr lfts v =
         subst_constr subs t
     | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*)
 
-and to_constr_case lfts ci p iv c ve env =
+and to_constr_case lfts ci u pms p iv c ve env =
   if is_subs_id env && is_lift_id lfts then
-    mkCase (ci, p, iv, to_constr lfts c, ve)
+    mkCase (ci, u, pms, p, iv, to_constr lfts c, ve)
   else
     let subs = comp_subs lfts env in
-    mkCase (ci, subst_constr subs p, iv,
-            to_constr lfts c,
-            Array.map (fun b -> subst_constr subs b) ve)
+    let f_ctx (nas, c) =
+      let c = subst_constr (Esubst.subs_liftn (Array.length nas) subs) c in
+      (nas, c)
+    in
+    mkCase (ci, u, Array.map (fun c -> subst_constr subs c) pms,
+        f_ctx p,
+        iv,
+        to_constr lfts c,
+        Array.map f_ctx ve)
 
 and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with
 | Rel i ->
@@ -687,8 +696,8 @@ let rec zip m stk =
   match stk with
     | [] -> m
     | Zapp args :: s -> zip {mark=Mark.neutr m.mark; term=FApp(m, args)} s
-    | ZcaseT(ci,p,br,e)::s ->
-        let t = FCaseT(ci, p, m, br, e) in
+    | ZcaseT(ci, u, pms, p, br, e)::s ->
+        let t = FCaseT(ci, u, pms, p, m, br, e) in
         let mark = mark (neutr (Mark.red_state m.mark)) Unknown  in
         zip {mark; term=t} s
     | Zproj p :: s ->
@@ -763,6 +772,9 @@ let rec subs_consn v i n s =
   if Int.equal i n then s
   else subs_consn v (i + 1) n (subs_cons v.(i) s)
 
+let subs_consv v s =
+  subs_consn v 0 (Array.length v) s
+
 (* Beta reduction: look for an applied argument in the stack.
    Since the encountered update marks are removed, h must be a whnf *)
 let rec get_args n tys f e = function
@@ -870,6 +882,74 @@ let drop_parameters depth n argstk =
   (* we know that n < stack_args_size(argstk) (if well-typed term) *)
   anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor.")
 
+let inductive_subst (ind, _) mib u pms e =
+  let rec self i accu =
+    if Int.equal i mib.mind_ntypes then accu
+    else
+      let c = inject (mkIndU ((ind, i), u)) in
+      self (i + 1) (subs_cons c accu)
+  in
+  let self = self 0 (subs_id 0) in
+  let rec mk_pms i ctx = match ctx with
+  | [] -> self
+  | RelDecl.LocalAssum _ :: ctx ->
+    let c = mk_clos e pms.(i) in
+    let subs = mk_pms (i - 1) ctx in
+    subs_cons c subs
+  | RelDecl.LocalDef (_, c, _) :: ctx ->
+    let c = Vars.subst_instance_constr u c in
+    let subs = mk_pms i ctx in
+    subs_cons (mk_clos subs c) subs
+  in
+  mk_pms (Array.length pms - 1) mib.mind_params_ctxt
+
+(* Iota-reduction: feed the arguments of the constructor to the branch *)
+let get_branch infos depth ci u pms (ind, c) br e args =
+  let i = c - 1 in
+  let args = drop_parameters depth ci.ci_npar args in
+  let (_nas, br) = br.(i) in
+  if Int.equal ci.ci_cstr_ndecls.(i) ci.ci_cstr_nargs.(i) then
+    (* No let-bindings in the constructor, we don't have to fetch the
+      environment to know the value of the branch. *)
+    let rec push e stk = match stk with
+    | [] -> e
+    | Zapp v :: stk -> push (subs_consv v e) stk
+    | (Zshift _ | ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _) :: _ ->
+      assert false
+    in
+    let e = push e args in
+    (br, e)
+  else
+    (* The constructor contains let-bindings, but they are not physically
+        present in the match, so we fetch them in the environment. *)
+    let env = info_env infos in
+    let mib = Environ.lookup_mind (fst ind) env in
+    let mip = mib.mind_packets.(snd ind) in
+    let (ctx, _) = mip.mind_nf_lc.(i) in
+    let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in
+    let map = function
+    | Zapp args -> args
+    | Zshift _ | ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _ ->
+      assert false
+    in
+    let ind_subst = inductive_subst ind mib u pms e in
+    let args = Array.concat (List.map map args) in
+    let rec push i e = function
+    | [] -> []
+    | RelDecl.LocalAssum _ :: ctx ->
+      let ans = push (pred i) e ctx in
+      args.(i) :: ans
+    | RelDecl.LocalDef (_, b, _) :: ctx ->
+      let ans = push i e ctx in
+      let b = subst_instance_constr u b in
+      let s = Array.rev_of_list ans in
+      let e = subs_consv s ind_subst in
+      let v = mk_clos e b in
+      v :: ans
+    in
+    let ext = push (Array.length args - 1) [] ctx in
+    (br, subs_consv (Array.rev_of_list ext) e)
+
 (** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
     to the conversion of the eta expansion of t, considered as an inhabitant
     of ind, and the Constructor c of this inductive type applied to arguments
@@ -909,7 +989,6 @@ let rec project_nth_arg n = function
   | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _ | Zprimitive _) :: _ | [] -> assert false
       (* After drop_parameters we have a purely applicative stack *)
 
-
 (* Iota reduction: expansion of a fixpoint.
  * Given a fixpoint and a substitution, returns the corresponding
  * fixpoint body, and the substitution in which it should be
@@ -1269,7 +1348,7 @@ let rec knh info m stk =
     | FCLOS(t,e) -> knht info e t (zupdate info m stk)
     | FLOCKED -> assert false
     | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk))
-    | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk)
+    | FCaseT(ci,u,pms,p,t,br,e) -> knh info t (ZcaseT(ci,u,pms,p,br,e)::zupdate info m stk)
     | FFix(((ri,n),_),_) ->
         (match get_nth_arg m ri.(n) stk with
              (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
@@ -1289,10 +1368,10 @@ and knht info e t stk =
   match kind t with
     | App(a,b) ->
         knht info e a (append_stack (mk_clos_vect e b) stk)
-    | Case(ci,p,NoInvert,t,br) ->
-        knht info e t (ZcaseT(ci, p, br, e)::stk)
-    | Case(ci,p,CaseInvert{univs;args},t,br) ->
-      let term = FCaseInvert (ci, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in
+    | Case(ci,u,pms,p,NoInvert,t,br) ->
+        knht info e t (ZcaseT(ci, u, pms, p, br, e)::stk)
+    | Case(ci,u,pms,p,CaseInvert{univs;args},t,br) ->
+      let term = FCaseInvert (ci, u, pms, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in
       { mark = mark Red Unknown; term }, stk
     | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk
     | Cast(a,_,_) -> knht info e a stk
@@ -1347,15 +1426,15 @@ let rec knr info tab m stk =
         | Def v -> kni info tab v stk
         | Primitive _ -> assert false
         | OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk)))
-  | FConstruct((_ind,c),_u) ->
+  | FConstruct(c,_u) ->
      let use_match = red_set info.i_flags fMATCH in
      let use_fix = red_set info.i_flags fFIX in
      if use_match || use_fix then
       (match [@ocaml.warning "-4"] strip_update_shift_app m stk with
-        | (depth, args, ZcaseT(ci,_,br,e)::s) when use_match ->
+        | (depth, args, ZcaseT(ci,u,pms,_,br,e)::s) when use_match ->
             assert (ci.ci_npar>=0);
-            let rargs = drop_parameters depth ci.ci_npar args in
-            knit info tab e br.(c-1) (rargs@s)
+            let (br, e) = get_branch info depth ci u pms c br e args in
+            knit info tab e br s
         | (_, cargs, Zfix(fx,par)::s) when use_fix ->
             let rarg = fapp_stack(m,cargs) in
             let stk' = par @ append_stack [|rarg|] s in
@@ -1399,7 +1478,7 @@ let rec knr info tab m stk =
            kni info tab a (Zprimitive(op,c,rargs,nargs)::s)
              end
      | (_, _, s) -> (m, s))
-  | FCaseInvert (ci,_p,iv,_c,v,env) when red_set info.i_flags fMATCH ->
+  | FCaseInvert (ci, _u, _pms, _p,iv,_c,v,env) when red_set info.i_flags fMATCH ->
     begin match case_inversion info tab ci iv v with
       | Some c -> knit info tab env c stk
       | None -> (m, stk)
@@ -1419,7 +1498,12 @@ and knit info tab e t stk =
 
 and case_inversion info tab ci (univs,args) v =
   let open Declarations in
-  if Array.is_empty args then Some v.(0)
+  (* No binders / lets at all in the unique branch *)
+  let v = match v with
+  | [| [||], v |] -> v
+  | _ -> assert false
+  in
+  if Array.is_empty args then Some v
   else
     let env = info_env info in
     let ind = ci.ci_ind in
@@ -1437,7 +1521,7 @@ and case_inversion info tab ci (univs,args) v =
       !conv {info with i_flags=all} tab expected index
     in
     if Array.for_all_i check_index 0 indices
-    then Some v.(0) else None
+    then Some v else None
 
 let kh info tab v stk = fapp_stack(kni info tab v stk)
 
@@ -1448,9 +1532,13 @@ let rec zip_term zfun m stk =
     | [] -> m
     | Zapp args :: s ->
         zip_term zfun (mkApp(m, Array.map zfun args)) s
-    | ZcaseT(ci,p,br,e)::s ->
-        let t = mkCase(ci, zfun (mk_clos e p), NoInvert, m,
-                       Array.map (fun b -> zfun (mk_clos e b)) br) in
+    | ZcaseT(ci, u, pms, p, br, e) :: s ->
+        let zip_ctx (nas, c) =
+          let e = Esubst.subs_liftn (Array.length nas) e in
+          (nas, zfun (mk_clos e c))
+        in
+        let t = mkCase(ci, u, Array.map (fun c -> zfun (mk_clos e c)) pms, zip_ctx p,
+          NoInvert, m, Array.map zip_ctx br) in
         zip_term zfun t s
     | Zproj p::s ->
         let t = mkProj (Projection.make p true, m) in
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 3e8916673d..bccbddb0fc 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -110,8 +110,8 @@ type fterm =
   | FProj of Projection.t * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
-  | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs
+  | FCaseT of case_info * Univ.Instance.t * constr array * case_return * fconstr * case_branch array * fconstr subs (* predicate and branches are closures *)
+  | FCaseInvert of case_info * Univ.Instance.t * constr array * case_return * finvert * fconstr * case_branch array * fconstr subs
   | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs
   | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs
   | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
@@ -130,7 +130,7 @@ type 'a next_native_args = (CPrimitives.arg_kind * 'a) list
 
 type stack_member =
   | Zapp of fconstr array
-  | ZcaseT of case_info * constr * constr array * fconstr subs
+  | ZcaseT of case_info * Univ.Instance.t * constr array * case_return * case_branch array * fconstr subs
   | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zprimitive of CPrimitives.t * pconstant * fconstr list * fconstr next_native_args
diff --git a/kernel/constr.ml b/kernel/constr.ml
index bbaf95c9df..0dc72025af 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -83,10 +83,16 @@ type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
-type ('constr, 'univs) case_invert =
+type ('constr, 'univs) pcase_invert =
   | NoInvert
   | CaseInvert of { univs : 'univs; args : 'constr array }
 
+type 'constr pcase_branch = Name.t Context.binder_annot array * 'constr
+type 'types pcase_return = Name.t Context.binder_annot array * 'types
+
+type ('constr, 'types, 'univs) pcase =
+  case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
+
 (* [Var] is used for named variables and [Rel] for variables as
    de Bruijn indices. *)
 type ('constr, 'types, 'sort, 'univs) kind_of_term =
@@ -103,7 +109,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Const     of (Constant.t * 'univs)
   | Ind       of (inductive * 'univs)
   | Construct of (constructor * 'univs)
-  | Case      of case_info * 'constr * ('constr, 'univs) case_invert * 'constr * 'constr array
+  | Case      of case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
@@ -119,6 +125,10 @@ type existential = existential_key * constr list
 
 type types = constr
 
+type case_invert = (constr, Instance.t) pcase_invert
+type case_return = types pcase_return
+type case_branch = constr pcase_branch
+type case = (constr, types, Instance.t) pcase
 type rec_declaration = (constr, types) prec_declaration
 type fixpoint = (constr, types) pfixpoint
 type cofixpoint = (constr, types) pcofixpoint
@@ -194,7 +204,7 @@ let mkConstructU c = Construct c
 let mkConstructUi ((ind,u),i) = Construct ((ind,i),u)
 
 (* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
-let mkCase (ci, p, iv, c, ac) = Case (ci, p, iv, c, ac)
+let mkCase (ci, u, params, p, iv, c, ac) = Case (ci, u, params, p, iv, c, ac)
 
 (* If recindxs = [|i1,...in|]
       funnames = [|f1,...fn|]
@@ -425,7 +435,7 @@ let destConstruct c = match kind c with
 
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
 let destCase c = match kind c with
-  | Case (ci,p,iv,c,v) -> (ci,p,iv,c,v)
+  | Case (ci,u,params,p,iv,c,v) -> (ci,u,params,p,iv,c,v)
   | _ -> raise DestKO
 
 let destProj c = match kind c with
@@ -484,7 +494,8 @@ let fold f acc c = match kind c with
   | App (c,l) -> Array.fold_left f (f acc c) l
   | Proj (_p,c) -> f acc c
   | Evar (_,l) -> List.fold_left f acc l
-  | Case (_,p,iv,c,bl) -> Array.fold_left f (f (fold_invert f (f acc p) iv) c) bl
+  | Case (_,_,pms,(_,p),iv,c,bl) ->
+    Array.fold_left (fun acc (_, b) -> f acc b) (f (fold_invert f (f (Array.fold_left f acc pms) p) iv) c) bl
   | Fix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
   | CoFix (_,(_lna,tl,bl)) ->
@@ -511,7 +522,8 @@ let iter f c = match kind c with
   | App (c,l) -> f c; Array.iter f l
   | Proj (_p,c) -> f c
   | Evar (_,l) -> List.iter f l
-  | Case (_,p,iv,c,bl) -> f p; iter_invert f iv; f c; Array.iter f bl
+  | Case (_,_,pms,p,iv,c,bl) ->
+    Array.iter f pms; f (snd p); iter_invert f iv; f c; Array.iter (fun (_, b) -> f b) bl
   | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty
@@ -531,7 +543,12 @@ let iter_with_binders g f n c = match kind c with
   | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
   | App (c,l) -> f n c; Array.Fun1.iter f n l
   | Evar (_,l) -> List.iter (fun c -> f n c) l
-  | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
+  | Case (_,_,pms,p,iv,c,bl) ->
+    Array.Fun1.iter f n pms;
+    f (iterate g (Array.length (fst p)) n) (snd p);
+    iter_invert (f n) iv;
+    f n c;
+    Array.Fun1.iter (fun n (ctx, b) -> f (iterate g (Array.length ctx) n) b) n bl
   | Proj (_p,c) -> f n c
   | Fix (_,(_,tl,bl)) ->
       Array.Fun1.iter f n tl;
@@ -560,7 +577,11 @@ let fold_constr_with_binders g f n acc c =
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_p,c) -> f n acc c
   | Evar (_,l) -> List.fold_left (f n) acc l
-  | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+  | Case (_,_,pms,p,iv,c,bl) ->
+    let fold_ctx n accu (nas, c) =
+      f (iterate g (Array.length nas) n) accu c
+    in
+    Array.fold_left (fold_ctx n) (f n (fold_invert (f n) (fold_ctx n (Array.fold_left (f n) acc pms) p) iv) c) bl
   | Fix (_,(_,tl,bl)) ->
       let n' = iterate g (Array.length tl) n in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
@@ -576,53 +597,30 @@ let fold_constr_with_binders g f n acc c =
    not recursive and the order with which subterms are processed is
    not specified *)
 
-let rec map_under_context f n d =
-  if n = 0 then f d else
-  match kind d with
-  | LetIn (na,b,t,c) ->
-    let b' = f b in
-    let t' = f t in
-    let c' = map_under_context f (n-1) c in
-    if b' == b && t' == t && c' == c then d
-    else mkLetIn (na,b',t',c')
-  | Lambda (na,t,b) ->
-    let t' = f t in
-    let b' = map_under_context f (n-1) b in
-    if t' == t && b' == b then d
-    else mkLambda (na,t',b')
-  | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
-
-let map_branches f ci bl =
-  let nl = Array.map List.length ci.ci_pp_info.cstr_tags in
-  let bl' = Array.map2 (map_under_context f) nl bl in
+let map_under_context f d =
+  let (nas, p) = d in
+  let p' = f p in
+  if p' == p then d else (nas, p')
+
+let map_branches f bl =
+  let bl' = Array.map (map_under_context f) bl in
   if Array.for_all2 (==) bl' bl then bl else bl'
 
-let map_return_predicate f ci p =
-  map_under_context f (List.length ci.ci_pp_info.ind_tags) p
-
-let rec map_under_context_with_binders g f l n d =
-  if n = 0 then f l d else
-  match kind d with
-  | LetIn (na,b,t,c) ->
-      let b' = f l b in
-      let t' = f l t in
-      let c' = map_under_context_with_binders g f (g l) (n-1) c in
-      if b' == b && t' == t && c' == c then d
-      else mkLetIn (na,b',t',c')
-  | Lambda (na,t,b) ->
-      let t' = f l t in
-      let b' = map_under_context_with_binders g f (g l) (n-1) b in
-      if t' == t && b' == b then d
-      else mkLambda (na,t',b')
-  | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
-
-let map_branches_with_binders g f l ci bl =
-  let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
-  let bl' = Array.map2 (map_under_context_with_binders g f l) tags bl in
+let map_return_predicate f p =
+  map_under_context f p
+
+let map_under_context_with_binders g f l d =
+  let (nas, p) = d in
+  let l = iterate g (Array.length nas) l in
+  let p' = f l p in
+  if p' == p then d else (nas, p')
+
+let map_branches_with_binders g f l bl =
+  let bl' = Array.map (map_under_context_with_binders g f l) bl in
   if Array.for_all2 (==) bl' bl then bl else bl'
 
-let map_return_predicate_with_binders g f l ci p =
-  map_under_context_with_binders g f l (List.length ci.ci_pp_info.ind_tags) p
+let map_return_predicate_with_binders g f l p =
+  map_under_context_with_binders g f l p
 
 let map_invert f = function
   | NoInvert -> NoInvert
@@ -631,7 +629,7 @@ let map_invert f = function
     if args == args' then orig
     else CaseInvert {univs;args=args';}
 
-let map_gen userview f c = match kind c with
+let map f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _ | Int _ | Float _) -> c
   | Cast (b,k,t) ->
@@ -668,20 +666,14 @@ let map_gen userview f c = match kind c with
       let l' = List.Smart.map f l in
       if l'==l then c
       else mkEvar (e, l')
-  | Case (ci,p,iv,b,bl) when userview ->
-      let b' = f b in
-      let iv' = map_invert f iv in
-      let p' = map_return_predicate f ci p in
-      let bl' = map_branches f ci bl in
-      if b'==b && iv'==iv && p'==p && bl'==bl then c
-      else mkCase (ci, p', iv', b', bl')
-  | Case (ci,p,iv,b,bl) ->
+  | Case (ci,u,pms,p,iv,b,bl) ->
+      let pms' = Array.Smart.map f pms in
       let b' = f b in
       let iv' = map_invert f iv in
-      let p' = f p in
-      let bl' = Array.Smart.map f bl in
-      if b'==b && iv'==iv && p'==p && bl'==bl then c
-      else mkCase (ci, p', iv', b', bl')
+      let p' = map_return_predicate f p in
+      let bl' = map_branches f bl in
+      if b'==b && iv'==iv && p'==p && bl'==bl && pms'==pms then c
+      else mkCase (ci, u, pms', p', iv', b', bl')
   | Fix (ln,(lna,tl,bl)) ->
       let tl' = Array.Smart.map f tl in
       let bl' = Array.Smart.map f bl in
@@ -699,9 +691,6 @@ let map_gen userview f c = match kind c with
     if def'==def && t==t' && ty==ty' then c
     else mkArray(u,t',def',ty')
 
-let map_user_view = map_gen true
-let map = map_gen false
-
 (* Like {!map} but with an accumulator. *)
 
 let fold_map_invert f acc = function
@@ -711,6 +700,18 @@ let fold_map_invert f acc = function
     if args==args' then acc, orig
     else acc, CaseInvert {univs;args=args';}
 
+let fold_map_under_context f accu d =
+  let (nas, p) = d in
+  let accu, p' = f accu p in
+  if p' == p then accu, d else accu, (nas, p')
+
+let fold_map_branches f accu bl =
+  let accu, bl' = Array.Smart.fold_left_map (fold_map_under_context f) accu bl in
+  if Array.for_all2 (==) bl' bl then accu, bl else accu, bl'
+
+let fold_map_return_predicate f accu p =
+  fold_map_under_context f accu p
+
 let fold_map f accu c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _ | Int _ | Float _) -> accu, c
@@ -749,13 +750,14 @@ let fold_map f accu c = match kind c with
       let accu, l' = List.fold_left_map f accu l in
       if l'==l then accu, c
       else accu, mkEvar (e, l')
-  | Case (ci,p,iv,b,bl) ->
-      let accu, b' = f accu b in
+  | Case (ci,u,pms,p,iv,b,bl) ->
+      let accu, pms' = Array.Smart.fold_left_map f accu pms in
+      let accu, p' = fold_map_return_predicate f accu p in
       let accu, iv' = fold_map_invert f accu iv in
-      let accu, p' = f accu p in
-      let accu, bl' = Array.Smart.fold_left_map f accu bl in
-      if b'==b && iv'==iv && p'==p && bl'==bl then accu, c
-      else accu, mkCase (ci, p', iv', b', bl')
+      let accu, b' = f accu b in
+      let accu, bl' = fold_map_branches f accu bl in
+      if pms'==pms && p'==p && iv'==iv && b'==b && bl'==bl then accu, c
+      else accu, mkCase (ci, u, pms', p', iv', b', bl')
   | Fix (ln,(lna,tl,bl)) ->
       let accu, tl' = Array.Smart.fold_left_map f accu tl in
       let accu, bl' = Array.Smart.fold_left_map f accu bl in
@@ -816,13 +818,14 @@ let map_with_binders g f l c0 = match kind c0 with
     let al' = List.Smart.map (fun c -> f l c) al in
     if al' == al then c0
     else mkEvar (e, al')
-  | Case (ci, p, iv, c, bl) ->
-    let p' = f l p in
+  | Case (ci, u, pms, p, iv, c, bl) ->
+    let pms' = Array.Fun1.Smart.map f l pms in
+    let p' = map_return_predicate_with_binders g f l p in
     let iv' = map_invert (f l) iv in
     let c' = f l c in
-    let bl' = Array.Fun1.Smart.map f l bl in
-    if p' == p && iv' == iv && c' == c && bl' == bl then c0
-    else mkCase (ci, p', iv', c', bl')
+    let bl' = map_branches_with_binders g f l bl in
+    if pms' == pms && p' == p && iv' == iv && c' == c && bl' == bl then c0
+    else mkCase (ci, u, pms', p', iv', c', bl')
   | Fix (ln, (lna, tl, bl)) ->
     let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
@@ -886,6 +889,9 @@ let eq_invert eq leq_universes iv1 iv2 =
     leq_universes univs iv2.univs
     && Array.equal eq args iv2.args
 
+let eq_under_context eq (_nas1, p1) (_nas2, p2) =
+  eq p1 p2
+
 let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 =
   match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with
   | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *)
@@ -911,8 +917,12 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
   | Ind (c1,u1), Ind (c2,u2) -> Ind.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2
   | Construct (c1,u1), Construct (c2,u2) ->
     Construct.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2
-  | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) ->
-    eq 0 p1 p2 && eq_invert (eq 0) (leq_universes None) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2
+  | Case (ci1,u1,pms1,p1,iv1,c1,bl1), Case (ci2,u2,pms2,p2,iv2,c2,bl2) ->
+    (** FIXME: what are we doing with u1 = u2 ? *)
+    Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind && leq_universes (Some (GlobRef.IndRef ci1.ci_ind, 0)) u1 u2 &&
+    Array.equal (eq 0) pms1 pms2 && eq_under_context (eq 0) p1 p2 &&
+    eq_invert (eq 0) (leq_universes None) iv1 iv2 &&
+    eq 0 c1 c2 && Array.equal (eq_under_context (eq 0)) bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
     Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
     && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
@@ -1063,6 +1073,9 @@ let constr_ord_int f t1 t2 =
   let fix_cmp (a1, i1) (a2, i2) =
     ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2
   in
+  let ctx_cmp f (_n1, p1) (_n2, p2) =
+    f p1 p2
+  in
   match kind t1, kind t2 with
     | Cast (c1,_,_), _ -> f c1 t2
     | _, Cast (c2,_,_) -> f t1 c2
@@ -1096,12 +1109,13 @@ let constr_ord_int f t1 t2 =
     | Ind _, _ -> -1 | _, Ind _ -> 1
     | Construct (ct1,_u1), Construct (ct2,_u2) -> Construct.CanOrd.compare ct1 ct2
     | Construct _, _ -> -1 | _, Construct _ -> 1
-    | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) ->
-      let c = f p1 p2 in
+    | Case (_,_u1,pms1,p1,iv1,c1,bl1), Case (_,_u2,pms2,p2,iv2,c2,bl2) ->
+      let c = Array.compare f pms1 pms2 in
+      if Int.equal c 0 then let c = ctx_cmp f p1 p2 in
       if Int.equal c 0 then let c = compare_invert f iv1 iv2 in
       if Int.equal c 0 then let c = f c1 c2 in
-      if Int.equal c 0 then Array.compare f bl1 bl2
-      else c else c else c
+      if Int.equal c 0 then Array.compare (ctx_cmp f) bl1 bl2
+      else c else c else c else c
     | Case _, _ -> -1 | _, Case _ -> 1
     | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
         ((fix_cmp =? (Array.compare f)) ==? (Array.compare f))
@@ -1180,6 +1194,9 @@ let invert_eqeq iv1 iv2 =
     iv1.univs == iv2.univs
     && iv1.args == iv2.args
 
+let hasheq_ctx (nas1, c1) (nas2, c2) =
+  array_eqeq nas1 nas2 && c1 == c2
+
 let hasheq t1 t2 =
   match t1, t2 with
     | Rel n1, Rel n2 -> n1 == n2
@@ -1197,8 +1214,11 @@ let hasheq t1 t2 =
     | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
     | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2
     | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2
-    | Case (ci1,p1,iv1,c1,bl1), Case (ci2,p2,iv2,c2,bl2) ->
-      ci1 == ci2 && p1 == p2 && invert_eqeq iv1 iv2 && c1 == c2 && array_eqeq bl1 bl2
+    | Case (ci1,u1,pms1,p1,iv1,c1,bl1), Case (ci2,u2,pms2,p2,iv2,c2,bl2) ->
+      (** FIXME: use deeper equality for contexts *)
+      u1 == u2 && array_eqeq pms1 pms2 &&
+      ci1 == ci2 && hasheq_ctx p1 p2 &&
+      invert_eqeq iv1 iv2 && c1 == c2 && Array.equal hasheq_ctx bl1 bl2
     | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) ->
       Int.equal i1 i2
       && Array.equal Int.equal ln1 ln2
@@ -1247,7 +1267,7 @@ let sh_instance = Univ.Instance.share
    representation for [constr] using [hash_consing_functions] on
    leaves. *)
 let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
-  let rec hash_term t =
+  let rec hash_term (t : t) =
     match t with
       | Var i ->
         (Var (sh_id i), combinesmall 1 (Id.hash i))
@@ -1289,13 +1309,27 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
         let u', hu = sh_instance u in
         (Construct (sh_construct c, u'),
          combinesmall 11 (combine (Construct.SyntacticOrd.hash c) hu))
-      | Case (ci,p,iv,c,bl) ->
-        let p, hp = sh_rec p
-        and iv, hiv = sh_invert iv
-        and c, hc = sh_rec c in
-        let bl,hbl = hash_term_array bl in
-        let hbl = combine4 hc hp hiv hbl in
-        (Case (sh_ci ci, p, iv, c, bl), combinesmall 12 hbl)
+      | Case (ci,u,pms,p,iv,c,bl) ->
+        (** FIXME: use a dedicated hashconsing structure *)
+        let hcons_ctx (lna, c) =
+          let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in
+          let fold accu na = combine (hash_annot Name.hash na) accu in
+          let hna = Array.fold_left fold 0 lna in
+          let c, hc = sh_rec c in
+          (lna, c), combine hna hc
+        in
+        let u, hu = sh_instance u in
+        let pms,hpms = hash_term_array pms in
+        let p, hp = hcons_ctx p in
+        let iv, hiv = sh_invert iv in
+        let c, hc = sh_rec c in
+        let fold accu c =
+          let c, h = hcons_ctx c in
+          combine accu h, c
+        in
+        let hbl, bl = Array.fold_left_map fold 0 bl in
+        let hbl = combine (combine hc (combine hiv (combine hpms (combine hu hp)))) hbl in
+        (Case (sh_ci ci, u, pms, p, iv, c, bl), combinesmall 12 hbl)
       | Fix (ln,(lna,tl,bl)) ->
         let bl,hbl = hash_term_array bl in
         let tl,htl = hash_term_array tl in
@@ -1400,8 +1434,8 @@ let rec hash t =
       combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u))
     | Construct (c,u) ->
       combinesmall 11 (combine (Construct.CanOrd.hash c) (Instance.hash u))
-    | Case (_ , p, iv, c, bl) ->
-      combinesmall 12 (combine4 (hash c) (hash p) (hash_invert iv) (hash_term_array bl))
+    | Case (_ , u, pms, p, iv, c, bl) ->
+      combinesmall 12 (combine (combine (hash c) (combine (hash_invert iv) (combine (hash_term_array pms) (combine (Instance.hash u) (hash_under_context p))))) (hash_branches bl))
     | Fix (_ln ,(_, tl, bl)) ->
       combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
     | CoFix(_ln, (_, tl, bl)) ->
@@ -1426,6 +1460,11 @@ and hash_term_array t =
 and hash_term_list t =
   List.fold_left (fun acc t -> combine (hash t) acc) 0 t
 
+and hash_under_context (_, t) = hash t
+
+and hash_branches bl =
+  Array.fold_left (fun acc t -> combine acc (hash_under_context t)) 0 bl
+
 module CaseinfoHash =
 struct
   type t = case_info
@@ -1551,10 +1590,15 @@ let rec debug_print c =
   | Construct (((sp,i),j),u) ->
       str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
   | Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")"
-  | Case (_ci,p,iv,c,bl) -> v 0
-      (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++
-             debug_print c ++ debug_invert iv ++ str"of") ++ cut() ++
-       prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++
+  | Case (_ci,_u,pms,p,iv,c,bl) ->
+    let pr_ctx (nas, c) =
+      prvect_with_sep spc (fun na -> Name.print na.binder_name) nas ++ spc () ++ str "|-" ++ spc () ++
+        debug_print c
+    in
+    v 0 (hv 0 (str"Case " ++
+             debug_print c ++ cut () ++ str "as" ++ cut () ++ prlist_with_sep cut debug_print (Array.to_list pms) ++
+             cut () ++ str"return"++ cut () ++ pr_ctx p ++ debug_invert iv ++ cut () ++ str"with") ++ cut() ++
+       prlist_with_sep (fun _ -> brk(1,2)) pr_ctx (Array.to_list bl) ++
       cut() ++ str"end")
   | Fix f -> debug_print_fix debug_print f
   | CoFix(i,(lna,tl,bl)) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index ed63ac507c..17c7da1cf6 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -49,7 +49,7 @@ type case_info =
     ci_pp_info    : case_printing   (* not interpreted by the kernel *)
   }
 
-type ('constr, 'univs) case_invert =
+type ('constr, 'univs) pcase_invert =
   | NoInvert
   (** Normal reduction: match when the scrutinee is a constructor. *)
 
@@ -152,14 +152,30 @@ val mkRef : GlobRef.t Univ.puniverses -> constr
 
 (** Constructs a destructor of inductive type.
 
-    [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac]
+    [mkCase ci params p c ac] stand for match [c] as [x] in [I args] return [p] with [ac]
     presented as describe in [ci].
 
-    [p] structure is [fun args x -> "return clause"]
+
+    [p] structure is [args x |- "return clause"]
 
     [ac]{^ ith} element is ith constructor case presented as
-    {e lambda construct_args (without params). case_term } *)
-val mkCase : case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array -> constr
+    {e construct_args |- case_term } *)
+
+type 'constr pcase_branch = Name.t Context.binder_annot array * 'constr
+(** Names of the indices + name of self *)
+
+type 'types pcase_return = Name.t Context.binder_annot array * 'types
+(** Names of the branches *)
+
+type ('constr, 'types, 'univs) pcase =
+  case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
+
+type case_invert = (constr, Univ.Instance.t) pcase_invert
+type case_return = types pcase_return
+type case_branch = constr pcase_branch
+type case = (constr, types, Univ.Instance.t) pcase
+
+val mkCase : case -> constr
 
 (** If [recindxs = [|i1,...in|]]
       [funnames = [|f1,.....fn|]]
@@ -243,7 +259,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
 
   | Ind       of (inductive * 'univs)                 (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
   | Construct of (constructor * 'univs)              (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
-  | Case      of case_info * 'constr * ('constr,'univs) case_invert * 'constr * 'constr array
+  | Case      of case_info * 'univs * 'constr array * 'types pcase_return * ('constr,'univs) pcase_invert * 'constr * 'constr pcase_branch array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
@@ -351,7 +367,7 @@ Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
 return P in t1], or [if c then t1 else t2])
 @return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])]
 where [info] is pretty-printing information *)
-val destCase : constr -> case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array
+val destCase : constr -> case
 
 (** Destructs a projection *)
 val destProj : constr -> Projection.t * constr
@@ -421,12 +437,6 @@ val lift : int -> constr -> constr
 (** {6 Functionals working on expressions canonically abstracted over
        a local context (possibly with let-ins)} *)
 
-(** [map_under_context f l c] maps [f] on the immediate subterms of a
-    term abstracted over a context of length [n] (local definitions
-    are counted) *)
-
-val map_under_context : (constr -> constr) -> int -> constr -> constr
-
 (** [map_branches f br] maps [f] on the immediate subterms of an array
    of "match" branches [br] in canonical eta-let-expanded form; it is
    not recursive and the order with which subterms are processed is
@@ -434,7 +444,7 @@ val map_under_context : (constr -> constr) -> int -> constr -> constr
    types and possibly terms occurring in the context of each branch as
    well as the body of each branch *)
 
-val map_branches : (constr -> constr) -> case_info -> constr array -> constr array
+val map_branches : (constr -> constr) -> case_branch array -> case_branch array
 
 (** [map_return_predicate f p] maps [f] on the immediate subterms of a
    return predicate of a "match" in canonical eta-let-expanded form;
@@ -443,16 +453,7 @@ val map_branches : (constr -> constr) -> case_info -> constr array -> constr arr
    the types and possibly terms occurring in the context of each
    branch as well as the body of the predicate *)
 
-val map_return_predicate : (constr -> constr) -> case_info -> constr -> constr
-
-(** [map_under_context_with_binders g f n l c] maps [f] on the
-    immediate subterms of a term abstracted over a context of length
-    [n] (local definitions are counted); it preserves sharing; it
-    carries an extra data [n] (typically a lift index) which is
-    processed by [g] (which typically add 1 to [n]) at each binder
-    traversal *)
-
-val map_under_context_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr
+val map_return_predicate : (constr -> constr) -> case_return -> case_return
 
 (** [map_branches_with_binders f br] maps [f] on the immediate
    subterms of an array of "match" branches [br] in canonical
@@ -464,7 +465,7 @@ val map_under_context_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> '
    occurring in the context of the branch as well as the body of the
    branch *)
 
-val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array
+val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_branch array -> case_branch array
 
 (** [map_return_predicate_with_binders f p] maps [f] on the immediate
    subterms of a return predicate of a "match" in canonical
@@ -476,7 +477,7 @@ val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a ->
    occurring in the context of each branch as well as the body of the
    predicate *)
 
-val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr
+val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_return -> case_return
 
 (** {6 Functionals working on the immediate subterm of a construction } *)
 
@@ -486,7 +487,7 @@ val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -
 
 val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 
-val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a
+val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) pcase_invert -> 'a
 
 (** [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
@@ -494,21 +495,14 @@ val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a
 
 val map : (constr -> constr) -> constr -> constr
 
-val map_invert : ('a -> 'a) -> ('a, 'b) case_invert -> ('a, 'b) case_invert
-
-(** [map_user_view f c] maps [f] on the immediate subterms of [c]; it
-   differs from [map f c] in that the typing context and body of the
-   return predicate and of the branches of a [match] are considered as
-   immediate subterm of a [match] *)
-
-val map_user_view : (constr -> constr) -> constr -> constr
+val map_invert : ('a -> 'a) -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert
 
 (** Like {!map}, but also has an additional accumulator. *)
 
 val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
 
 val fold_map_invert : ('a -> 'b -> 'a * 'b) ->
-  'a -> ('b, 'c) case_invert -> 'a * ('b, 'c) case_invert
+  'a -> ('b, 'c) pcase_invert -> 'a * ('b, 'c) pcase_invert
 
 (** [map_with_binders g f n c] maps [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
@@ -525,7 +519,7 @@ val map_with_binders :
 
 val iter : (constr -> unit) -> constr -> unit
 
-val iter_invert : ('a -> unit) -> ('a, 'b) case_invert -> unit
+val iter_invert : ('a -> unit) -> ('a, 'b) pcase_invert -> unit
 
 (** [iter_with_binders g f n c] iters [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
@@ -604,7 +598,7 @@ val compare_head_gen_leq : Univ.Instance.t instance_compare_fn ->
   constr constr_compare_fn
 
 val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool)
-  -> ('a, 'b) case_invert -> ('a, 'b) case_invert -> bool
+  -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert -> bool
 
 (** {6 Hashconsing} *)
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3707a75157..930efa5d36 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -75,30 +75,30 @@ let share_univs cache r u l =
   let (u', args) = share cache r l in
     mkApp (instantiate_my_gr r (Instance.append u' u), args)
 
-let update_case cache ci iv modlist =
-  match share cache (IndRef ci.ci_ind) modlist with
-  | exception Not_found -> ci, iv
-  | u, l ->
-    let iv = match iv with
-      | NoInvert -> NoInvert
-      | CaseInvert {univs; args;} ->
-        let univs = Instance.append u univs in
-        let args = Array.append l args in
-        CaseInvert {univs; args;}
-    in
-    { ci with ci_npar = ci.ci_npar + Array.length l }, iv
-
 let is_empty_modlist (cm, mm) =
   Cmap.is_empty cm && Mindmap.is_empty mm
 
 let expmod_constr cache modlist c =
   let share_univs = share_univs cache in
-  let update_case = update_case cache in
   let rec substrec c =
     match kind c with
-      | Case (ci,p,iv,t,br) ->
-        let ci,iv = update_case ci iv modlist in
-        Constr.map substrec (mkCase (ci,p,iv,t,br))
+      | Case (ci, u, pms, p, iv, t, br) ->
+        begin match share cache (IndRef ci.ci_ind) modlist with
+        | (u', prefix) ->
+          let u = Instance.append u' u in
+          let pms = Array.append prefix pms in
+          let ci = { ci with ci_npar = ci.ci_npar + Array.length prefix } in
+          let iv = match iv with
+            | NoInvert -> NoInvert
+            | CaseInvert {univs; args;} ->
+              let univs = Instance.append u' univs in
+              let args = Array.append prefix args in
+              CaseInvert {univs; args;}
+          in
+          Constr.map substrec (mkCase (ci,u,pms,p,iv,t,br))
+        | exception Not_found ->
+          Constr.map substrec c
+        end
 
       | Ind (ind,u) ->
           (try
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ce12d65614..eb18d4b90e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -72,7 +72,7 @@ let constructor_instantiate mind u mib c =
   let s = ind_subst mind mib u in
     substl s (subst_instance_constr u c)
 
-let instantiate_params full t u args sign =
+let instantiate_params t u args sign =
   let fail () =
     anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in
   let (rem_args, subs, ty) =
@@ -81,8 +81,7 @@ let instantiate_params full t u args sign =
         match (decl, largs, kind ty) with
           | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
           | (LocalDef (_,b,_), _, LetIn(_,_,_,t))    ->
-             (largs, (substl subs (subst_instance_constr u b))::subs, t)
-          | (_,[],_)                -> if full then fail() else ([], subs, ty)
+            (largs, (substl subs (subst_instance_constr u b))::subs, t)
           | _                       -> fail ())
       sign
       ~init:(args,[],t)
@@ -93,11 +92,11 @@ let instantiate_params full t u args sign =
 let full_inductive_instantiate mib u params sign =
   let dummy = Sorts.prop in
   let t = Term.mkArity (Vars.subst_instance_context u sign,dummy) in
-    fst (Term.destArity (instantiate_params true t u params mib.mind_params_ctxt))
+    fst (Term.destArity (instantiate_params t u params mib.mind_params_ctxt))
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
   let inst_ind = constructor_instantiate mind u mib t in
-   instantiate_params true inst_ind u params mib.mind_params_ctxt
+   instantiate_params inst_ind u params mib.mind_params_ctxt
 
 (************************************************************************)
 (************************************************************************)
@@ -372,6 +371,91 @@ let check_correct_arity env c pj ind specif params =
   with LocalArity kinds ->
     error_elim_arity env ind c pj kinds
 
+(** {6 Changes of representation of Case nodes} *)
+
+(** Provided:
+    - a universe instance [u]
+    - a term substitution [subst]
+    - name replacements [nas]
+    [instantiate_context u subst nas ctx] applies both [u] and [subst] to [ctx]
+    while replacing names using [nas] (order reversed)
+*)
+let instantiate_context u subst nas ctx =
+  let rec instantiate i ctx = match ctx with
+  | [] -> assert (Int.equal i (-1)); []
+  | LocalAssum (_, ty) :: ctx ->
+    let ctx = instantiate (pred i) ctx in
+    let ty = substnl subst i (subst_instance_constr u ty) in
+    LocalAssum (nas.(i), ty) :: ctx
+  | LocalDef (_, ty, bdy) :: ctx ->
+    let ctx = instantiate (pred i) ctx in
+    let ty = substnl subst i (subst_instance_constr u ty) in
+    let bdy = substnl subst i (subst_instance_constr u bdy) in
+    LocalDef (nas.(i), ty, bdy) :: ctx
+  in
+  instantiate (Array.length nas - 1) ctx
+
+let expand_case_specif mib (ci, u, params, p, iv, c, br) =
+  (* Γ ⊢ c : I@{u} params args *)
+  (* Γ, indices, self : I@{u} params indices ⊢ p : Type *)
+  let mip = mib.mind_packets.(snd ci.ci_ind) in
+  let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list params) in
+  (* Expand the return clause *)
+  let ep =
+    let (nas, p) = p in
+    let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
+    let self =
+      let args = Context.Rel.to_extended_vect mkRel 0 mip.mind_arity_ctxt in
+      let inst = Instance.of_array (Array.init (Instance.length u) Level.var) in
+      mkApp (mkIndU (ci.ci_ind, inst), args)
+    in
+    let realdecls = LocalAssum (Context.anonR, self) :: realdecls in
+    let realdecls = instantiate_context u paramsubst nas realdecls in
+    Term.it_mkLambda_or_LetIn p realdecls
+  in
+  (* Expand the branches *)
+  let subst = paramsubst @ ind_subst (fst ci.ci_ind) mib u in
+  let ebr =
+    let build_one_branch i (nas, br) (ctx, _) =
+      let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in
+      let ctx = instantiate_context u subst nas ctx in
+      Term.it_mkLambda_or_LetIn br ctx
+    in
+    Array.map2_i build_one_branch br mip.mind_nf_lc
+  in
+  (ci, ep, iv, c, ebr)
+
+let expand_case env (ci, _, _, _, _, _, _ as case) =
+  let specif = Environ.lookup_mind (fst ci.ci_ind) env in
+  expand_case_specif specif case
+
+let contract_case env (ci, p, iv, c, br) =
+  let (mib, mip) = lookup_mind_specif env ci.ci_ind in
+  let (arity, p) = Term.decompose_lam_n_decls (mip.mind_nrealdecls + 1) p in
+  let (u, pms) = match arity with
+  | LocalAssum (_, ty) :: _ ->
+    (** Last binder is the self binder for the term being eliminated *)
+    let (ind, args) = decompose_appvect ty in
+    let (ind, u) = destInd ind in
+    let () = assert (Ind.CanOrd.equal ind ci.ci_ind) in
+    let pms = Array.sub args 0 mib.mind_nparams in
+    (** Unlift the parameters from under the index binders *)
+    let dummy = List.make mip.mind_nrealdecls mkProp in
+    let pms = Array.map (fun c -> Vars.substl dummy c) pms in
+    (u, pms)
+  | _ -> assert false
+  in
+  let p =
+    let nas = Array.of_list (List.rev_map get_annot arity) in
+    (nas, p)
+  in
+  let map i br =
+    let (ctx, br) = Term.decompose_lam_n_decls mip.mind_consnrealdecls.(i) br in
+    let nas = Array.of_list (List.rev_map get_annot ctx) in
+    (nas, br)
+  in
+  (ci, u, pms, p, iv, c, Array.mapi map br)
 
 (************************************************************************)
 (* Type of case branches *)
@@ -793,7 +877,8 @@ let rec subterm_specif renv stack t =
   let f,l = decompose_app (whd_all renv.env t) in
     match kind f with
     | Rel k -> subterm_var k renv
-    | Case (ci,p,_iv,c,lbr) -> (* iv ignored: it's just a cache *)
+    | Case (ci, u, pms, p, iv, c, lbr) -> (* iv ignored: it's just a cache *)
+      let (ci, p, _iv, c, lbr) = expand_case renv.env (ci, u, pms, p, iv, c, lbr) in
        let stack' = push_stack_closures renv l stack in
        let cases_spec =
          branches_specif renv (lazy_subterm_specif renv [] c) ci
@@ -1018,7 +1103,8 @@ let check_one_fix renv recpos trees def =
                       check_rec_call renv stack (Term.applist(lift p c,l))
               end
 
-        | Case (ci,p,iv,c_0,lrest) -> (* iv ignored: it's just a cache *)
+        | Case (ci, u, pms, ret, iv, c_0, br) -> (* iv ignored: it's just a cache *)
+            let (ci, p, _iv, c_0, lrest) = expand_case renv.env (ci, u, pms, ret, iv, c_0, br) in
             begin try
               List.iter (check_rec_call renv []) (c_0::p::l);
               (* compute the recarg info for the arguments of each branch *)
@@ -1040,7 +1126,7 @@ let check_one_fix renv recpos trees def =
                   (* the call to whd_betaiotazeta will reduce the
                      apparent iota redex away *)
                   check_rec_call renv []
-                    (Term.applist (mkCase (ci,p,iv,c_0,lrest), l))
+                    (Term.applist (mkCase (ci, u, pms, ret, iv, c_0, br), l))
               | _ -> Exninfo.iraise exn
             end
 
@@ -1324,13 +1410,14 @@ let check_one_cofix env nbfix def deftype =
             else
               raise (CoFixGuardError (env,UnguardedRecursiveCall c))
 
-        | Case (_,p,_,tm,vrest) -> (* iv ignored: just a cache *)
-           begin
-             let tree = match restrict_spec env (Subterm (Strict, tree)) p with
-             | Dead_code -> assert false
-             | Subterm (_, tree') -> tree'
-             | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c))
-             in
+        | Case (ci, u, pms, p, iv, tm, br) -> (* iv ignored: just a cache *)
+          begin
+            let (_, p, _iv, tm, vrest) = expand_case env (ci, u, pms, p, iv, tm, br) in
+            let tree = match restrict_spec env (Subterm (Strict, tree)) p with
+            | Dead_code -> assert false
+            | Subterm (_, tree') -> tree'
+            | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c))
+            in
                if (noccur_with_meta n nbfix p) then
                  if (noccur_with_meta n nbfix tm) then
                    if (List.for_all (noccur_with_meta n nbfix) args) then
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 78658dc4de..5808a3fa65 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -79,6 +79,23 @@ val arities_of_specif : MutInd.t puniverses -> mind_specif -> types array
 
 val inductive_params : mind_specif -> int
 
+(** Given a pattern-matching represented compactly, expands it so as to produce
+    lambda and let abstractions in front of the return clause and the pattern
+    branches. *)
+val expand_case : env -> case -> (case_info * constr * case_invert * constr * constr array)
+
+val expand_case_specif : mutual_inductive_body -> case -> (case_info * constr * case_invert * constr * constr array)
+
+(** Dual operation of the above. Fails if the return clause or branch has not
+    the expected form. *)
+val contract_case : env -> (case_info * constr * case_invert * constr * constr array) -> case
+
+(** [instantiate_context u subst nas ctx] applies both [u] and [subst]
+    to [ctx] while replacing names using [nas] (order reversed). In particular,
+    assumes that [ctx] and [nas] have the same length. *)
+val instantiate_context : Instance.t -> Vars.substl -> Name.t Context.binder_annot array ->
+  rel_context -> rel_context
+
 (** [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
       <p>Cases (c :: (I args)) of b1..bn end
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index d02f92ef26..50c3ba1cc6 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -198,7 +198,9 @@ let rec infer_fterm cv_pb infos variances hd stk =
     let variances = infer_vect infos variances elems in
     infer_stack infos variances stk
 
-  | FCaseInvert (_,p,_,_,br,e) ->
+  | FCaseInvert (ci, u, pms, p, _, _, br, e) ->
+    let mib = Environ.lookup_mind (fst ci.ci_ind) (info_env (fst infos)) in
+    let (_, p, _, _, br) = Inductive.expand_case_specif mib (ci, u, pms, p, NoInvert, mkProp, br) in
     let infer c variances = infer_fterm CONV infos variances (mk_clos e c) [] in
     let variances = infer p variances in
     Array.fold_right infer br variances
@@ -217,7 +219,10 @@ and infer_stack infos variances (stk:CClosure.stack) =
       | Zfix (fx,a) ->
         let variances = infer_fterm CONV infos variances fx [] in
         infer_stack infos variances a
-      | ZcaseT (_, p, br, e) ->
+      | ZcaseT (ci,u,pms,p,br,e) ->
+        let dummy = mkProp in
+        let case = (ci, u, pms, p, NoInvert, dummy, br) in
+        let (_, p, _, _, br) = Inductive.expand_case (info_env (fst infos)) case in
         let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
         infer_vect infos variances (Array.map (mk_clos e) br)
       | Zshift _ -> variances
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 4778bf1121..c5ac57a2cd 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -355,21 +355,26 @@ let rec map_kn f f' c =
       | Construct (((kn,i),j),u) ->
           let kn' = f kn in
           if kn'==kn then c else mkConstructU (((kn',i),j),u)
-      | Case (ci,p,iv,ct,l) ->
+      | Case (ci,u,pms,p,iv,ct,l) ->
           let ci_ind =
             let (kn,i) = ci.ci_ind in
             let kn' = f kn in
             if kn'==kn then ci.ci_ind else kn',i
           in
-          let p' = func p in
+          let f_ctx (nas, c as d) =
+            let c' = func c in
+            if c' == c then d else (nas, c')
+          in
+          let pms' = Array.Smart.map func pms in
+          let p' = f_ctx p in
           let iv' = map_invert func iv in
           let ct' = func ct in
-          let l' = Array.Smart.map func l in
-            if (ci.ci_ind==ci_ind && p'==p && iv'==iv
+          let l' = Array.Smart.map f_ctx l in
+            if (ci.ci_ind==ci_ind && pms'==pms && p'==p && iv'==iv
                 && l'==l && ct'==ct)then c
             else
-              mkCase ({ci with ci_ind = ci_ind},
-                      p',iv',ct', l')
+              mkCase ({ci with ci_ind = ci_ind}, u,
+                      pms',p',iv',ct', l')
       | Cast (ct,k,t) ->
           let ct' = func ct in
           let t'= func t in
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 09db29d222..c19b883e3d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2101,7 +2101,7 @@ let compile_deps env sigma prefix init t =
   | Proj (p,c) ->
     let init = compile_mind_deps env prefix init (Projection.mind p) in
     aux env lvl init c
-  | Case (ci, _p, _iv, _c, _ac) ->
+  | Case (ci, _u, _pms, _p, _iv, _c, _ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix init mind in
       fold_constr_with_binders succ (aux env) lvl init t
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index b27c53ef0f..f3b483467d 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -535,7 +535,8 @@ let rec lambda_of_constr cache env sigma c =
     let prefix = get_mind_prefix env (fst ind) in
     mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|]
 
-  | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *)
+  | Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *)
+    let (ci, t, _iv, a, branches) = Inductive.expand_case env (ci, u, pms, t, iv, a, br) in
     let (mind,i as ind) = ci.ci_ind in
     let mib = lookup_mind mind env in
     let oib = mib.mind_packets.(i) in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cf40263f61..1e39756d47 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -56,7 +56,7 @@ let compare_stack_shape stk1 stk2 =
     | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
     | (Zproj _p1::s1, Zproj _p2::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
-    | (ZcaseT(_c1,_,_,_)::s1, ZcaseT(_c2,_,_,_)::s2) ->
+    | (ZcaseT(_c1,_,_,_,_,_)::s1, ZcaseT(_c2,_,_,_,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
     | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -74,7 +74,7 @@ type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
   | Zlproj of Projection.Repr.t * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
-  | Zlcase of case_info * lift * constr * constr array * fconstr subs
+  | Zlcase of case_info * lift * Univ.Instance.t * constr array * case_return * case_branch array * fconstr subs
   | Zlprimitive of
      CPrimitives.t * pconstant * lft_fconstr list * lft_fconstr next_native_args
 and lft_constr_stack = lft_constr_stack_elt list
@@ -109,8 +109,8 @@ let pure_stack lfts stk =
             | (Zfix(fx,a),(l,pstk)) ->
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
-            | (ZcaseT(ci,p,br,e),(l,pstk)) ->
-                (l,Zlcase(ci,l,p,br,e)::pstk)
+            | (ZcaseT(ci,u,pms,p,br,e),(l,pstk)) ->
+                (l,Zlcase(ci,l,u,pms,p,br,e)::pstk)
             | (Zprimitive(op,c,rargs,kargs),(l,pstk)) ->
                 (l,Zlprimitive(op,c,List.map (fun t -> (l,t)) rargs,
                             List.map (fun (k,t) -> (k,(l,t))) kargs)::pstk))
@@ -233,6 +233,9 @@ let convert_instances ~flex u u' (s, check) =
 
 exception MustExpand
 
+let convert_instances_cumul pb var u u' (s, check) =
+  (check.compare_cumul_instances pb var u u' s, check)
+
 let get_cumulativity_constraints cv_pb variance u u' =
   match cv_pb with
   | CONV ->
@@ -294,8 +297,6 @@ let conv_table_key infos ~nargs k1 k2 cuniv =
   | RelKey n, RelKey n' when Int.equal n n' -> cuniv
   | _ -> raise NotConvertible
 
-exception IrregularPatternShape
-
 let unfold_ref_with_args infos tab fl v =
   match unfold_reference infos tab fl with
   | Def def -> Some (def, v)
@@ -327,17 +328,6 @@ let push_relevance infos r =
 let push_relevances infos nas =
   { infos with cnv_inf = CClosure.push_relevances infos.cnv_inf nas }
 
-let rec skip_pattern infos relevances n c1 c2 =
-  if Int.equal n 0 then {infos with cnv_inf = CClosure.set_info_relevances infos.cnv_inf relevances}, c1, c2
-  else match kind c1, kind c2 with
-    | Lambda (x, _, c1), Lambda (_, _, c2) ->
-      skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2
-    | _ -> raise IrregularPatternShape
-
-let skip_pattern infos n c1 c2 =
-  if Int.equal n 0 then infos, c1, c2
-  else skip_pattern infos (info_relevances infos.cnv_inf) n c1 c2
-
 let is_irrelevant infos lft c =
   let env = info_env infos.cnv_inf in
   try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false
@@ -364,6 +354,39 @@ let eta_expand_constructor env ((ind,ctor),u as pctor) =
   let c = Term.it_mkLambda_or_LetIn c ctx in
   inject c
 
+let inductive_subst (mind, _) mib u pms =
+  let open Context.Rel.Declaration in
+  let ntypes = mib.mind_ntypes in
+  let rec self i accu =
+    if Int.equal i ntypes then accu
+    else self (i + 1) (subs_cons (inject (mkIndU ((mind, i), u))) accu)
+  in
+  let accu = self 0 (subs_id 0) in
+  let rec mk_pms pms ctx = match ctx, pms with
+  | [], [] -> accu
+  | LocalAssum _ :: ctx, c :: pms ->
+    let subs = mk_pms pms ctx in
+    subs_cons c subs
+  | LocalDef (_, c, _) :: ctx, pms ->
+    let c = Vars.subst_instance_constr u c in
+    let subs = mk_pms pms ctx in
+    subs_cons (mk_clos subs c) subs
+  | LocalAssum _ :: _, [] | [], _ :: _ -> assert false
+  in
+  mk_pms (List.rev pms) mib.mind_params_ctxt
+
+let esubst_of_rel_context_instance ctx u args e =
+  let open Context.Rel.Declaration in
+  let rec aux lft e args ctx = match ctx with
+  | [] -> lft, e
+  | LocalAssum _ :: ctx -> aux (lft + 1) (subs_lift e) (subs_lift args) ctx
+  | LocalDef (_, c, _) :: ctx ->
+    let c = Vars.subst_instance_constr u c in
+    let c = mk_clos args c in
+    aux lft (subs_cons c e) (subs_cons c args) ctx
+  in
+  aux 0 e args (List.rev ctx)
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
   try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
@@ -672,13 +695,23 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         if Float64.equal f1 f2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
-    | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) ->
+    | FCaseInvert (ci1,u1,pms1,p1,_,_,br1,e1), FCaseInvert (ci2,u2,pms2,p2,_,_,br2,e2) ->
       (if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible);
       let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in
-      let ccnv = ccnv CONV l2r infos el1 el2 in
-      let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in
-      Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv)
-        br1 br2 cuniv
+      let fold c1 c2 cuniv = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
+      (** FIXME: cache the presence of let-bindings in the case_info *)
+      let mind = Environ.lookup_mind (fst ci1.ci_ind) (info_env infos.cnv_inf) in
+      let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in
+      let cuniv =
+        let ind = (mind,snd ci1.ci_ind) in
+        let nargs = inductive_cumulativity_arguments ind in
+        convert_inductives CONV ind nargs u1 u2 cuniv
+      in
+      let pms1 = Array.map_to_list (fun c -> mk_clos e1 c) pms1 in
+      let pms2 = Array.map_to_list (fun c -> mk_clos e2 c) pms2 in
+      let cuniv = List.fold_right2 fold pms1 pms2 cuniv in
+      let cuniv = convert_return_clause ci1.ci_ind mind mip l2r infos e1 e2 el1 el2 u1 u2 pms1 pms2 p1 p2 cuniv in
+      convert_branches ci1.ci_ind mind mip l2r infos e1 e2 el1 el2 u1 u2 pms1 pms2 br1 br2 cuniv
 
     | FArray (u1,t1,ty1), FArray (u2,t2,ty2) ->
       let len = Parray.length_int t1 in
@@ -714,11 +747,27 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 let cu2 = f fx1 fx2 cu1 in
                 cmp_rec a1 a2 cu2
-            | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) ->
+            | (Zlcase(ci1,l1,u1,pms1,p1,br1,e1),Zlcase(ci2,l2,u2,pms2,p2,br2,e2)) ->
                 if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then
                   raise NotConvertible;
-                let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in
-                convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2
+                let cu = cu1 in
+                (** FIXME: cache the presence of let-bindings in the case_info *)
+                let mind = Environ.lookup_mind (fst ci1.ci_ind) (info_env infos.cnv_inf) in
+                let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in
+                let cu =
+                  if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+                    convert_instances ~flex:false u1 u2 cu
+                  else
+                    match mind.Declarations.mind_variance with
+                    | None -> convert_instances ~flex:false u1 u2 cu
+                    | Some variances -> convert_instances_cumul CONV variances u1 u2 cu
+                in
+                let pms1 = Array.map_to_list (fun c -> mk_clos e1 c) pms1 in
+                let pms2 = Array.map_to_list (fun c -> mk_clos e2 c) pms2 in
+                let fold_params c1 c2 accu = f (l1, c1) (l2, c2) accu in
+                let cu = List.fold_right2 fold_params pms1 pms2 cu in
+                let cu = convert_return_clause ci1.ci_ind mind mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu in
+                convert_branches ci1.ci_ind mind mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 br1 br2 cu
             | (Zlprimitive(op1,_,rargs1,kargs1),Zlprimitive(op2,_,rargs2,kargs2)) ->
               if not (CPrimitives.equal op1 op2) then raise NotConvertible else
                 let cu2 = List.fold_right2 f rargs1 rargs2 cu1 in
@@ -743,21 +792,55 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
     fold 0 cuniv
   else raise NotConvertible
 
-and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv =
-  (** Skip comparison of the pattern types. We know that the two terms are
-      living in a common type, thus this check is useless. *)
-  let fold n c1 c2 cuniv = match skip_pattern infos n c1 c2 with
-  | (infos, c1, c2) ->
-    let lft1 = el_liftn n lft1 in
-    let lft2 = el_liftn n lft2 in
+and convert_under_context l2r infos e1 e2 lft1 lft2 ctx (nas1, c1) (nas2, c2) cu =
+  let n = Array.length nas1 in
+  let () = assert (Int.equal n (Array.length nas2)) in
+  let n, e1, e2 = match ctx with
+  | None -> (* nolet *)
     let e1 = subs_liftn n e1 in
     let e2 = subs_liftn n e2 in
-    ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
-  | exception IrregularPatternShape ->
-    (** Might happen due to a shape invariant that is not enforced *)
-    ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
+    (n, e1, e2)
+  | Some (ctx, u1, u2, args1, args2) ->
+    let n1, e1 = esubst_of_rel_context_instance ctx u1 args1 e1 in
+    let n2, e2 = esubst_of_rel_context_instance ctx u2 args2 e2 in
+    let () = assert (Int.equal n1 n2) in
+    n1, e1, e2
+  in
+  let lft1 = el_liftn n lft1 in
+  let lft2 = el_liftn n lft2 in
+  let infos = push_relevances infos nas1 in
+  ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cu
+
+and convert_return_clause ind mib mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu =
+  let ctx =
+    if Int.equal mip.mind_nrealargs mip.mind_nrealdecls then None
+    else
+      let ctx, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
+      let pms1 = inductive_subst ind mib u1 pms1 in
+      let pms2 = inductive_subst ind mib u1 pms2 in
+      let open Context.Rel.Declaration in
+      (* Add the inductive binder *)
+      let dummy = mkProp in
+      let ctx = LocalAssum (Context.anonR, dummy) :: ctx in
+      Some (ctx, u1, u2, pms1, pms2)
+  in
+  convert_under_context l2r infos e1 e2 l1 l2 ctx p1 p2 cu
+
+and convert_branches ind mib mip l2r infos e1 e2 lft1 lft2 u1 u2 pms1 pms2 br1 br2 cuniv =
+  let fold i (ctx, _) cuniv =
+    let ctx =
+      if Int.equal mip.mind_consnrealdecls.(i) mip.mind_consnrealargs.(i) then None
+      else
+        let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in
+        let pms1 = inductive_subst ind mib u1 pms1 in
+        let pms2 = inductive_subst ind mib u2 pms2 in
+        Some (ctx, u1, u2, pms1, pms2)
+    in
+    let c1 = br1.(i) in
+    let c2 = br2.(i) in
+    convert_under_context l2r infos e1 e2 lft1 lft2 ctx c1 c2 cuniv
   in
-  Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv
+  Array.fold_right_i fold mip.mind_nf_lc cuniv
 
 and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
 | [], [] -> cuniv
diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml
index f12b8cba37..986fc685d1 100644
--- a/kernel/relevanceops.ml
+++ b/kernel/relevanceops.ml
@@ -61,7 +61,7 @@ let rec relevance_of_fterm env extra lft f =
       | FProj (p, _) -> relevance_of_projection env p
       | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance
       | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance
-      | FCaseT (ci, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _) -> ci.ci_relevance
+      | FCaseT (ci, _, _, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _, _, _) -> ci.ci_relevance
       | FLambda (len, tys, bdy, e) ->
         let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in
         let lft = Esubst.el_liftn len lft in
@@ -97,7 +97,7 @@ and relevance_of_term_extra env extra lft subs c =
   | App (c, _) -> relevance_of_term_extra env extra lft subs c
   | Const (c,_) -> relevance_of_constant env c
   | Construct (c,_) -> relevance_of_constructor env c
-  | Case (ci, _, _, _, _) -> ci.ci_relevance
+  | Case (ci, _, _, _, _, _, _) -> ci.ci_relevance
   | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
   | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
   | Proj (p, _) -> relevance_of_projection env p
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 802a32b0e7..83e41a63ec 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -548,7 +548,9 @@ let rec execute env cstr =
     | Construct c ->
       cstr, type_of_constructor env c
 
-    | Case (ci,p,iv,c,lf) ->
+    | Case (ci, u, pms, p, iv, c, lf) ->
+        (** FIXME: change type_of_case to handle the compact form *)
+        let (ci, p, iv, c, lf) = expand_case env (ci, u, pms, p, iv, c, lf) in
         let c', ct = execute env c in
         let iv' = match iv with
           | NoInvert -> NoInvert
@@ -563,7 +565,7 @@ let rec execute env cstr =
         let lf', lft = execute_array env lf in
         let ci', t = type_of_case env ci p' pt iv' c' ct lf' lft in
         let cstr = if ci == ci' && c == c' && p == p' && iv == iv' && lf == lf' then cstr
-          else mkCase(ci',p',iv',c',lf')
+          else mkCase (Inductive.contract_case env (ci',p',iv',c',lf'))
         in
         cstr, t
 
@@ -720,11 +722,6 @@ let judge_of_inductive env indu =
 let judge_of_constructor env cu =
   make_judge (mkConstructU cu) (type_of_constructor env cu)
 
-let judge_of_case env ci pj iv cj lfj =
-  let lf, lft = dest_judgev lfj in
-  let ci, t = type_of_case env ci pj.uj_val pj.uj_type iv cj.uj_val cj.uj_type lf lft in
-  make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, iv, cj.uj_val, lft)) t
-
 (* Building type of primitive operators and type *)
 
 let type_of_prim_const env _u c =
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index d381e55dd6..5ea7163f72 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -92,12 +92,6 @@ val judge_of_cast :
 val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment
 val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment
 
-(** {6 Type of Cases. } *)
-val judge_of_case : env -> case_info
-  -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment
-  -> unsafe_judgment array
-  -> unsafe_judgment
-
 (** {6 Type of global references. } *)
 
 val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
diff --git a/kernel/vars.ml b/kernel/vars.ml
index a446fa413c..0f71057787 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -253,12 +253,21 @@ let subst_univs_level_constr subst c =
            if u' == u then t else
              (changed := true; mkSort (Sorts.sort_of_univ u'))
 
-      | Case (ci,p,CaseInvert {univs;args},c,br) ->
-        if Univ.Instance.is_empty univs then Constr.map aux t
+      | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
+        if Univ.Instance.is_empty u && Univ.Instance.is_empty univs then Constr.map aux t
         else
+          let u' = f u in
           let univs' = f univs in
-          if univs' == univs then Constr.map aux t
-          else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)))
+          if u' == u && univs' == univs then Constr.map aux t
+          else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br)))
+
+      | Case (ci, u, pms, p, NoInvert, c, br) ->
+        if Univ.Instance.is_empty u then Constr.map aux t
+        else
+          let u' = f u in
+          if u' == u then Constr.map aux t
+          else
+            (changed := true; Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br)))
 
       | Array (u,elems,def,ty) ->
         let u' = f u in
@@ -305,10 +314,19 @@ let subst_instance_constr subst c =
           if u' == u then t else
             (mkSort (Sorts.sort_of_univ u'))
 
-      | Case (ci,p,CaseInvert {univs;args},c,br) ->
+      | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
+        let u' = f u in
         let univs' = f univs in
-        if univs' == univs then Constr.map aux t
-        else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))
+        if u' == u && univs' == univs then Constr.map aux t
+        else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br))
+
+      | Case (ci, u, pms, p, NoInvert, c, br) ->
+        if Univ.Instance.is_empty u then Constr.map aux t
+        else
+          let u' = f u in
+          if u' == u then Constr.map aux t
+          else
+            Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br))
 
       | Array (u,elems,def,ty) ->
         let u' = f u in
@@ -348,8 +366,11 @@ let universes_of_constr c =
     | Array (u,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels u) s in
       Constr.fold aux s c
-    | Case (_,_,CaseInvert {univs;args=_},_,_) ->
+    | Case (_, u, _, _, CaseInvert {univs;args=_},_ ,_) ->
+      let s = LSet.fold LSet.add (Instance.levels u) s in
       let s = LSet.fold LSet.add (Instance.levels univs) s in
       Constr.fold aux s c
+    | Case (_, u, _, _, NoInvert, _, _) ->
+      Constr.fold aux (LSet.fold LSet.add (Instance.levels u) s) c
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index 390fa58883..91de58b0e6 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -674,7 +674,8 @@ let rec lambda_of_constr env c =
 
   | Construct _ ->  lambda_of_app env c empty_args
 
-  | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *)
+  | Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *)
+    let (ci, t, _iv, a, branches) = Inductive.expand_case env.global_env (ci, u, pms, t, iv, a, br) in
     let ind = ci.ci_ind in
     let mib = lookup_mind (fst ind) env.global_env in
     let oib = mib.mind_packets.(snd ind) in
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index ac2058ba1b..343fb0b1fe 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -112,13 +112,13 @@ module Bool = struct
       else if head === negb && Array.length args = 1 then
         Negb (aux args.(0))
       else Var (Env.add env c)
-    | Case (info, r, _iv, arg, pats) ->
+    | Case (info, _, _, _, _, arg, pats) ->
       let is_bool =
         let i = info.ci_ind in
         Names.Ind.CanOrd.equal i (Lazy.force ind)
       in
       if is_bool then
-        Ifb ((aux arg), (aux pats.(0)), (aux pats.(1)))
+        Ifb ((aux arg), (aux (snd pats.(0))), (aux (snd pats.(1))))
       else
         Var (Env.add env c)
     | _ ->
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6869f9c47e..0cad192332 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -672,9 +672,11 @@ let rec extract_term env sg mle mlt c args =
         (* we unify it with an fresh copy of the stored type of [Rel n]. *)
         let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
         in extract_app env sg mle mlt extract_rel args
-    | Case ({ci_ind=ip},_,iv,c0,br) ->
-      (* If invert_case then this is a match that will get erased later, but right now we don't care. *)
-      extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
+    | Case (ci, u, pms, r, iv, c0, br) ->
+        (* If invert_case then this is a match that will get erased later, but right now we don't care. *)
+        let (ip, r, iv, c0, br) = EConstr.expand_case env sg (ci, u, pms, r, iv, c0, br) in
+        let ip = ci.ci_ind in
+        extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
     | Fix ((_,i),recd) ->
         extract_app env sg mle mlt (extract_fix env sg mle i recd) args
     | CoFix (i,recd) ->
@@ -1078,9 +1080,13 @@ let fake_match_projection env p =
         let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
         fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem
       else
-        let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in
-        let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in
-        let body = mkCase (ci, p, NoInvert, mkRel 1, [|branch|]) in
+        let p = ([|x|], liftn 1 2 ty) in
+        let branch =
+          let nas = Array.of_list (List.rev_map Context.Rel.Declaration.get_annot ctx) in
+          (nas, mkRel (List.length ctx - (j - 1)))
+        in
+        let params = Context.Rel.to_extended_vect mkRel 1 paramslet in
+        let body = mkCase (ci, u, params, p, NoInvert, mkRel 1, [|branch|]) in
         it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
     | LocalDef (_,c,t) :: rem ->
       let c = liftn 1 j c in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index c62bc73e41..e208ba9a5c 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -67,10 +67,13 @@ let unif env evd t1 t2=
           | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
           | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
               Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
-          | Case (_,pa,_,ca,va),Case (_,pb,_,cb,vb)->
-            Queue.add (pa,pb) bige;
-            Queue.add (ca,cb) bige;
-            let l=Array.length va in
+          | Case (cia,ua,pmsa,pa,iva,ca,va),Case (cib,ub,pmsb,pb,ivb,cb,vb)->
+            let env = Global.env () in
+            let (cia,pa,iva,ca,va) = EConstr.expand_case env evd (cia,ua,pmsa,pa,iva,ca,va) in
+            let (cib,pb,iva,cb,vb) = EConstr.expand_case env evd (cib,ub,pmsb,pb,ivb,cb,vb) in
+              Queue.add (pa,pb) bige;
+              Queue.add (ca,cb) bige;
+              let l=Array.length va in
                 if not (Int.equal l (Array.length vb)) then
                   raise (UFAIL (nt1,nt2))
                 else
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 67b6839b6e..3234d40f73 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -598,12 +598,12 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
         let sigma = Proofview.Goal.sigma g in
         (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
         match EConstr.kind sigma dyn_infos.info with
-        | Case (ci, ct, iv, t, cb) ->
+        | Case (ci, u, pms, ct, iv, t, cb) ->
           let do_finalize_t dyn_info' =
             Proofview.Goal.enter (fun g ->
                 let t = dyn_info'.info in
                 let dyn_infos =
-                  {dyn_info' with info = mkCase (ci, ct, iv, t, cb)}
+                  {dyn_info' with info = mkCase (ci, u, pms, ct, iv, t, cb)}
                 in
                 let g_nb_prod =
                   nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g)
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index c344fdd611..cbdebb7bbc 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -972,7 +972,7 @@ and intros_with_rewrite_aux () : unit Proofview.tactic =
                     ( UnivGen.constr_of_monomorphic_global
                     @@ Coqlib.lib_ref "core.False.type" )) ->
           tauto
-        | Case (_, _, _, v, _) ->
+        | Case (_, _, _, _, _, v, _) ->
           tclTHENLIST [simplest_case v; intros_with_rewrite ()]
         | LetIn _ ->
           tclTHENLIST
@@ -1005,7 +1005,7 @@ let rec reflexivity_with_destruct_cases () =
               (snd (destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g))).(
               2)
           with
-          | Case (_, _, _, v, _) ->
+          | Case (_, _, _, _, _, v, _) ->
             tclTHENLIST
               [ simplest_case v
               ; intros
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9d896e9182..9e9444951f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -301,10 +301,11 @@ let check_not_nested env sigma forbidden e =
     | Const _ -> ()
     | Ind _ -> ()
     | Construct _ -> ()
-    | Case (_, t, _, e, a) ->
+    | Case (_, _, pms, (_, t), _, e, a) ->
+      Array.iter check_not_nested pms;
       check_not_nested t;
       check_not_nested e;
-      Array.iter check_not_nested a
+      Array.iter (fun (_, c) -> check_not_nested c) a
     | Fix _ -> user_err Pp.(str "check_not_nested : Fix")
     | CoFix _ -> user_err Pp.(str "check_not_nested : Fix")
   in
@@ -367,7 +368,7 @@ type journey_info =
           -> unit Proofview.tactic)
       -> ( case_info
            * constr
-           * (constr, EInstance.t) case_invert
+           * case_invert
            * constr
            * constr array
          , constr )
@@ -472,7 +473,8 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) =
             ++ Printer.pr_leconstr_env env sigma expr_info.info
             ++ str " can not contain a recursive call to "
             ++ Id.print expr_info.f_id ) )
-      | Case (ci, t, iv, a, l) ->
+      | Case (ci, u, pms, t, iv, a, l) ->
+        let (ci, t, iv, a, l) = EConstr.expand_case env sigma (ci, u, pms, t, iv, a, l) in
         let continuation_tac_a =
           jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
         in
@@ -776,7 +778,7 @@ let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
       let a' = infos.info in
       let new_info =
         { infos with
-          info = mkCase (ci, a, iv, a', l)
+          info = mkCase (EConstr.contract_case env sigma (ci, a, iv, a', l))
         ; is_main_branch = expr_info.is_main_branch
         ; is_final = expr_info.is_final }
       in
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4a2c298caa..90c366ed63 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -774,7 +774,7 @@ let rec find_a_destructable_match sigma t =
   let cl = [cl, (None, None), None], None in
   let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in
   match EConstr.kind sigma t with
-    | Case (_,_,_,x,_) when closed0 sigma x ->
+    | Case (_,_,_,_,_,x,_) when closed0 sigma x ->
         if isVar sigma x then
           (* TODO check there is no rel n. *)
           raise (Found (Tacinterp.eval_tactic dest))
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 59533eb3e3..6d0e0c36b3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -918,7 +918,8 @@ let reset_env env =
     Environ.push_rel_context (Environ.rel_context env) env'
 
 let fold_match ?(force=false) env sigma c =
-  let (ci, p, iv, c, brs) = destCase sigma c in
+  let case = destCase sigma c in
+  let (ci, p, iv, c, brs) = EConstr.expand_case env sigma case in
   let cty = Retyping.get_type_of env sigma c in
   let dep, pred, exists, sk =
     let env', ctx, body =
@@ -986,7 +987,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
                     let argty = Retyping.get_type_of env (goalevars evars) arg in
                     let state, res = s.strategy { state ; env ;
                                                   unfresh ;
-                                                  term1 = arg ;	ty1 = argty ;
+                                                  term1 = arg ;        ty1 = argty ;
                                                   cstr = (prop,None) ;
                                                   evars } in
                     let res' =
@@ -1153,7 +1154,8 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
           | Fail | Identity -> b'
         in state, res
 
-      | Case (ci, p, iv, c, brs) ->
+      | Case (ci, u, pms, p, iv, c, brs) ->
+        let (ci, p, iv, c, brs) = EConstr.expand_case env (goalevars evars) (ci, u, pms, p, iv, c, brs) in
         let cty = Retyping.get_type_of env (goalevars evars) c in
         let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
         let cstr' = Some eqty in
@@ -1163,7 +1165,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
         let state, res =
           match c' with
           | Success r ->
-            let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in
+            let case = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs)) in
             let res = make_leibniz_proof env case ty r in
               state, Success (coerce env (prop,cstr) res)
           | Fail | Identity ->
@@ -1185,7 +1187,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
               in
                 match found with
                 | Some r ->
-                  let ctxc = mkCase (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c'))) in
+                  let ctxc = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c')))) in
                     state, Success (make_leibniz_proof env ctxc ty r)
                 | None -> state, c'
             else
@@ -1386,7 +1388,7 @@ module Strategies =
 
     let fold_glob c : 'a pure_strategy = { strategy =
       fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
-(* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
+(*         let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
         let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
         let unfolded =
           try Tacred.try_red_product env sigma c
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 2a21049c6e..7774258fca 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -285,7 +285,8 @@ let iter_constr_LR f c = match kind c with
   | Prod (_, t, b) | Lambda (_, t, b)  -> f t; f b
   | LetIn (_, v, t, b) -> f v; f t; f b
   | App (cf, a) -> f cf; Array.iter f a
-  | Case (_, p, iv, v, b) -> f v; iter_invert f iv; f p; Array.iter f b
+  | Case (_, _, pms, (_, p), iv, v, b) ->
+    f v; Array.iter f pms; f p; iter_invert f iv; Array.iter (fun (_, c) -> f c) b
   | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
     for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
   | Proj(_,a) -> f a
@@ -749,7 +750,7 @@ let rec uniquize = function
         EConstr.push_rel ctx_item env, h' + 1 in
       let self acc c = EConstr.of_constr (subst_loop acc (EConstr.Unsafe.to_constr c)) in
       let f = EConstr.of_constr f in
-      let f' = map_constr_with_binders_left_to_right sigma inc_h self acc f in
+      let f' = map_constr_with_binders_left_to_right env sigma inc_h self acc f in
       let f' = EConstr.Unsafe.to_constr f' in
       mkApp (f', Array.map_left (subst_loop acc) a) in
   subst_loop (env,h) c) : find_P),
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d2859b1b4e..6370bd4f9a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1165,17 +1165,16 @@ let rec ungeneralize sigma n ng body =
   | LetIn (na,b,t,c) ->
       (* We traverse an alias *)
       mkLetIn (na,b,t,ungeneralize sigma (n+1) ng c)
-  | Case (ci,p,iv,c,brs) ->
+  | Case (ci,u,pms,p,iv,c,brs) ->
       (* We traverse a split *)
       let p =
-        let sign,p = decompose_lam_assum sigma p in
+        let (nas, p) = p in
         let sign2,p = decompose_prod_n_assum sigma ng p in
-        let p = prod_applist sigma p [mkRel (n+List.length sign+ng)] in
-        it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in
-      mkCase (ci,p,iv,c,Array.map2 (fun q c ->
-        let sign,b = decompose_lam_n_decls sigma q c in
-        it_mkLambda_or_LetIn (ungeneralize sigma (n+q) ng b) sign)
-        ci.ci_cstr_ndecls brs)
+        let p = prod_applist sigma p [mkRel (n+Array.length nas+ng)] in
+        nas, it_mkProd_or_LetIn p sign2
+      in
+      let map (nas, br) = nas, ungeneralize sigma (n + Array.length nas) ng br in
+      mkCase (ci, u, pms, p, iv, c, Array.map map brs)
   | App (f,args) ->
       (* We traverse an inner generalization *)
       assert (isCase sigma f);
@@ -1195,12 +1194,9 @@ let rec is_dependent_generalization sigma ng body =
   | LetIn (na,b,t,c) ->
       (* We traverse an alias *)
       is_dependent_generalization sigma ng c
-  | Case (ci,p,iv,c,brs) ->
+  | Case (ci,u,pms,p,iv,c,brs) ->
       (* We traverse a split *)
-      Array.exists2 (fun q c ->
-        let _,b = decompose_lam_n_decls sigma q c in
-        is_dependent_generalization sigma ng b)
-        ci.ci_cstr_ndecls brs
+      Array.exists (fun (_, b) -> is_dependent_generalization sigma ng b) brs
   | App (g,args) ->
       (* We traverse an inner generalization *)
       assert (isCase sigma g);
@@ -1759,7 +1755,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
     let good = List.filter (fun (_,u,_) -> is_conv_leq !!env sigma t u) subst in
     match good with
     | [] ->
-      map_constr_with_full_binders sigma (push_binder sigma) aux x t
+      map_constr_with_full_binders !!env sigma (push_binder sigma) aux x t
     | (_, _, u) :: _ -> (* u is in extenv *)
       let vl = List.map pi1 good in
       let ty =
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index bada2c3a60..7930c3d634 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -76,8 +76,7 @@ type cbv_value =
 and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
-  | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert
-            * case_info * cbv_value subs * cbv_stack
+  | CASE of Univ.Instance.t * constr array * case_return * case_branch array * Constr.case_invert * case_info * cbv_value subs * cbv_stack
   | PROJ of Projection.t * cbv_stack
 
 (* les vars pourraient etre des constr,
@@ -143,7 +142,7 @@ let rec stack_concat stk1 stk2 =
   match stk1 with
       TOP -> stk2
     | APP(v,stk1') -> APP(v,stack_concat stk1' stk2)
-    | CASE(c,b,iv,i,s,stk1') -> CASE(c,b,iv,i,s,stack_concat stk1' stk2)
+    | CASE(u,pms,c,b,iv,i,s,stk1') -> CASE(u,pms,c,b,iv,i,s,stack_concat stk1' stk2)
     | PROJ (p,stk1') -> PROJ (p,stack_concat stk1' stk2)
 
 (* merge stacks when there is no shifts in between *)
@@ -357,9 +356,9 @@ let rec reify_stack t = function
   | TOP -> t
   | APP (args,st) ->
       reify_stack (mkApp(t,Array.map reify_value args)) st
-  | CASE (ty,br,iv,ci,env,st) ->
+  | CASE (u,pms,ty,br,iv,ci,env,st) ->
       reify_stack
-        (mkCase (ci, ty, iv, t, br))
+        (mkCase (ci, u, pms, ty, iv, t,br))
         st
   | PROJ (p, st) ->
        reify_stack (mkProj (p, t)) st
@@ -410,6 +409,29 @@ let rec subs_consn v i n s =
   if Int.equal i n then s
   else subs_consn v (i + 1) n (subs_cons v.(i) s)
 
+(* TODO: share the common parts with EConstr *)
+let expand_branch env u pms (ind, i) br =
+  let open Declarations in
+  let nas, _br = br.(i - 1) in
+  let (mib, mip) = Inductive.lookup_mind_specif env ind in
+  let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list pms) in
+  let subst = paramsubst @ Inductive.ind_subst (fst ind) mib u in
+  let (ctx, _) = mip.mind_nf_lc.(i - 1) in
+  let (ctx, _) = List.chop mip.mind_consnrealdecls.(i - 1) ctx in
+  Inductive.instantiate_context u subst nas ctx
+
+let cbv_subst_of_rel_context_instance mkclos sign args env =
+  let rec aux subst sign l =
+    let open Context.Rel.Declaration in
+    match sign, l with
+    | LocalAssum _ :: sign', a::args' -> aux (subs_cons a subst) sign' args'
+    | LocalDef (_,c,_)::sign', args' ->
+        aux (subs_cons (mkclos subst c) subst) sign' args'
+    | [], [] -> subst
+    | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.")
+  in aux env (List.rev sign) (Array.to_list args)
+
 (* The main recursive functions
  *
  * Go under applications and cases/projections (pushed in the stack),
@@ -429,7 +451,7 @@ let rec norm_head info env t stack =
                         they could be computed when getting out of the stack *)
       let nargs = Array.map (cbv_stack_term info TOP env) args in
       norm_head info env head (stack_app nargs stack)
-  | Case (ci,p,iv,c,v) -> norm_head info env c (CASE(p,v,iv,ci,env,stack))
+  | Case (ci,u,pms,p,iv,c,v) -> norm_head info env c (CASE(u,pms,p,v,iv,ci,env,stack))
   | Cast (ct,_,_) -> norm_head info env ct stack
 
   | Proj (p, c) ->
@@ -557,16 +579,33 @@ and cbv_stack_value info env = function
         cbv_stack_term info stk envf redfix
 
     (* constructor in a Case -> IOTA *)
-    | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,iv,ci,env,stk)))
+    | (CONSTR(((sp,n),_),[||]), APP(args,CASE(u,pms,_p,br,iv,ci,env,stk)))
             when red_set info.reds fMATCH ->
+        let nargs = Array.length args - ci.ci_npar in
         let cargs =
-          Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
-        cbv_stack_term info (stack_app cargs stk) env br.(n-1)
+          Array.sub args ci.ci_npar nargs in
+        let env =
+          if (Int.equal ci.ci_cstr_ndecls.(n - 1) ci.ci_cstr_nargs.(n - 1)) then (* no lets *)
+            subs_consn cargs 0 nargs env
+          else
+            let mkclos env c = cbv_stack_term info TOP env c in
+            let ctx = expand_branch info.env u pms (sp, n) br in
+            cbv_subst_of_rel_context_instance mkclos ctx cargs env
+        in
+        cbv_stack_term info stk env (snd br.(n-1))
 
     (* constructor of arity 0 in a Case -> IOTA *)
-    | (CONSTR(((_,n),u),[||]), CASE(_,br,_,_,env,stk))
+    | (CONSTR(((sp, n), _),[||]), CASE(u,pms,_,br,_,ci,env,stk))
             when red_set info.reds fMATCH ->
-                    cbv_stack_term info stk env br.(n-1)
+        let env =
+          if (Int.equal ci.ci_cstr_ndecls.(n - 1) ci.ci_cstr_nargs.(n - 1)) then (* no lets *)
+            env
+          else
+            let mkclos env c = cbv_stack_term info TOP env c in
+            let ctx = expand_branch info.env u pms (sp, n) br in
+            cbv_subst_of_rel_context_instance mkclos ctx [||] env
+        in
+        cbv_stack_term info stk env (snd br.(n-1))
 
     (* constructor in a Projection -> IOTA *)
     | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk)))
@@ -640,10 +679,31 @@ let rec apply_stack info t = function
   | TOP -> t
   | APP (args,st) ->
       apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st
-  | CASE (ty,br,iv,ci,env,st) ->
+  | CASE (u,pms,ty,br,iv,ci,env,st) ->
+    (* FIXME: Prevent this expansion by caching whether an inductive contains let-bindings *)
+    let (_, ty, _, _, br) = Inductive.expand_case info.env (ci, u, pms, ty, iv, mkProp, br) in
+    let ty =
+      let (_, mip) = Inductive.lookup_mind_specif info.env ci.ci_ind in
+      Term.decompose_lam_n_decls (mip.Declarations.mind_nrealdecls + 1) ty
+    in
+    let mk_br c n = Term.decompose_lam_n_decls n c in
+    let br = Array.map2 mk_br br ci.ci_cstr_ndecls in
+    let map_ctx (nas, c) =
+      let open Context.Rel.Declaration in
+      let fold decl e = match decl with
+      | LocalAssum _ -> subs_lift e
+      | LocalDef (_, b, _) ->
+        let b = cbv_stack_term info TOP e b in
+        (* The let-binding persists, so we have to shift *)
+        subs_shft (1, subs_cons b e)
+      in
+      let env = List.fold_right fold nas env in
+      let nas = Array.of_list (List.rev_map get_annot nas) in
+      (nas, cbv_norm_term info env c)
+    in
       apply_stack info
-        (mkCase (ci, cbv_norm_term info env ty, iv, t,
-                    Array.map (cbv_norm_term info env) br))
+        (mkCase (ci, u, Array.map (cbv_norm_term info env) pms, map_ctx ty, iv, t,
+                    Array.map map_ctx br))
         st
   | PROJ (p, st) ->
        apply_stack info (mkProj (p, t)) st
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 409f4c0f70..4d81678200 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -42,8 +42,7 @@ type cbv_value =
 and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
-  | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert
-            * case_info * cbv_value subs * cbv_stack
+  | CASE of Univ.Instance.t * constr array * case_return * case_branch array * Constr.case_invert * case_info * cbv_value subs * cbv_stack
   | PROJ of Projection.t * cbv_stack
 
 val shift_value : int -> cbv_value -> cbv_value
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 0e69b814c7..c77feeafbb 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -351,7 +351,9 @@ let matches_core env sigma allow_bound_rels
           sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
-      | PIf (a1,b1,b1'), Case (ci,_,_,a2,[|b2;b2'|]) ->
+      | PIf (a1,b1,b1'), Case (ci, u2, pms2, p2, iv, a2, ([|b2;b2'|] as br2)) ->
+          let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in
+          let b2, b2' = match br2 with [|b2; b2'|] -> b2, b2' | _ -> assert false in
           let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in
           let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in
           let n = Context.Rel.length ctx_b2 in
@@ -367,7 +369,8 @@ let matches_core env sigma allow_bound_rels
           else
             raise PatternMatchingFailure
 
-      | PCase (ci1,p1,a1,br1), Case (ci2,p2,_,a2,br2) ->
+      | PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) ->
+          let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
           let n2 = Array.length br2 in
           let () = match ci1.cip_ind with
           | None -> ()
@@ -504,12 +507,30 @@ let sub_match ?(closed=true) env sigma pat c =
        | [app';c] -> mk_ctx (mkApp (app',[|c|]))
        | _ -> assert false in
      try_aux [(env, app); (env, Array.last lc)] mk_ctx next
-  | Case (ci,hd,iv,c1,lc) ->
+  | Case (ci,u,pms,hd0,iv,c1,lc0) ->
+      let (mib, mip) = Inductive.lookup_mind_specif env ci.ci_ind in
+      let (_, hd, _, _, br) = expand_case env sigma (ci, u, pms, hd0, iv, c1, lc0) in
+      let hd =
+        let (ctx, hd) = decompose_lam_assum sigma hd in
+        (push_rel_context ctx env, hd)
+      in
+      let map i br =
+        let decls = mip.Declarations.mind_consnrealdecls.(i) in
+        let (ctx, c) = decompose_lam_n_decls sigma decls br in
+        (push_rel_context ctx env, c)
+      in
+      let lc = Array.to_list (Array.mapi map br) in
       let next_mk_ctx = function
-      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,iv,c1,Array.of_list lc))
+      | c1 :: rem ->
+        let pms, rem = List.chop (Array.length pms) rem in
+        let pms = Array.of_list pms in
+        let hd, lc = match rem with [] -> assert false | x :: l -> (x, l) in
+        let hd = (fst hd0, hd) in
+        let map_br (nas, _) br = (nas, br) in
+        mk_ctx (mkCase (ci,u,pms,hd,iv,c1,Array.map2 map_br lc0 (Array.of_list lc)))
       | _ -> assert false
       in
-      let sub = (env, c1) :: (env, hd) :: subargs env lc in
+      let sub = (env, c1) :: Array.fold_right (fun c accu -> (env, c) :: accu) pms (hd :: lc) in
       try_aux sub next_mk_ctx next
   | Fix (indx,(names,types,bodies as recdefs)) ->
     let nb_fix = Array.length types in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 402a6f6ed3..27b193f144 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -241,16 +241,9 @@ let print_primproj_params =
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)
 
-let computable sigma p k =
+let computable sigma (nas, ccl) =
     (* We first remove as many lambda as the arity, then we look
-       if it remains a lambda for a dependent elimination. This function
-       works for normal eta-expanded term. For non eta-expanded or
-       non-normal terms, it may affirm the pred is synthetisable
-       because of an undetected ultimate dependent variable in the second
-       clause, or else, it may affirm the pred non synthetisable
-       because of a non normal term in the fourth clause.
-       A solution could be to store, in the MutCase, the eta-expanded
-       normal form of pred to decide if it depends on its variables
+       if it remains a lambda for a dependent elimination.
 
        Lorsque le prédicat est dépendant de manière certaine, on
        ne déclare pas le prédicat synthétisable (même si la
@@ -258,10 +251,7 @@ let computable sigma p k =
        sinon on perd la réciprocité de la synthèse (qui, lui,
        engendrera un prédicat non dépendant) *)
 
-  let sign,ccl = decompose_lam_assum sigma p in
-  Int.equal (Context.Rel.length sign) (k + 1)
-  &&
-  noccur_between sigma 1 (k+1) ccl
+  noccur_between sigma 1 (Array.length nas) ccl
 
 let lookup_name_as_displayed env sigma t s =
   let rec lookup avoid n c = match EConstr.kind sigma c with
@@ -429,11 +419,12 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
   | [] -> [Id.Set.empty,[],rhs]
   | na::nal ->
     match EConstr.kind sigma c with
-    | Case (ci,p,iv,c,cl) when
+    | Case (ci,u,pms,p,iv,c,cl) when
         eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e))))
         && not (Int.equal (Array.length cl) 0)
         && (* don't contract if p dependent *)
-        computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
+        computable sigma p (* FIXME: can do better *) ->
+        let (ci, _, _, _, cl) = EConstr.expand_case (snd (snd e)) sigma (ci, u, pms, p, iv, c, cl) in
         let clauses = build_tree na isgoal e sigma ci cl in
         List.flatten
           (List.map (fun (ids,pat,rhs) ->
@@ -788,8 +779,9 @@ and detype_r d flags avoid env sigma t =
         GRef (GlobRef.IndRef ind_sp, detype_instance sigma u)
     | Construct (cstr_sp,u) ->
         GRef (GlobRef.ConstructRef cstr_sp, detype_instance sigma u)
-    | Case (ci,p,iv,c,bl) ->
-        let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
+    | Case (ci,u,pms,p,iv,c,bl) ->
+        let comp = computable sigma p in
+        let (ci, p, iv, c, bl) = EConstr.expand_case (snd env) sigma (ci, u, pms, p, iv, c, bl) in
         detype_case comp (detype d flags avoid env sigma)
           (detype_eqns d flags avoid env sigma ci comp)
           (is_nondep_branch sigma) avoid
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4b0974ae03..990e84e5a7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -206,7 +206,7 @@ let occur_rigidly flags env evd (evk,_) t =
       if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true
       else Reducible
     | Rel _ | Var _ -> Reducible
-    | Case (_,_,_,c,_) ->
+    | Case (_,_,_,_,_,c,_) ->
       (match aux c with
       | Rigid b -> Rigid b
       | _ -> Reducible)
@@ -381,7 +381,10 @@ let rec ise_stack2 no_app env evd f sk1 sk2 =
       else None, x in
     match revsk1, revsk2 with
     | [], [] -> None, Success i
-    | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
+    | Stack.Case (ci1,u1,pms1,t1,iv1,c1)::q1, Stack.Case (ci2,u2,pms2,t2,iv2,c2)::q2 ->
+      let dummy = mkProp in
+      let (_, t1, _, _, c1) = EConstr.expand_case env evd (ci1,u1,pms1,t1,iv1,dummy,c1) in
+      let (_, t2, _, _, c2) = EConstr.expand_case env evd (ci2,u2,pms2,t2,iv2,dummy,c2) in
       begin
         match ise_and i [
           (fun i -> f env i CONV t1 t2);
@@ -418,7 +421,10 @@ let rec exact_ise_stack2 env evd f sk1 sk2 =
   let rec ise_rev_stack2 i revsk1 revsk2 =
     match revsk1, revsk2 with
     | [], [] -> Success i
-    | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
+    | Stack.Case (ci1,u1,pms1,t1,iv1,c1)::q1, Stack.Case (ci2,u2,pms2,t2,iv2,c2)::q2 ->
+      let dummy = mkProp in
+      let (_, t1, _, _, c1) = EConstr.expand_case env evd (ci1,u1,pms1,t1,iv1,dummy,c1) in
+      let (_, t2, _, _, c2) = EConstr.expand_case env evd (ci2,u2,pms2,t2,iv2,dummy,c2) in
       ise_and i [
       (fun i -> ise_rev_stack2 i q1 q2);
       (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);
@@ -1278,7 +1284,7 @@ let apply_on_subterm env evd fixed f test c t =
     if occur_evars !evdref !fixedref t then
       match EConstr.kind !evdref t with
       | Evar (ev, args) when Evar.Set.mem ev !fixedref -> t
-      | _ -> map_constr_with_binders_left_to_right !evdref
+      | _ -> map_constr_with_binders_left_to_right env !evdref
               (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
               applyrec acc t
     else
@@ -1293,7 +1299,7 @@ let apply_on_subterm env evd fixed f test c t =
                 evdref := evd'; t')
      else (
        if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed");
-       map_constr_with_binders_left_to_right !evdref
+       map_constr_with_binders_left_to_right env !evdref
         (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
         applyrec acc t))
   in
@@ -1383,7 +1389,7 @@ let thin_evars env sigma sign c =
        if not (Id.Set.mem id ctx) then raise (TypingFailed !sigma)
        else t
     | _ ->
-       map_constr_with_binders_left_to_right !sigma
+       map_constr_with_binders_left_to_right env !sigma
         (fun d (env,acc) -> (push_rel d env, acc+1))
         applyrec (env,acc) t
   in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f9f6f74a66..cb3eef9df0 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -232,7 +232,7 @@ let recheck_applications unify flags env evdref t =
        else ()
      in aux 0 fty
     | _ ->
-       iter_with_full_binders !evdref (fun d env -> push_rel d env) aux env t
+       iter_with_full_binders env !evdref (fun d env -> push_rel d env) aux env t
   in aux env t
 
 
@@ -304,7 +304,7 @@ let noccur_evar env evd evk c =
         | LocalAssum _ -> ()
         | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (EConstr.of_constr b)))
   | Proj (p,c) -> occur_rec true acc c
-  | _ -> iter_with_full_binders evd (fun rd (k,env) -> (succ k, push_rel rd env))
+  | _ -> iter_with_full_binders env evd (fun rd (k,env) -> (succ k, push_rel rd env))
     (occur_rec check_types) acc c
   in
   try occur_rec false (0,env) c; true with Occur -> false
@@ -490,14 +490,14 @@ let expansion_of_var sigma aliases x =
   | Some a, _ -> (true, Alias.repr sigma a)
   | None, a :: _ -> (true, Some a)
 
-let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t with
+let rec expand_vars_in_term_using env sigma aliases t = match EConstr.kind sigma t with
   | Rel n -> of_alias (normalize_alias sigma aliases (RelAlias n))
   | Var id -> of_alias (normalize_alias sigma aliases (VarAlias id))
   | _ ->
-    let self aliases c = expand_vars_in_term_using sigma aliases c in
-    map_constr_with_full_binders sigma (extend_alias sigma) self aliases t
+    let self aliases c = expand_vars_in_term_using env sigma aliases c in
+    map_constr_with_full_binders env sigma (extend_alias sigma) self aliases t
 
-let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env sigma)
+let expand_vars_in_term env sigma = expand_vars_in_term_using env sigma (make_alias_map env sigma)
 
 let free_vars_and_rels_up_alias_expansion env sigma aliases c =
   let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
@@ -533,7 +533,7 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c =
     | Const _ | Ind _ | Construct _ ->
         acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2
     | _ ->
-        iter_with_full_binders sigma
+        iter_with_full_binders env sigma
           (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
           frec (aliases,depth) c
   in
@@ -1645,7 +1645,7 @@ let rec invert_definition unify flags choose imitate_defs
             let candidates =
               try
                 let t =
-                  map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+                  map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1)
                     imitate envk t in
                 (* Less dependent solutions come last *)
                 l@[t]
@@ -1659,7 +1659,7 @@ let rec invert_definition unify flags choose imitate_defs
               evar'')
         | None ->
            (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
-          map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+          map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1)
                                         imitate envk t
   in
   let rhs = whd_beta env evd rhs (* heuristic *) in
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 52e3364109..9f84b7683f 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -73,7 +73,7 @@ type 'a testing_function = {
    (b,l), b=true means no occurrence except the ones in l and b=false,
    means all occurrences except the ones in l *)
 
-let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
+let replace_term_occ_gen_modulo env sigma occs like_first test bywhat cl occ t =
   let count = ref (Locusops.initialize_occurrence_counter occs) in
   let nested = ref false in
   let add_subst pos t subst =
@@ -107,23 +107,23 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
     with NotUnifiable _ ->
       subst_below k t
   and subst_below k t =
-    map_constr_with_binders_left_to_right sigma (fun d k -> k+1) substrec k t
+    map_constr_with_binders_left_to_right env sigma (fun d k -> k+1) substrec k t
   in
   let t' = substrec 0 t in
   (!count, t')
 
-let replace_term_occ_modulo evd occs test bywhat t =
+let replace_term_occ_modulo env evd occs test bywhat t =
   let occs',like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
   proceed_with_occurrences
-    (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t
+    (replace_term_occ_gen_modulo env evd occs' like_first test bywhat None) occs' t
 
-let replace_term_occ_decl_modulo evd occs test bywhat d =
+let replace_term_occ_decl_modulo env evd occs test bywhat d =
   let (plocs,hyploc),like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (replace_term_occ_gen_modulo evd plocs like_first test bywhat)
+       (replace_term_occ_gen_modulo env evd plocs like_first test bywhat)
        hyploc)
     plocs d
 
@@ -145,7 +145,7 @@ let make_eq_univs_test env evd c =
 let subst_closed_term_occ env evd occs c t =
   let test = make_eq_univs_test env evd c in
   let bywhat () = mkRel 1 in
-  let t' = replace_term_occ_modulo evd occs test bywhat t in
+  let t' = replace_term_occ_modulo env evd occs test bywhat t in
     t', test.testing_state
 
 let subst_closed_term_occ_decl env evd occs c d =
@@ -155,6 +155,6 @@ let subst_closed_term_occ_decl env evd occs c d =
   let bywhat () = mkRel 1 in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (fun _ -> replace_term_occ_gen_modulo evd plocs like_first test bywhat None)
+       (fun _ -> replace_term_occ_gen_modulo env evd plocs like_first test bywhat None)
        hyploc) plocs d,
   test.testing_state
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 1ddae01e2b..c71cb207ab 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -43,13 +43,13 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
     matching subterms at the indicated occurrences [occl] with [mk
     ()]; it turns a NotUnifiable exception raised by the testing
     function into a SubtermUnificationError. *)
-val replace_term_occ_modulo : evar_map -> occurrences or_like_first ->
+val replace_term_occ_modulo : env -> evar_map -> occurrences or_like_first ->
   'a testing_function -> (unit -> constr) -> constr -> constr
 
 (** [replace_term_occ_decl_modulo] is similar to
     [replace_term_occ_modulo] but for a named_declaration. *)
 val replace_term_occ_decl_modulo :
-  evar_map ->
+  env -> evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
   'a testing_function -> (unit -> constr) ->
   named_declaration -> named_declaration
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index a012f1cb15..f6e45613e1 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -76,7 +76,7 @@ and kind_of_head env t =
   | App (c,al) -> aux k (Array.to_list al @ l) c b
   | Proj (p,c) -> RigidHead RigidOther
 
-  | Case (_,_,_,c,_) -> aux k [] c true
+  | Case (_,_,_,_,_,c,_) -> aux k [] c true
   | Int _ | Float _ | Array _ -> ConstructorHead
   | Fix ((i,j),_) ->
       let n = i.(j) in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 5ffd919312..dd7cf8abaa 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -122,12 +122,24 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
         | None ->
           let iv = make_case_invert env (find_rectype env sigma (EConstr.of_constr (lift 1 depind))) ci in
           let iv = EConstr.Unsafe.to_case_invert iv in
-          mkCase (ci, lift ndepar p, iv, mkRel 1, Termops.rel_vect ndepar k)
+          let ncons = Array.length mip.mind_consnames in
+          let mk_branch i =
+            (* eta-expansion to please branch contraction *)
+            let ft = get_type (lookup_rel (ncons - i) env) in
+            (* we need that to get the generated names for the branch *)
+            let (ctx, _) = decompose_prod_assum ft in
+            let n = mkRel (List.length ctx + 1) in
+            let args = Context.Rel.to_extended_vect mkRel 0 ctx in
+            let br = it_mkLambda_or_LetIn (mkApp (n, args)) ctx in
+            lift (ndepar + ncons - i - 1) br
+          in
+          let br = Array.init ncons mk_branch in
+          mkCase (Inductive.contract_case env (ci, lift ndepar p,  iv, mkRel 1, br))
         | Some ps ->
           let term =
             mkApp (mkRel 2,
-                   Array.map
-                   (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
+                    Array.map
+                    (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
             if dep then
               let ty = mkApp (mkRel 3, [| mkRel 1 |]) in
                 mkCast (term, DEFAULTcast, ty)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index bd875cf68b..04feae35d8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -356,8 +356,7 @@ let make_case_or_project env sigma indt ci pred c branches =
   let IndType (((ind,_),_),_) = indt in
   let projs = get_projections env ind in
   match projs with
-  | None ->
-    mkCase (ci, pred, make_case_invert env indt ci, c, branches)
+  | None -> (mkCase (EConstr.contract_case env sigma (ci, pred, make_case_invert env indt ci, c, branches)))
   | Some ps ->
      assert(Array.length branches == 1);
      let na, ty, t = destLambda sigma pred in
@@ -749,6 +748,6 @@ let control_only_guard env sigma c =
   in
   let rec iter env c =
     check_fix_cofix env c;
-    EConstr.iter_with_full_binders sigma EConstr.push_rel iter env c
+    EConstr.iter_with_full_binders env sigma EConstr.push_rel iter env c
   in
   iter env c
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 3705d39280..8e83814fa0 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -213,7 +213,7 @@ val make_case_or_project :
   (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
 
 val make_case_invert : env -> inductive_type -> case_info
-  -> (EConstr.constr,EConstr.EInstance.t) case_invert
+  -> EConstr.case_invert
 
 (*i Compatibility
 val make_default_case_info : env -> case_style -> inductive -> case_info
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index d06d6e01d1..8da615acfc 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -343,7 +343,8 @@ and nf_atom_type env sigma atom =
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type p realargs a in
-      mkCase(ans.asw_ci, p, iv, a, branchs), tcase
+      let ci = ans.asw_ci in
+      mkCase (Inductive.contract_case env (ci, p, iv, a, branchs)), tcase
   | Afix(tt,ft,rp,s) ->
       let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in
       let tt = Array.map fst tt and rt = Array.map snd tt in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b259945d9e..47097a0e32 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -202,7 +202,8 @@ let pattern_of_constr env sigma t =
       | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
       | _ ->
         PMeta None)
-    | Case (ci,p,_,a,br) ->
+    | Case (ci, u, pms, p, iv, a, br) ->
+        let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p, iv, a, br) in
         let cip =
           { cip_style = ci.ci_pp_info.style;
             cip_ind = Some ci.ci_ind;
@@ -213,7 +214,7 @@ let pattern_of_constr env sigma t =
           (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c)
         in
         PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
-               Array.to_list (Array.mapi branch_of_constr br))
+                Array.to_list (Array.mapi branch_of_constr br))
     | Fix (lni,(lna,tl,bl)) ->
        let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
        let env' = Array.fold_left2 push env lna tl in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9dbded75ba..e86a8a28c9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1043,7 +1043,7 @@ struct
       if not record then
         let f = it_mkLambda_or_LetIn f fsign in
         let ci = make_case_info !!env (ind_of_ind_type indt) rci LetStyle in
-          mkCase (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|])
+          mkCase (EConstr.contract_case !!env sigma (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|]))
       else it_mkLambda_or_LetIn f fsign
     in
     (* Make dependencies from arity signature impossible *)
@@ -1159,7 +1159,7 @@ struct
         let pred = nf_evar sigma pred in
         let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val pred in
         let ci = make_case_info !!env (fst ind) rci IfStyle in
-          mkCase (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|])
+        mkCase (EConstr.contract_case !!env sigma (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|]))
       in
       let cj = { uj_val = v; uj_type = p } in
       discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 52f60fbc5e..85214eb245 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -177,9 +177,12 @@ sig
   type 'a app_node
   val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
+  type 'a case_stk =
+    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
+  | Case of 'a case_stk
   | Proj of Projection.t
   | Fix of ('a, 'a) pfixpoint * 'a t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
@@ -230,9 +233,12 @@ struct
                      )
 
 
+  type 'a case_stk =
+    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
+  | Case of 'a case_stk
   | Proj of Projection.t
   | Fix of ('a, 'a) pfixpoint * 'a t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
@@ -245,9 +251,9 @@ struct
     let pr_c x = hov 1 (pr_c x) in
     match member with
     | App app -> str "ZApp" ++ pr_app_node pr_c app
-    | Case (_,_,_,br) ->
+    | Case (_,_,_,_,_,br) ->
        str "ZCase(" ++
-         prvect_with_sep (pr_bar) pr_c br
+         prvect_with_sep (pr_bar) (fun (_, c) -> pr_c c) br
        ++ str ")"
     | Proj p  ->
       str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
@@ -284,7 +290,7 @@ struct
         ([],[]) -> Int.equal bal 0
       | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2
       | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2
-      | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) ->
+      | (Case _ :: s1, Case _::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
       | (Proj (p)::s1, Proj(p2)::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
@@ -304,8 +310,9 @@ struct
         let t1,l1 = decomp_node_last n1 q1 in
         let t2,l2 = decomp_node_last n2 q2 in
         aux (f o t1 t2) l1 l2
-      | Case (_,t1,_,a1) :: q1, Case (_,t2,_,a2) :: q2 ->
-        aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2
+      | Case ((_,_,pms1,(_, t1),_,a1)) :: q1, Case ((_,_,pms2, (_, t2),_,a2)) :: q2 ->
+        let f' o (_, t1) (_, t2) = f o t1 t2 in
+        aux (Array.fold_left2 f' (f (Array.fold_left2 f o pms1 pms2) t1 t2) a1 a2) q1 q2
       | Proj (p1) :: q1, Proj (p2) :: q2 ->
         aux o q1 q2
       | Fix ((_,(_,a1,b1)),s1) :: q1, Fix ((_,(_,a2,b2)),s2) :: q2 ->
@@ -320,8 +327,8 @@ struct
                                | App (i,a,j) ->
                                   let le = j - i + 1 in
                                   App (0,Array.map f (Array.sub a i le), le-1)
-                               | Case (info,ty,iv,br) ->
-                                 Case (info, f ty, map_invert f iv, Array.map f br)
+                               | Case (info,u,pms,ty,iv,br) ->
+                                  Case (info, u, Array.map f pms, on_snd f ty, iv, Array.map (on_snd f) br)
                                | Fix ((r,(na,ty,bo)),arg) ->
                                   Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg)
                                | Primitive (p,c,args,kargs) ->
@@ -408,7 +415,7 @@ struct
                 then a
                 else Array.sub a i (j - i + 1) in
        zip (mkApp (f, a'), s)
-    | f, (Case (ci,rt,iv,br)::s) -> zip (mkCase (ci,rt,iv,f,br), s)
+    | f, (Case (ci,u,pms,rt,iv,br)::s) -> zip (mkCase (ci,u,pms,rt,iv,f,br), s)
   | f, (Fix (fix,st)::s) -> zip
     (mkFix fix, st @ (append_app [|f|] s))
   | f, (Proj (p)::s) -> zip (mkProj (p,f),s)
@@ -469,13 +476,13 @@ let strong_with_flags whdfun flags env sigma t =
       | d -> d in
     push_rel d env in
   let rec strongrec env t =
-    map_constr_with_full_binders sigma
+    map_constr_with_full_binders env sigma
       push_rel_check_zeta strongrec env (whdfun flags env sigma t) in
   strongrec env t
 
 let strong whdfun env sigma t =
   let rec strongrec env t =
-    map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in
+    map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in
   strongrec env t
 
 (*************************************)
@@ -702,6 +709,20 @@ let debug_RAKAM =
     ~key:["Debug";"RAKAM"]
     ~value:false
 
+let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
+  let args = Stack.tail ci.ci_npar args in
+  let args = Option.get (Stack.list_of_app_stack args) in
+  let br = lf.(i - 1) in
+  let subst =
+    if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then
+      (* No let-bindings *)
+      List.rev args
+    else
+      let ctx = expand_branch env sigma u pms (ind, i) br in
+      subst_of_rel_context_instance ctx args
+  in
+  Vars.substl subst (snd br)
+
 let rec whd_state_gen flags env sigma =
   let open Context.Named.Declaration in
   let rec whrec (x, stack) : state =
@@ -785,8 +806,8 @@ let rec whd_state_gen flags env sigma =
         | _ -> fold ())
       | _ -> fold ())
 
-    | Case (ci,p,iv,d,lf) ->
-      whrec (d, Stack.Case (ci,p,iv,lf) :: stack)
+    | Case (ci,u,pms,p,iv,d,lf) ->
+      whrec (d, Stack.Case (ci,u,pms,p,iv,lf) :: stack)
 
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
@@ -794,13 +815,14 @@ let rec whd_state_gen flags env sigma =
       |Some (bef,arg,s') ->
         whrec (arg, Stack.Fix(f,bef)::s'))
 
-    | Construct ((ind,c),u) ->
+    | Construct (cstr ,u) ->
       let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
       let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(ci, _, _, lf)::s') when use_match ->
-          whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+        |args, (Stack.Case case::s') when use_match ->
+          let r = apply_branch env sigma cstr args case in
+          whrec (r, s')
         |args, (Stack.Proj (p)::s') when use_match ->
           whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
         |args, (Stack.Fix (f,s')::s'') when use_fix ->
@@ -850,7 +872,7 @@ let rec whd_state_gen flags env sigma =
   whrec
 
 (** reduction machine without global env and refold machinery *)
-let local_whd_state_gen flags _env sigma =
+let local_whd_state_gen flags env sigma =
   let rec whrec (x, stack) =
     let c0 = EConstr.kind sigma x in
     let s = (EConstr.of_kind c0, stack) in
@@ -882,8 +904,8 @@ let local_whd_state_gen flags _env sigma =
     | Proj (p,c) when CClosure.RedFlags.red_projection flags p ->
       (whrec (c, Stack.Proj (p) :: stack))
 
-    | Case (ci,p,iv,d,lf) ->
-      whrec (d, Stack.Case (ci,p,iv,lf) :: stack)
+    | Case (ci,u,pms,p,iv,d,lf) ->
+      whrec (d, Stack.Case (ci,u,pms,p,iv,lf) :: stack)
 
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
@@ -896,13 +918,14 @@ let local_whd_state_gen flags _env sigma =
         Some c -> whrec (c,stack)
       | None -> s)
 
-    | Construct ((ind,c),u) ->
+    | Construct (cstr, u) ->
       let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
       let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(ci, _, _, lf)::s') when use_match ->
-          whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+        |args, (Stack.Case case :: s') when use_match ->
+          let r = apply_branch env sigma cstr args case in
+          whrec (r, s')
         |args, (Stack.Proj (p) :: s') when use_match ->
           whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
         |args, (Stack.Fix (f,s')::s'') when use_fix ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ae93eb48b4..e60def72f6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -57,9 +57,12 @@ module Stack : sig
 
   val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
+  type 'a case_stk =
+    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
+  | Case of 'a case_stk
   | Proj of Projection.t
   | Fix of ('a, 'a) pfixpoint * 'a t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 34bcd0982c..064990f6bf 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -129,7 +129,8 @@ let retype ?(polyprop=true) sigma =
     | Evar ev -> existential_type sigma ev
     | Ind (ind, u) -> EConstr.of_constr (rename_type_of_inductive env (ind, EInstance.kind sigma u))
     | Construct (cstr, u) -> EConstr.of_constr (rename_type_of_constructor env (cstr, EInstance.kind sigma u))
-    | Case (_,p,_iv,c,lf) ->
+    | Case (ci,u,pms,p,iv,c,lf) ->
+        let (_,p,iv,c,lf) = EConstr.expand_case env sigma (ci,u,pms,p,iv,c,lf) in
         let Inductiveops.IndType(indf,realargs) =
           let t = type_of env c in
           try Inductiveops.find_rectype env sigma t
@@ -309,7 +310,7 @@ let relevance_of_term env sigma c =
       | Const (c,_) -> Relevanceops.relevance_of_constant env c
       | Ind _ -> Sorts.Relevant
       | Construct (c,_) -> Relevanceops.relevance_of_constructor env c
-      | Case (ci, _, _, _, _) -> ci.ci_relevance
+      | Case (ci, _, _, _, _, _, _) -> ci.ci_relevance
       | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
       | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
       | Proj (p, _) -> Relevanceops.relevance_of_projection env p
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 411fb0cd89..01819a650b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -296,8 +296,8 @@ let compute_consteval_direct env sigma ref =
       | Fix fix when not onlyproj ->
           (try check_fix_reversibility sigma labs l fix
           with Elimconst -> NotAnElimination)
-      | Case (_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
-      | Case (_,_,_,d,_) -> srec env n labs true d
+      | Case (_,_,_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
+      | Case (_,_,_,_,_,d,_) -> srec env n labs true d
       | Proj (p, d) when isRel sigma d -> EliminationProj n
       | _ -> NotAnElimination
   in
@@ -478,29 +478,36 @@ let contract_cofix_use_function env sigma f
     sigma (nf_beta env sigma bodies.(bodynum))
 
 type 'a miota_args = {
-  mP      : constr;     (** the result type *)
+  mU      : EInstance.t; (* Universe instance of the return clause *)
+  mParams : constr array; (* Parameters of the inductive *)
+  mP      : case_return;     (* the result type *)
   mconstr : constr;     (** the constructor *)
   mci     : case_info;  (** special info to re-build pattern *)
   mcargs  : 'a list;    (** the constructor's arguments *)
-  mlf     : 'a array }  (** the branch code vector *)
+  mlf     : 'a pcase_branch array }  (** the branch code vector *)
 
-let reduce_mind_case sigma mia =
+let reduce_mind_case env sigma mia =
   match EConstr.kind sigma mia.mconstr with
-    | Construct ((ind_sp,i),u) ->
-(*      let ncargs = (fst mia.mci).(i-1) in*)
+    | Construct ((_, i as cstr), u) ->
         let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
-        applist (mia.mlf.(i-1),real_cargs)
+        let br = mia.mlf.(i - 1) in
+        let ctx = EConstr.expand_branch env sigma mia.mU mia.mParams cstr br in
+        let br = it_mkLambda_or_LetIn (snd br) ctx in
+        applist (br, real_cargs)
     | CoFix cofix ->
         let cofix_def = contract_cofix sigma cofix in
         (* XXX Is NoInvert OK here? *)
-        mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
+        mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
 let reduce_mind_case_use_function func env sigma mia =
   match EConstr.kind sigma mia.mconstr with
-    | Construct ((ind_sp,i),u) ->
+    | Construct ((_, i as cstr),u) ->
         let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
-        applist (mia.mlf.(i-1), real_cargs)
+        let br = mia.mlf.(i - 1) in
+        let ctx = EConstr.expand_branch env sigma mia.mU mia.mParams cstr br in
+        let br = it_mkLambda_or_LetIn (snd br) ctx in
+        applist (br, real_cargs)
     | CoFix (bodynum,(names,_,_) as cofix) ->
         let build_cofix_name =
           if isConst sigma func then
@@ -526,8 +533,7 @@ let reduce_mind_case_use_function func env sigma mia =
             fun _ -> None in
         let cofix_def =
           contract_cofix_use_function env sigma build_cofix_name cofix in
-        (* Is NoInvert OK here? *)
-        mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
+        mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
 
@@ -728,9 +734,9 @@ and whd_simpl_stack env sigma =
       | LetIn (n,b,t,c) -> redrec (Vars.substl [b] c, stack)
       | App (f,cl) -> assert false (* see push_app above *)
       | Cast (c,_,_) -> redrec (c, stack)
-      | Case (ci,p,iv,c,lf) ->
+      | Case (ci,u,pms,p,iv,c,lf) ->
           (try
-            redrec (special_red_case env sigma (ci,p,iv,c,lf), stack)
+            redrec (special_red_case env sigma (ci,u,pms,p,iv,c,lf), stack)
           with
               Redelimination -> s')
       | Fix fix ->
@@ -842,15 +848,15 @@ and reduce_proj env sigma c =
           let proj_narg = Projection.npars proj + Projection.arg proj in
           List.nth cargs proj_narg
         | _ -> raise Redelimination)
-    | Case (n,p,iv,c,brs) ->
+    | Case (n,u,pms,p,iv,c,brs) ->
       let c' = redrec c in
-      let p = (n,p,iv,c',brs) in
+      let p = (n,u,pms,p,iv,c',brs) in
         (try special_red_case env sigma p
          with Redelimination -> mkCase p)
     | _ -> raise Redelimination
   in redrec c
 
-and special_red_case env sigma (ci, p, iv, c, lf) =
+and special_red_case env sigma (ci, u, pms, p, iv, c, lf) =
   let rec redrec s =
     let (constr, cargs) = whd_simpl_stack env sigma s in
     match match_eval_ref env sigma constr cargs with
@@ -860,14 +866,14 @@ and special_red_case env sigma (ci, p, iv, c, lf) =
       | Some gvalue ->
         if reducible_mind_case sigma gvalue then
           reduce_mind_case_use_function constr env sigma
-          {mP=p; mconstr=gvalue; mcargs=cargs;
+          {mP=p; mU = u; mParams = pms; mconstr=gvalue; mcargs=cargs;
            mci=ci; mlf=lf}
         else
           redrec (gvalue, cargs))
     | None ->
       if reducible_mind_case sigma constr then
-        reduce_mind_case sigma
-          {mP=p; mconstr=constr; mcargs=cargs;
+        reduce_mind_case env sigma
+          {mP=p; mU = u; mParams = pms; mconstr=constr; mcargs=cargs;
           mci=ci; mlf=lf}
       else
         raise Redelimination
@@ -915,7 +921,7 @@ let try_red_product env sigma c =
           let open Context.Rel.Declaration in
           mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b)
       | LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t)
-      | Case (ci,p,iv,d,lf) -> simpfun (mkCase (ci,p,iv,redrec env d,lf))
+      | Case (ci,u,pms,p,iv,d,lf) -> simpfun (mkCase (ci,u,pms,p,iv,redrec env d,lf))
       | Proj (p, c) ->
         let c' =
           match EConstr.kind sigma c with
@@ -1062,7 +1068,7 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
       (* Still the same projection, we ignore the change in parameters *)
       mkProj (p, a')
     else mkApp (app', [| a' |])
-  | _ -> map_constr_with_binders_left_to_right sigma g f acc c
+  | _ -> map_constr_with_binders_left_to_right env sigma g f acc c
 
 let e_contextually byhead (occs,c) f = begin fun env sigma t ->
   let count = ref (Locusops.initialize_occurrence_counter occs) in
@@ -1131,7 +1137,7 @@ let substlin env sigma evalref occs c =
         count := count';
         if ok then value u else c
       | None ->
-        map_constr_with_binders_left_to_right sigma
+        map_constr_with_binders_left_to_right env sigma
           (fun _ () -> ())
           substrec () c
   in
@@ -1295,9 +1301,9 @@ let one_step_reduce env sigma c =
       | App (f,cl) -> redrec (f, (Array.to_list cl)@stack)
       | LetIn (_,f,_,cl) -> (Vars.subst1 f cl,stack)
       | Cast (c,_,_) -> redrec (c,stack)
-      | Case (ci,p,iv,c,lf) ->
+      | Case (ci,u,pms,p,iv,c,lf) ->
           (try
-             (special_red_case env sigma (ci,p,iv,c,lf), stack)
+             (special_red_case env sigma (ci,u,pms,p,iv,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
           (try match reduce_fix env sigma fix stack with
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e3e5244a8c..b0ce4fd63a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -178,7 +178,7 @@ let type_case_branches env sigma (ind,largs) pj c =
   let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
   sigma, (lc, ty, Sorts.relevance_of_sort ps)
 
-let judge_of_case env sigma ci pj iv cj lfj =
+let judge_of_case env sigma case ci pj iv cj lfj =
   let ((ind, u), spec) =
     try find_mrectype env sigma cj.uj_type
     with Not_found -> error_case_not_inductive env sigma cj in
@@ -189,7 +189,7 @@ let judge_of_case env sigma ci pj iv cj lfj =
   let () = if (match iv with | NoInvert -> false | CaseInvert _ -> true) != should_invert_case env ci
     then Type_errors.error_bad_invert env
   in
-  sigma, { uj_val  = mkCase (ci, pj.uj_val, iv, cj.uj_val, Array.map j_val lfj);
+  sigma, { uj_val  = mkCase case;
            uj_type = rslty }
 
 let check_type_fixpoint ?loc env sigma lna lar vdefj =
@@ -383,7 +383,9 @@ let rec execute env sigma cstr =
         let sigma, ty = type_of_constructor env sigma ctor in
         sigma, make_judge cstr ty
 
-    | Case (ci,p,iv,c,lf) ->
+    | Case (ci, u, pms, p, iv, c, lf) ->
+        let case = (ci, u, pms, p, iv, c, lf) in
+        let (ci, p, iv, c, lf) = EConstr.expand_case env sigma case in
         let sigma, cj = execute env sigma c in
         let sigma, pj = execute env sigma p in
         let sigma, lfj = execute_array env sigma lf in
@@ -396,7 +398,7 @@ let rec execute env sigma cstr =
             let sigma = check_actual_type env sigma cj tj.utj_val in
             sigma
         in
-        judge_of_case env sigma ci pj iv cj lfj
+        judge_of_case env sigma case ci pj iv cj lfj
 
     | Fix ((vn,i as vni),recdef) ->
         let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3d3010d1a4..a845fc3246 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -563,7 +563,7 @@ let is_rigid_head sigma flags t =
   | Construct _ | Int _ | Float _ | Array _ -> true
   | Fix _ | CoFix _ -> true
   | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _
-    | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _, _)
+    | Lambda _ | LetIn _ | App (_, _) | Case _
     | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
 
 let force_eqs c =
@@ -652,7 +652,7 @@ let rec is_neutral env sigma ts t =
       not (TransparentState.is_transparent_variable ts id)
     | Rel n -> true
     | Evar _ | Meta _ -> true
-    | Case (_, p, _, c, _) -> is_neutral env sigma ts c
+    | Case (_, _, _, _, _, c, _) -> is_neutral env sigma ts c
     | Proj (p, c) -> is_neutral env sigma ts c
     | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> false
     | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
@@ -853,7 +853,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
                unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2
              | _ -> raise ex)
 
-        | Case (ci1,p1,_,c1,cl1), Case (ci2,p2,_,c2,cl2) ->
+        | Case (ci1, u1, pms1, p1, iv1, c1, cl1), Case (ci2, u2, pms2, p2, iv2, c2, cl2) ->
+          let (ci1, p1, iv1, c1, cl1) = EConstr.expand_case env sigma (ci1, u1, pms1, p1, iv1, c1, cl1) in
+          let (ci2, p2, iv2, c2, cl2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv2, c2, cl2) in
             (try
              if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN);
              let opt' = {opt with at_top = true; with_types = false} in
@@ -1678,7 +1680,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         (push_named_context_val d sign,depdecls)
     | (AllOccurrences | AtLeastOneOccurrence), InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
-        let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in
+        let newdecl = replace_term_occ_decl_modulo env sigma occ test mkvarid d in
         if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl
            && not (indirectly_dependent sigma c d depdecls)
         then
@@ -1689,7 +1691,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
           (push_named_context_val newdecl sign, newdecl :: depdecls)
     | occ ->
         (* There are specific occurrences, hence not like first *)
-        let newdecl = replace_term_occ_decl_modulo sigma (AtOccs occ) test mkvarid d in
+        let newdecl = replace_term_occ_decl_modulo env sigma (AtOccs occ) test mkvarid d in
         (push_named_context_val newdecl sign, newdecl :: depdecls) in
   try
     let sign,depdecls =
@@ -1699,7 +1701,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       | NoOccurrences -> concl
       | occ ->
           let occ = if likefirst then LikeFirst else AtOccs occ in
-          replace_term_occ_modulo sigma occ test mkvarid concl
+          replace_term_occ_modulo env sigma occ test mkvarid concl
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in
@@ -1787,11 +1789,11 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
                  matchrec c1
                with ex when precatchable_exception ex ->
                  matchrec c2)
-          | Case(_,_,_,c,lf) -> (* does not search in the predicate *)
+          | Case(_,_,_,_,_,c,lf) -> (* does not search in the predicate *)
                (try
                  matchrec c
                with ex when precatchable_exception ex ->
-                 iter_fail matchrec lf)
+                 iter_fail matchrec (Array.map snd lf))
           | LetIn(_,c1,_,c2) ->
                (try
                  matchrec c1
@@ -1881,8 +1883,8 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
                 let c2 = args.(n-1) in
                 bind (matchrec c1) (matchrec c2)
 
-            | Case(_,_,_,c,lf) -> (* does not search in the predicate *)
-                bind (matchrec c) (bind_iter matchrec lf)
+            | Case(_,_,_,_,_,c,lf) -> (* does not search in the predicate *)
+                bind (matchrec c) (bind_iter matchrec (Array.map snd lf))
 
             | Proj (p,c) -> matchrec c
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 1420401875..314cada2d7 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -287,7 +287,7 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
           CaseInvert {univs=u; args=allargs}
         else NoInvert
       in
-      nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk
+      nf_stk env sigma (mkCase (Inductive.contract_case env (ci, p, iv, c, branchs))) tcase stk
   | Zproj p :: stk ->
      assert (from = 0) ;
      let p' = Projection.make p true in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 00ac5a0624..44d3b44077 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -268,7 +268,7 @@ let meta_reducible_instance env evd b =
   let rec irec u =
     let u = whd_betaiota env Evd.empty u (* FIXME *) in
     match EConstr.kind evd u with
-    | Case (ci,p,iv,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
+    | Case (ci,u,pms,p,iv,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
         let m = destMeta evd (strip_outer_cast evd c) in
         (match
           try
@@ -277,8 +277,10 @@ let meta_reducible_instance env evd b =
             if isConstruct evd g || not is_coerce then Some g else None
           with Not_found -> None
           with
-            | Some g -> irec (mkCase (ci,p,iv,g,bl))
-            | None -> mkCase (ci,irec p,iv,c,Array.map irec bl))
+            | Some g -> irec (mkCase (ci,u,pms,p,iv,g,bl))
+            | None ->
+              let on_ctx (na, c) = (na, irec c) in
+              mkCase (ci,u,Array.map irec pms,on_ctx p,iv,c,Array.map on_ctx bl))
     | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) ->
         let m = destMeta evd (strip_outer_cast evd f) in
         (match
@@ -627,8 +629,10 @@ let clenv_cast_meta clenv =
             else mkCast (mkMeta mv, DEFAULTcast, b)
           with Not_found -> u)
       | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
-      | Case(ci,p,iv,c,br) ->
-          mkCase (ci, crec_hd p, map_invert crec_hd iv, crec_hd c, Array.map crec br)
+      | Case(ci,u,pms,p,iv,c,br) ->
+          (* FIXME: we only change c because [p] is always a lambda and [br] is
+             most of the time??? *)
+          mkCase (ci, u, pms, p, iv, crec_hd c, br)
       | Proj (p, c) -> mkProj (p, crec_hd c)
       | _ -> u
   in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index f159395177..cb67d42bdc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -265,15 +265,12 @@ let collect_meta_variables c =
   let rec collrec deep acc c = match kind c with
     | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
     | Cast(c,_,_) -> collrec deep acc c
-    | Case(ci,p,iv,c,br) ->
-      (* Hack assuming only two situations: the legacy one that branches,
-         if with Metas, are Meta, and the new one with eta-let-expanded
-         branches *)
-      let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in
-      let acc = Constr.fold (collrec deep) acc p in
+    | Case(ci,u,pms,p,iv,c,br) ->
+      let acc = Array.fold_left (collrec deep) acc pms in
+      let acc = Constr.fold (collrec deep) acc (snd p) in
       let acc = Constr.fold_invert (collrec deep) acc iv in
       let acc = Constr.fold (collrec deep) acc c in
-      Array.fold_left (collrec deep) acc br
+      Array.fold_left (fun accu (_, br) -> collrec deep accu br) acc br
     | App _ -> Constr.fold (collrec deep) acc c
     | Proj (_, c) -> collrec deep acc c
     | _ -> Constr.fold (collrec true) acc c
@@ -369,15 +366,16 @@ let rec mk_refgoals ~check env sigma goalacc conclty trm =
         let ty = EConstr.Unsafe.to_constr ty in
           (acc',ty,sigma,c)
 
-      | Case (ci,p,iv,c,lf) ->
+      | Case (ci, u, pms, p, iv, c, lf) ->
         (* XXX Is ignoring iv OK? *)
+        let (ci, p, iv, c, lf) = Inductive.expand_case env (ci, u, pms, p, iv, c, lf) in
         let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in
         let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in
         let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
-          else mkCase (ci,p',iv,c',lf')
+          else mkCase (Inductive.contract_case env (ci,p',iv,c',lf'))
         in
         (acc'',conclty',sigma, ans)
 
@@ -418,14 +416,15 @@ and mk_hdgoals ~check env sigma goalacc trm =
         let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
         (acc'',conclty',sigma, ans)
 
-    | Case (ci,p,iv,c,lf) ->
+    | Case (ci, u, pms, p, iv, c, lf) ->
         (* XXX is ignoring iv OK? *)
+        let (ci, p, iv, c, lf) = Inductive.expand_case env (ci, u, pms, p, iv, c, lf) in
         let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in
         let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
-          else mkCase (ci,p',iv,c',lf')
+          else mkCase (Inductive.contract_case env (ci,p',iv,c',lf'))
         in
         (acc'',conclty',sigma, ans)
 
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 31873ea6b0..56bf2b056d 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -104,9 +104,11 @@ sig
     | Cst_const of pconstant
     | Cst_proj of Projection.t
 
+  type 'a case_stk =
+    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array * Cst_stack.t
+  | Case of 'a case_stk * Cst_stack.t
   | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
@@ -121,7 +123,7 @@ sig
   val append_app : 'a array -> 'a t -> 'a t
   val decomp : 'a t -> ('a * 'a t) option
   val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool)
-    -> 'a t -> 'a t -> bool
+    -> ('a case_stk -> 'a case_stk -> bool) -> 'a t -> 'a t -> bool
   val strip_app : 'a t -> 'a t * 'a t
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
   val will_expose_iota : 'a t -> bool
@@ -156,9 +158,11 @@ struct
     | Cst_const of pconstant
     | Cst_proj of Projection.t
 
+  type 'a case_stk =
+    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array * Cst_stack.t
+  | Case of 'a case_stk * Cst_stack.t
   | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
@@ -172,9 +176,9 @@ struct
     let pr_c x = hov 1 (pr_c x) in
     match member with
     | App app -> str "ZApp" ++ pr_app_node pr_c app
-    | Case (_,_,_,br,cst) ->
+    | Case ((_,_,_,_,_,br),cst) ->
        str "ZCase(" ++
-         prvect_with_sep (pr_bar) pr_c br
+         prvect_with_sep (pr_bar) (fun (_, b) -> pr_c b) br
        ++ str ")"
     | Proj (p,cst) ->
       str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
@@ -221,7 +225,7 @@ struct
     if i < j then (l.(j), App (i,l,pred j) :: sk)
     else (l.(j), sk)
 
-  let equal f f_fix sk1 sk2 =
+  let equal f f_fix f_case sk1 sk2 =
     let equal_cst_member x y =
       match x, y with
       | Cst_const (c1,u1), Cst_const (c2, u2) ->
@@ -236,8 +240,8 @@ struct
         let t1,s1' = decomp_node_last a1 s1 in
         let t2,s2' = decomp_node_last a2 s2 in
         (f t1 t2) && (equal_rec s1' s2')
-      | Case (_,t1,_,a1,_) :: s1, Case (_,t2,_,a2,_) :: s2 ->
-        f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
+      | Case ((ci1,pms1,p1,t1,iv1,a1),_) :: s1, Case ((ci2,pms2,p2,iv2,t2,a2),_) :: s2 ->
+        f_case (ci1,pms1,p1,t1,iv1,a1) (ci2,pms2,p2,iv2,t2,a2) && equal_rec s1 s2
       | (Proj (p,_)::s1, Proj(p2,_)::s2) ->
         Projection.Repr.CanOrd.equal (Projection.repr p) (Projection.repr p2)
         && equal_rec s1 s2
@@ -284,7 +288,7 @@ struct
 
   let will_expose_iota args =
     List.exists
-      (function (Fix (_,_,l) | Case (_,_,_,_,l) |
+      (function (Fix (_,_,l) | Case (_,l) |
                  Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false)
       args
 
@@ -346,9 +350,9 @@ struct
                 then a
                 else Array.sub a i (j - i + 1) in
        zip (mkApp (f, a'), s)
-    | f, (Case (ci,rt,iv,br,cst_l)::s) when refold ->
-      zip (best_state sigma (mkCase (ci,rt,iv,f,br), s) cst_l)
-    | f, (Case (ci,rt,iv,br,_)::s) -> zip (mkCase (ci,rt,iv,f,br), s)
+    | f, (Case ((ci,u,pms,rt,iv,br),cst_l)::s) when refold ->
+      zip (best_state sigma (mkCase (ci,u,pms,rt,iv,f,br), s) cst_l)
+    | f, (Case ((ci,u,pms,rt,iv,br),_)::s) -> zip (mkCase (ci,u,pms,rt,iv,f,br), s)
     | f, (Fix (fix,st,cst_l)::s) when refold ->
       zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l)
   | f, (Fix (fix,st,_)::s) -> zip
@@ -533,7 +537,26 @@ let debug_RAKAM = Reductionops.debug_RAKAM
 let equal_stacks sigma (x, l) (y, l') =
   let f_equal x y = eq_constr sigma x y in
   let eq_fix a b = f_equal (mkFix a) (mkFix b) in
-  Stack.equal f_equal eq_fix l l' && f_equal x y
+  let eq_case (ci1, u1, pms1, p1, _, br1) (ci2, u2, pms2, p2, _, br2) =
+    Array.equal f_equal pms1 pms2 &&
+    f_equal (snd p1) (snd p2) &&
+    Array.equal (fun (_, c1) (_, c2) -> f_equal c1 c2) br1 br2
+  in
+  Stack.equal f_equal eq_fix eq_case l l' && f_equal x y
+
+let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
+  let args = Stack.tail ci.ci_npar args in
+  let args = Option.get (Stack.list_of_app_stack args) in
+  let br = lf.(i - 1) in
+  let subst =
+    if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then
+      (* No let-bindings *)
+      List.rev args
+    else
+      let ctx = expand_branch env sigma u pms (ind, i) br in
+      subst_of_rel_context_instance ctx args
+  in
+  Vars.substl subst (snd br)
 
 let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let open Context.Named.Declaration in
@@ -699,8 +722,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
         | _ -> fold ())
       | _ -> fold ())
 
-    | Case (ci,p,iv,d,lf) ->
-      whrec Cst_stack.empty (d, Stack.Case (ci,p,iv,lf,cst_l) :: stack)
+    | Case (ci,u,pms,p,iv,d,lf) ->
+      whrec Cst_stack.empty (d, Stack.Case ((ci,u,pms,p,iv,lf),cst_l) :: stack)
 
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
@@ -708,13 +731,14 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       |Some (bef,arg,s') ->
         whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s'))
 
-    | Construct ((ind,c),u) ->
+    | Construct (cstr ,u) ->
       let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
       let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(ci, _, _, lf,_)::s') when use_match ->
-          whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+        |args, (Stack.Case(case,_)::s') when use_match ->
+          let r = apply_branch env sigma cstr args case in
+          whrec Cst_stack.empty (r, s')
         |args, (Stack.Proj (p,_)::s') when use_match ->
           whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s')
         |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f90c143a1a..54e9a87c96 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -216,7 +216,7 @@ let build_sym_scheme env ind =
   let c =
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign_ind
-  (mkCase (ci,
+  (mkCase (Inductive.contract_case env (ci,
      my_it_mkLambda_or_LetIn_name
        (lift_rel_context (nrealargs+1) realsign_ind)
        (mkApp (mkIndU indu,Array.concat
@@ -225,7 +225,7 @@ let build_sym_scheme env ind =
            rel_vect (2*nrealargs+2) nrealargs])),
            NoInvert,
      mkRel 1 (* varH *),
-       [|cstr (nrealargs+1)|]))))
+       [|cstr (nrealargs+1)|])))))
   in c, UState.of_context_set ctx
 
 let sym_scheme_kind =
@@ -279,13 +279,13 @@ let build_sym_involutive_scheme env ind =
   let c =
     (my_it_mkLambda_or_LetIn paramsctxt
      (my_it_mkLambda_or_LetIn_name realsign_ind
-      (mkCase (ci,
-               my_it_mkLambda_or_LetIn_name
-               (lift_rel_context (nrealargs+1) realsign_ind)
-               (mkApp (eq,[|
-               mkApp
-               (mkIndU indu, Array.concat
-               [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
+      (mkCase (Inductive.contract_case env (ci,
+                my_it_mkLambda_or_LetIn_name
+                (lift_rel_context (nrealargs+1) realsign_ind)
+                (mkApp (eq,[|
+                mkApp
+                (mkIndU indu, Array.concat
+                [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
                 rel_vect (2*nrealargs+2) nrealargs;
                 rel_vect 1 nrealargs]);
                mkApp (sym,Array.concat
@@ -300,7 +300,7 @@ let build_sym_involutive_scheme env ind =
                mkRel 1|])),
                NoInvert,
                mkRel 1 (* varH *),
-               [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
+               [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))))
   in (c, UState.of_context_set ctx)
 
 let sym_involutive_scheme_kind =
@@ -437,11 +437,11 @@ let build_l2r_rew_scheme dep env ind kind =
                rel_vect 4 nrealargs;
                [|mkRel 2|]])|]]) in
   let main_body =
-    mkCase (ci,
+    mkCase (Inductive.contract_case env (ci,
             my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG,
             NoInvert,
             applied_sym_C 3,
-            [|mkVar varHC|])
+            [|mkVar varHC|]))
   in
   let c =
   (my_it_mkLambda_or_LetIn paramsctxt
@@ -451,7 +451,7 @@ let build_l2r_rew_scheme dep env ind kind =
   (mkNamedLambda (make_annot varHC indr) applied_PC
   (mkNamedLambda (make_annot varH indr) (lift 2 applied_ind)
      (if dep then (* we need a coercion *)
-     mkCase (cieq,
+     mkCase (Inductive.contract_case env (cieq,
        mkLambda (make_annot (Name varH) indr,lift 3 applied_ind,
          mkLambda (make_annot Anonymous indr,
                    mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
@@ -459,7 +459,7 @@ let build_l2r_rew_scheme dep env ind kind =
        NoInvert,
        mkApp (sym_involutive,
          Array.append (Context.Rel.to_extended_vect mkRel 3 mip.mind_arity_ctxt) [|mkVar varH|]),
-       [|main_body|])
+       [|main_body|]))
    else
      main_body))))))
   in (c, UState.of_context_set ctx)
@@ -540,7 +540,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign
   (mkNamedLambda (make_annot varH indr) applied_ind
-  (mkCase (ci,
+  (mkCase (Inductive.contract_case env (ci,
      my_it_mkLambda_or_LetIn_name
        (lift_rel_context (nrealargs+1) realsign_ind)
        (mkNamedProd (make_annot varP indr)
@@ -553,7 +553,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
         (my_it_mkProd_or_LetIn
           (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
       (mkNamedLambda (make_annot varHC indr) applied_PC'
-        (mkVar varHC))|])))))
+        (mkVar varHC))|]))))))
   in c, UState.of_context_set ctx
 
 (**********************************************************************)
@@ -620,7 +620,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
                              (if dep then realsign_ind else realsign)) s)
   (mkNamedLambda (make_annot varHC indr) (lift 1 applied_PG)
   (mkApp
-    (mkCase (ci,
+    (mkCase (Inductive.contract_case env (ci,
        my_it_mkLambda_or_LetIn_name
          (lift_rel_context (nrealargs+3) realsign_ind)
          (mkArrow applied_PG indr (lift (2*nrealargs+5) applied_PC)),
@@ -629,7 +629,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
        [|mkLambda
           (make_annot (Name varHC) indr,
            lift (nrealargs+3) applied_PC,
-           mkRel 1)|]),
+           mkRel 1)|])),
     [|mkVar varHC|]))))))
   in c, UState.of_context_set ctx
 
@@ -825,7 +825,7 @@ let build_congr env (eq,refl,ctx) ind =
            (mkIndU indu,
             Context.Rel.to_extended_list mkRel (mip.mind_nrealargs+2) paramsctxt @
             Context.Rel.to_extended_list mkRel 0 realsign))
-     (mkCase (ci,
+     (mkCase (Inductive.contract_case env (ci,
        my_it_mkLambda_or_LetIn_name
          (lift_rel_context (mip.mind_nrealargs+3) realsign)
          (mkLambda
@@ -843,7 +843,7 @@ let build_congr env (eq,refl,ctx) ind =
        mkVar varH,
        [|mkApp (refl,
           [|mkVar varB;
-            mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|]))))))
+            mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))))
   in c, UState.of_context_set ctx
 
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ace51c40d4..0cc8becd8f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -46,7 +46,7 @@ let rec head_bound sigma t = match EConstr.kind sigma t with
 | Prod (_, _, b)  -> head_bound sigma b
 | LetIn (_, _, _, b) -> head_bound sigma b
 | App (c, _) -> head_bound sigma c
-| Case (_, _, _, c, _) -> head_bound sigma c
+| Case (_, _, _, _, _, c, _) -> head_bound sigma c
 | Ind (ind, _) -> GlobRef.IndRef ind
 | Const (c, _) -> GlobRef.ConstRef c
 | Construct (c, _) -> GlobRef.ConstructRef c
@@ -591,7 +591,7 @@ struct
   let head_evar sigma c =
     let rec hrec c = match EConstr.kind sigma c with
       | Evar (evk,_)   -> evk
-      | Case (_,_,_,c,_) -> hrec c
+      | Case (_,_,_,_,_,c,_) -> hrec c
       | App (c,_)      -> hrec c
       | Cast (c,_,_)   -> hrec c
       | Proj (p, c)    -> hrec c
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 39c5c9562f..b40bdbc25e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3293,7 +3293,7 @@ let expand_projections env sigma c =
   let rec aux env c =
     match EConstr.kind sigma c with
     | Proj (p, c) -> Retyping.expand_projection env sigma p (aux env c) []
-    | _ -> map_constr_with_full_binders sigma push_rel aux env c
+    | _ -> map_constr_with_full_binders env sigma push_rel aux env c
   in
   aux env c
 
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index df07dcbca7..f12d4e5de5 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -335,8 +335,9 @@ struct
           meta
       in
       Meta meta
-    | Case (ci,c1,_iv,c2,ca)     ->
-      Term(DCase(ci,pat_of_constr c1,pat_of_constr c2,Array.map pat_of_constr ca))
+    | Case (ci,u1,pms1,c1,_iv,c2,ca)     ->
+      let f_ctx (_, p) = pat_of_constr p in
+      Term(DCase(ci,f_ctx c1,pat_of_constr c2,Array.map f_ctx ca))
     | Fix ((ia,i),(_,ta,ca)) ->
       Term(DFix(ia,i,Array.map pat_of_constr ta, Array.map pat_of_constr ca))
     | CoFix (i,(_,ta,ca))    ->
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 8663691c0a..1efbc80e93 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -378,6 +378,7 @@ end
 let () = define1 "constr_kind" constr begin fun c ->
   let open Constr in
   Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.tclENV >>= fun env ->
   return begin match EConstr.kind sigma c with
   | Rel n ->
     v_blk 0 [|Value.of_int n|]
@@ -434,7 +435,9 @@ let () = define1 "constr_kind" constr begin fun c ->
       Value.of_ext Value.val_constructor cstr;
       of_instance u;
     |]
-  | Case (ci, c, iv, t, bl) ->
+  | Case (ci, u, pms, c, iv, t, bl) ->
+    (* FIXME: also change representation Ltac2-side? *)
+    let (ci, c, iv, t, bl) = EConstr.expand_case env sigma (ci, u, pms, c, iv, t, bl) in
     v_blk 13 [|
       Value.of_ext Value.val_case ci;
       Value.of_constr c;
@@ -472,6 +475,8 @@ let () = define1 "constr_kind" constr begin fun c ->
 end
 
 let () = define1 "constr_make" valexpr begin fun knd ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.tclENV >>= fun env ->
   let c = match Tac2ffi.to_block knd with
   | (0, [|n|]) ->
     let n = Value.to_int n in
@@ -529,7 +534,7 @@ let () = define1 "constr_make" valexpr begin fun knd ->
     let iv = to_case_invert iv in
     let t = Value.to_constr t in
     let bl = Value.to_array Value.to_constr bl in
-    EConstr.mkCase (ci, c, iv, t, bl)
+    EConstr.mkCase (EConstr.contract_case env sigma (ci, c, iv, t, bl))
   | (14, [|recs; i; nas; cs|]) ->
     let recs = Value.to_array Value.to_int recs in
     let i = Value.to_int i in
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 792f07bb89..9c5f111e28 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -176,7 +176,10 @@ let fold_with_full_binders g f n acc c =
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_,c) -> f n acc c
   | Evar (_,l) -> List.fold_left (f n) acc l
-  | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+  | Case (ci, u, pms, p, iv, c, bl) ->
+    let mib = lookup_mind (fst ci.ci_ind) in
+    let (ci, p, iv, c, bl) = Inductive.expand_case_specif mib (ci, u, pms, p, iv, c, bl) in
+    Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
   | Fix (_,(lna,tl,bl)) ->
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
@@ -201,12 +204,11 @@ let rec traverse current ctx accu t =
 | Construct (((mind, _), _) as cst, _) ->
   traverse_inductive accu mind (ConstructRef cst)
 | Meta _ | Evar _ -> assert false
-| Case (_,oty,_,c,[||]) ->
+| Case (_, _, _, ([|_|], oty), _, c, [||]) when Vars.noccurn 1 oty ->
     (* non dependent match on an inductive with no constructors *)
-    begin match Constr.(kind oty, kind c) with
-    | Lambda(_,_,oty), Const (kn, _)
-      when Vars.noccurn 1 oty &&
-      not (Declareops.constant_has_body (lookup_constant kn)) ->
+    begin match Constr.kind c with
+    | Const (kn, _)
+      when not (Declareops.constant_has_body (lookup_constant kn)) ->
         let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
         traverse_object
           ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f715459616..cc59a96834 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -351,13 +351,13 @@ let build_beq_scheme mode kn =
             done;
 
           ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
-                        (mkCase (ci,do_predicate rel_list nb_cstr_args,NoInvert,
-                                  mkVar (Id.of_string "Y") ,ar2))
+                        (mkCase (Inductive.contract_case env ((ci,do_predicate rel_list nb_cstr_args,
+                                  NoInvert, mkVar (Id.of_string "Y") ,ar2))))
                          (constrsi.(i).cs_args))
         done;
         mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1))  (
           mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2))  (
-            mkCase (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar)))
+            mkCase (Inductive.contract_case env (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar))))
     in (* build_beq_scheme *)
     let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
         types = Array.make nb_ind mkSet and
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c54adb45f9..b3ffb864f2 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -69,9 +69,10 @@ let protect_pattern_in_binder bl c ctypopt =
         | LetIn (x,b,t,c) ->
           let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in
           evd, mkLetIn (x,t,b,c)
-        | Case (ci,p,iv,a,bl) ->
+        | Case (ci,u,pms,p,iv,a,bl) ->
+          let (ci, p, iv, a, bl) = EConstr.expand_case env evd (ci, u, pms, p, iv, a, bl) in
           let evd,bl = Array.fold_left_map (aux env) evd bl in
-          evd, mkCase (ci,p,iv,a,bl)
+          evd, mkCase (EConstr.contract_case env evd (ci, p, iv, a, bl))
         | Cast (c,_,_)    -> f env evd c  (* we remove the cast we had set *)
         (* This last case may happen when reaching the proof of an
            impossible case, as when pattern-matching on a vector of length 1 *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 2be6097184..a91771f22d 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -492,7 +492,7 @@ let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams ~binders:k c =
           end)
         sigma args
     | _ -> Termops.fold_constr_with_full_binders
-             sigma
+             env sigma
              (fun d (env,k) -> EConstr.push_rel d env, k+1)
              aux envk sigma c
   in
diff --git a/vernac/record.ml b/vernac/record.ml
index 68219603b4..96e4a47d2d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -366,7 +366,7 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde
         let ci = Inductiveops.make_case_info env indsp rci LetStyle in
         (* Record projections are always NoInvert because they're at
            constant relevance *)
-        mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None
+        mkCase (Inductive.contract_case env (ci, p, NoInvert, mkRel 1, [|branch|])), None
   in
   let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
   let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in