Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)

Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle

79 files changed, 1571 insertions, 796 deletions

diff --git a/checker/values.ml b/checker/values.ml
index 4e99d087df..907f9f7e32 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 *)
@@ -160,7 +160,11 @@ and v_prec = Tuple ("prec_declaration",
                     [|Array (v_binder_annot v_name); Array v_constr; Array v_constr|])
 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_invert = Sum ("case_inversion", 1, [|[|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 *)
diff --git a/dev/ci/user-overlays/09710-ppedrot-compact-case-repr.sh b/dev/ci/user-overlays/09710-ppedrot-compact-case-repr.sh
new file mode 100644
index 0000000000..dc57e6efb9
--- /dev/null
+++ b/dev/ci/user-overlays/09710-ppedrot-compact-case-repr.sh
@@ -0,0 +1,9 @@
+overlay coq_dpdgraph https://github.com/ppedrot/coq-dpdgraph compact-case-repr 13563
+overlay coqhammer https://github.com/ppedrot/coqhammer compact-case-repr 13563
+overlay elpi https://github.com/ppedrot/coq-elpi compact-case-repr 13563
+overlay equations https://github.com/ppedrot/Coq-Equations compact-case-repr 13563
+overlay metacoq https://github.com/ppedrot/metacoq compact-case-repr 13563
+overlay mtac2 https://github.com/ppedrot/Mtac2 compact-case-repr 13563
+overlay paramcoq https://github.com/ppedrot/paramcoq compact-case-repr 13563
+overlay relation_algebra https://github.com/ppedrot/relation-algebra compact-case-repr 13563
+overlay unicoq https://github.com/ppedrot/unicoq compact-case-repr 13563
diff --git a/dev/doc/case-repr.md b/dev/doc/case-repr.md
new file mode 100644
index 0000000000..e1a78797bd
--- /dev/null
+++ b/dev/doc/case-repr.md
@@ -0,0 +1,122 @@
+## Case representation
+
+Starting from Coq 8.14, the term representation of pattern-matching uses a
+so-called *compact form*. Compared to the previous representation, the major
+difference is that all type and term annotations on lambda and let abstractions
+that were present in branches and return clause of pattern-matchings were
+removed. In order to keep the ability to construct the old expanded form out of
+the new compact form, the case node also makes explicit data that was stealthily
+present in the expanded return clause, namely universe instances and parameters
+of the inductive type being eliminated.
+
+### ML Representation
+
+The case node now looks like
+```
+Case of
+  case_info *
+  Instance.t * (* universe instances of the inductive *)
+  constr array * (* parameters of the inductive *)
+  case_return * (* erased return clause *)
+  case_invert * (* SProp inversion data *)
+  constr * (* scrutinee *)
+  case_branch array (* erased branches *)
+```
+where
+```
+type case_branch = Name.t binder_annot array * constr
+type case_return = Name.t binder_annot array * types
+```
+
+For comparison, pre-8.14 case nodes were defined as follows.
+```
+Case of
+  case_info *
+  constr * (* annotated return clause *)
+  case_invert * (* SProp inversion data *)
+  constr * (* scrutinee *)
+  constr array (* annotated branches *)
+```
+
+### Typing Rules and Invariants
+
+Disregarding the `case_info` cache and the SProp inversion, the typing rules for
+the case node can be given as follows.
+
+Provided
+- Γ ⊢ c : Ind@{u} pms Indices
+- Inductive Ind@{i} Δ : forall Θ, Type := cᵢ : forall Ξᵢ, Ind Δ Aᵢ
+- Γ, Θ@{i := u}{Δ := pms} ⊢ p : Type
+- Γ, Ξᵢ@{i := u}{Δ := pms} ⊢ snd brᵢ : p{Θ := Aᵢ{Δ := pms}}
+
+Then Γ ⊢ Case (_, u, pms, ( _, p), _, c, br) : p{Θ := Indices}
+
+In particular, this implies that Γ ⊢ pms : Δ@{i := u}. Parameters are stored in
+the same order as in the application node.
+
+The u universe instance must be a valid instance for the corresponding
+inductive type, in particular their length must coincide.
+
+The `Name.t binder_annot array` appearing both in the return clause and
+in the branches must satisfy these invariants:
+- For branches, it must have the same length as the corresponding Ξᵢ context
+(including let-ins)
+- For the return clause, it must have the same length as the context
+Θ, self : Ind@{u} pms Θ (including let-ins). The last variable appears as
+the term being destructed and corresponds to the variable introduced by the
+"as" clause of the user-facing syntax.
+- The relevance annotations must match with the corresponding sort of the
+variable from the context.
+
+Note that the annotated variable array is reversed w.r.t. the context,
+i.e. variables appear left to right as in standard practice.
+
+Let-bindings can appear in Δ, Θ or Ξᵢ, since they are arbitrary
+contexts. As a general rule, let bindings appear as binders but not as
+instances. That is, they MUST appear in the variable array, but they MUST NOT
+appear in the parameter array.
+
+Example:
+```
+Inductive foo (X := tt) : forall (Y := X), Type := Foo : forall (Z := X), foo.
+
+Definition case (x : foo) : unit := match x as x₀ in foo with Foo _ z => z end
+```
+The case node of the `case` function is represented as
+```
+Case (
+  _,
+  Instance.empty,
+  [||],
+  ([|(Y, Relevant); (x₀, Relevant)|], unit), (* let (Y := tt) in fun (x₀ : foo) => unit *)
+  NoInvert,
+  #1,
+  [|
+    ([|(z, Relevant)|], #1) (* let z := tt in z *)
+  |]
+)
+```
+
+This choice of representation for let-bindings requires access to the
+environment in some cases, e.g. to compute branch reduction. There is a
+fast-path for non-let-containing inductive types though, which are the vast
+majority.
+
+### Porting plugins
+
+The conversion functions from and to the expanded form are:
+- `[Inductive, EConstr].expand_case` which goes from the compact to the expanded
+form and cannot fail (assuming the term was well-typed)
+- `[Inductive, EConstr].contract_case` which goes the other way and will
+raise anomalies if the expanded forms are not fully eta-expanded.
+
+As such, it is always painless to convert to the old representation. Converting
+the other way, you must ensure that all the terms you provide the
+compatibility function with are fully eta-expanded, **including let-bindings**.
+This works as expected for the common case with eta-expanded branches but will
+fail for plugins that generate non-eta-expanded branches.
+
+Some other useful variants of these functions are:
+- `Inductive.expand_case_specif`
+- `EConstr.annotate_case`
+- `EConstr.expand_branch`
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/doc/changelog/01-kernel/13563-compact-case-repr.rst b/doc/changelog/01-kernel/13563-compact-case-repr.rst
new file mode 100644
index 0000000000..c8ee9bc1e6
--- /dev/null
+++ b/doc/changelog/01-kernel/13563-compact-case-repr.rst
@@ -0,0 +1,15 @@
+- **Changed:**
+  The term representation of pattern-matchings now uses a compact form that
+  provides a few static guarantees such as eta-expansion of branches and return
+  clauses and is usually more efficient. The most visible user change is that for
+  the time being, the :tacn:`destruct` tactic and its variants generate dummy
+  cuts (β redexes) in the branches of the generated proof.
+  This can also generate very uncommon backwards incompatibilities, such as a
+  change of occurrence numbering for subterms, or breakage of unification in
+  complex situations involving pattern-matchings whose underlying inductive type
+  declares let-bindings in parameters, arity or constructor types. For ML plugin
+  developers, an in-depth description of the new representation, as well as
+  porting tips, can be found in dev/doc/case-repr.md
+  (`#13563 <https://github.com/coq/coq/pull/13563>`_,
+  fixes `#3166 <https://github.com/coq/coq/issues/3166>`_,
+  by Pierre-Marie Pédrot).
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c29de27efb..157995a173 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 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,61 @@ 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 annotate_case env sigma (ci, u, pms, p, iv, c, bl as case) =
+  let (_, p, _, _, bl) = expand_case env sigma case in
+  let p =
+    (* Too bad we need to fetch this data in the environment, should be in the
+      case_info instead. *)
+    let (_, mip) = Inductive.lookup_mind_specif env ci.ci_ind in
+    decompose_lam_n_decls sigma (mip.Declarations.mind_nrealdecls + 1) p
+  in
+  let mk_br c n = decompose_lam_n_decls sigma n c in
+  let bl = Array.map2 mk_br bl ci.ci_cstr_ndecls in
+  (ci, u, pms, 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 +424,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) ->
+    let (ci, _, pms, p, iv, c, bl) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+    let f_ctx (ctx, c) = f (List.fold_right g ctx n) c in
+    Array.Fun1.iter f n pms; f_ctx p; iter_invert (f n) iv; f n c; Array.iter f_ctx bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
@@ -566,8 +636,8 @@ 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=_},_,_) ->
-      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma univs)) s in
+    | Case (_,u,_,_,_,_,_) ->
+      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..0d038e9a67 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 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,21 @@ 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 annotate_case : Environ.env -> Evd.evar_map -> case ->
+  case_info * EInstance.t * t array * (rel_context * t) * case_invert * t * (rel_context * t) array
+(** Same as above, but doesn't turn contexts into binders *)
+
+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 +363,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 +389,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..58f635b7bd 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 pcase_invert -> econstr pcase_invert
+  val unsafe_to_case_invert : econstr pcase_invert -> constr 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..4dc584cfa8 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,20 @@ 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) ->
+      let (ci, _, pms, p0, _, b, bl0) = annotate_case env sigma (ci, u, pms, p, iv, b, bl) in
+      let f_ctx (nas, _ as r) (ctx, c) =
+        let c' = f (List.fold_right g ctx l) c in
+        if c' == c then r else (nas, c')
+      in
       (* In v8 concrete syntax, predicate is after the term to match! *)
       let b' = f l b in
+      let pms' = Array.map_left (f l) pms in
+      let p' = f_ctx p p0 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')
+      let bl' = Array.map_left (fun (c, c0) -> f_ctx c c0) (Array.map2 (fun x y -> (x, y)) bl bl0) in
+        if b' == b && pms' == pms && p' == p && iv' == iv && bl' == bl then c
+        else mkCase (ci, u, pms', 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 +683,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 +716,19 @@ 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) ->
-      let p' = f l p in
+  | Case (ci, u, pms, p, iv, c, bl) ->
+      let (ci, _, pms, p0, _, c, bl0) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+      let f_ctx (nas, _ as r) (ctx, c) =
+        let c' = f (List.fold_right g ctx l) c in
+        if c' == c then r else (nas, c')
+      in
+      let pms' = Array.Smart.map (f l) pms in
+      let p' = f_ctx p p0 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')
+      let bl' = Array.map2 f_ctx bl bl0 in
+      if pms==pms' && p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
+        mkCase (ci, u, pms', 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 +749,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 +756,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 +768,10 @@ 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, _, pms, p, _, c, bl) = EConstr.annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+    let f_ctx acc (ctx, c) = f (List.fold_right g ctx n) acc c in
+    Array.fold_left f_ctx (f n (fold_invert (f n) (f_ctx (Array.fold_left (f n) acc pms) 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..330ed5d0ad 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -68,6 +68,10 @@ 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, iv, c, br) ->
+      let u' = fi u in
+      if u' == u then map aux t
+      else (changed := true; map aux (mkCase (ci, u', pms, p, iv, c, br)))
     | _ -> map aux t
   in
   let c' = aux c in
@@ -147,10 +151,10 @@ 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) ->
-      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))
+    | Case (ci,u,pms,p,iv,t,br) ->
+      let u' = Instance.subst_fn lsubst u in
+      if u' == u then Constr.map aux c
+      else Constr.map aux (mkCase (ci,u',pms,p,iv,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..a32c8f1cd1 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
@@ -355,7 +357,7 @@ and fterm =
   | FCLOS of constr * fconstr subs
   | FLOCKED
 
-and finvert = Univ.Instance.t * fconstr array
+and finvert = fconstr array
 
 let fterm_of v = v.term
 let set_ntrl v = v.mark <- Mark.set_ntrl v.mark
@@ -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) ->
-      let iv = CaseInvert {univs;args=Array.map (to_constr lfts) args} in
-       to_constr_case lfts ci p iv 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, indices, c, ve, env) ->
+      let iv = CaseInvert {indices=Array.map (to_constr lfts) indices} in
+      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{indices},t,br) ->
+      let term = FCaseInvert (ci, u, pms, p, (Array.map (mk_clos e) indices), 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,8 +1478,9 @@ 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 ->
-    begin match case_inversion info tab ci iv v with
+  | FCaseInvert (ci, u, pms, _p,iv,_c,v,env) when red_set info.i_flags fMATCH ->
+    let pms = mk_clos_vect env pms in
+    begin match case_inversion info tab ci u pms iv v with
       | Some c -> knit info tab env c stk
       | None -> (m, stk)
     end
@@ -1417,13 +1497,17 @@ and knit info tab e t stk =
   let (ht,s) = knht info e t stk in
   knr info tab ht s
 
-and case_inversion info tab ci (univs,args) v =
+and case_inversion info tab ci u params indices 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 indices then Some v
   else
     let env = info_env info in
     let ind = ci.ci_ind in
-    let params, indices = Array.chop ci.ci_npar args in
     let psubst = subs_consn params 0 ci.ci_npar (subs_id 0) in
     let mib = Environ.lookup_mind (fst ind) env in
     let mip = mib.mind_packets.(snd ind) in
@@ -1432,12 +1516,12 @@ and case_inversion info tab ci (univs,args) v =
     let _ind, expect_args = destApp expect in
     let check_index i index =
       let expected = expect_args.(ci.ci_npar + i) in
-      let expected = Vars.subst_instance_constr univs expected in
+      let expected = Vars.subst_instance_constr u expected in
       let expected = mk_clos psubst expected in
       !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..30542597c5 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -83,9 +83,15 @@ type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
-type ('constr, 'univs) case_invert =
+type 'constr pcase_invert =
   | NoInvert
-  | CaseInvert of { univs : 'univs; args : 'constr array }
+  | CaseInvert of { indices : '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 pcase_invert * 'constr * 'constr pcase_branch array
 
 (* [Var] is used for named variables and [Rel] for variables as
    de Bruijn indices. *)
@@ -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 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 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
@@ -471,8 +481,8 @@ let decompose_appvect c =
 
 let fold_invert f acc = function
   | NoInvert -> acc
-  | CaseInvert {univs=_;args} ->
-    Array.fold_left f acc args
+  | CaseInvert {indices} ->
+    Array.fold_left f acc indices
 
 let fold f acc c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -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)) ->
@@ -498,8 +509,8 @@ let fold f acc c = match kind c with
 
 let iter_invert f = function
   | NoInvert -> ()
-  | CaseInvert {univs=_; args;} ->
-    Array.iter f args
+  | CaseInvert {indices;} ->
+    Array.iter f indices
 
 let iter f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -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,62 +597,39 @@ 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
-  | CaseInvert {univs;args;} as orig ->
-    let args' = Array.Smart.map f args in
-    if args == args' then orig
-    else CaseInvert {univs;args=args';}
+  | CaseInvert {indices;} as orig ->
+    let indices' = Array.Smart.map f indices in
+    if indices == indices' then orig
+    else CaseInvert {indices=indices';}
 
-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 ->
+  | 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' = 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) ->
-      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,17 +691,26 @@ 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
   | NoInvert -> acc, NoInvert
-  | CaseInvert {univs;args;} as orig ->
-    let acc, args' = Array.fold_left_map f acc args in
-    if args==args' then acc, orig
-    else acc, CaseInvert {univs;args=args';}
+  | CaseInvert {indices;} as orig ->
+    let acc, indices' = Array.fold_left_map f acc indices in
+    if indices==indices' then acc, orig
+    else acc, CaseInvert {indices=indices';}
+
+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 _
@@ -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
@@ -878,13 +881,15 @@ type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool
    optimisation that physically equal arrays are equals (hence the
    calls to {!Array.equal_norefl}). *)
 
-let eq_invert eq leq_universes iv1 iv2 =
+let eq_invert eq iv1 iv2 =
   match iv1, iv2 with
   | NoInvert, NoInvert -> true
   | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false
-  | CaseInvert {univs;args}, CaseInvert iv2 ->
-    leq_universes univs iv2.univs
-    && Array.equal eq args iv2.args
+  | CaseInvert {indices}, CaseInvert iv2 ->
+    Array.equal eq indices iv2.indices
+
+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
@@ -911,8 +916,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) 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
@@ -1050,8 +1059,7 @@ let compare_invert f iv1 iv2 =
   | NoInvert, CaseInvert _ -> -1
   | CaseInvert _, NoInvert -> 1
   | CaseInvert iv1, CaseInvert iv2 ->
-    (* univs ignored deliberately *)
-    Array.compare f iv1.args iv2.args
+    Array.compare f iv1.indices iv2.indices
 
 let constr_ord_int f t1 t2 =
   let (=?) f g i1 i2 j1 j2=
@@ -1063,6 +1071,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 +1107,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))
@@ -1176,9 +1188,11 @@ let invert_eqeq iv1 iv2 =
   match iv1, iv2 with
   | NoInvert, NoInvert -> true
   | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false
-  | CaseInvert iv1, CaseInvert iv2 ->
-    iv1.univs == iv2.univs
-    && iv1.args == iv2.args
+  | CaseInvert {indices=i1}, CaseInvert {indices=i2} ->
+    i1 == i2
+
+let hasheq_ctx (nas1, c1) (nas2, c2) =
+  array_eqeq nas1 nas2 && c1 == c2
 
 let hasheq t1 t2 =
   match t1, t2 with
@@ -1197,8 +1211,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 +1264,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 +1306,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
@@ -1334,10 +1365,9 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
 
   and sh_invert = function
     | NoInvert -> NoInvert, 0
-    | CaseInvert {univs;args;} ->
-      let univs, hu = sh_instance univs in
-      let args, ha = hash_term_array args in
-      CaseInvert {univs;args;}, combinesmall 1 (combine hu ha)
+    | CaseInvert {indices;} ->
+      let indices, ha = hash_term_array indices in
+      CaseInvert {indices;}, combinesmall 1 ha
 
   and sh_rec t =
     let (y, h) = hash_term t in
@@ -1400,8 +1430,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)) ->
@@ -1417,8 +1447,8 @@ let rec hash t =
 
 and hash_invert = function
   | NoInvert -> 0
-  | CaseInvert {univs;args;} ->
-    combinesmall 1 (combine (Instance.hash univs) (hash_term_array args))
+  | CaseInvert {indices;} ->
+    combinesmall 1 (hash_term_array indices)
 
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine acc (hash t)) 0 t
@@ -1426,6 +1456,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 +1586,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)) ->
@@ -1573,6 +1613,6 @@ let rec debug_print c =
 
 and debug_invert = let open Pp in function
   | NoInvert -> mt()
-  | CaseInvert {univs;args;} ->
-    spc() ++ str"Invert {univs=" ++ Instance.pr Level.pr univs ++
-    str "; args=" ++ prlist_with_sep spc debug_print (Array.to_list args) ++ str "} "
+  | CaseInvert {indices;} ->
+    spc() ++ str"Invert {indices=" ++
+    prlist_with_sep spc debug_print (Array.to_list indices) ++ str "} "
diff --git a/kernel/constr.mli b/kernel/constr.mli
index ed63ac507c..57dd850ee7 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -49,11 +49,11 @@ type case_info =
     ci_pp_info    : case_printing   (* not interpreted by the kernel *)
   }
 
-type ('constr, 'univs) case_invert =
+type 'constr pcase_invert =
   | NoInvert
   (** Normal reduction: match when the scrutinee is a constructor. *)
 
-  | CaseInvert of { univs : 'univs; args : 'constr array; }
+  | CaseInvert of { indices : 'constr array; }
   (** Reduce when the indices match those of the unique constructor.
       (SProp to non SProp only) *)
 
@@ -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 pcase_invert * 'constr * 'constr pcase_branch array
+
+type case_invert = constr 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 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 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 pcase_invert -> 'a 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 pcase_invert -> 'a * 'b 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 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
@@ -603,8 +597,8 @@ val compare_head_gen_leq : Univ.Instance.t instance_compare_fn ->
   constr constr_compare_fn ->
   constr constr_compare_fn
 
-val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool)
-  -> ('a, 'b) case_invert -> ('a, 'b) case_invert -> bool
+val eq_invert : ('a -> 'a -> bool)
+  -> 'a pcase_invert -> 'a pcase_invert -> bool
 
 (** {6 Hashconsing} *)
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3707a75157..f82b754c59 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -75,30 +75,23 @@ 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
+          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/kernel.mllib b/kernel/kernel.mllib
index 5b2a7bd9c2..75fd70d923 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -31,6 +31,8 @@ Primred
 CClosure
 Relevanceops
 Reduction
+Type_errors
+Inductive
 Vmlambda
 Nativelambda
 Vmbytegen
@@ -40,9 +42,7 @@ Vmsymtable
 Vm
 Vconv
 Nativeconv
-Type_errors
 Modops
-Inductive
 Typeops
 InferCumulativity
 IndTyping
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..741491c917 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -548,22 +548,26 @@ 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
-          | CaseInvert {univs;args} ->
-            let ct' = mkApp (mkIndU (ci.ci_ind,univs), args) in
+          | CaseInvert {indices} ->
+            let args = Array.append pms indices in
+            let ct' = mkApp (mkIndU (ci.ci_ind,u), args) in
             let (ct', _) : constr * Sorts.t = execute_is_type env ct' in
             let () = conv_leq false env ct ct' in
             let _, args' = decompose_appvect ct' in
-            if args == args' then iv else CaseInvert {univs;args=args'}
+            if args == args' then iv
+            else CaseInvert {indices=Array.sub args' (Array.length pms) (Array.length indices)}
         in
         let p', pt = execute env p in
         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 +724,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..b09577d4db 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -253,12 +253,20 @@ 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 {indices}, c, br) ->
+        if Univ.Instance.is_empty u then Constr.map aux t
         else
-          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)))
+          let u' = f u in
+          if u' == u then Constr.map aux t
+          else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},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 +313,18 @@ 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) ->
-        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))
+      | Case (ci, u, pms, p, CaseInvert {indices}, c, br) ->
+        let u' = f u in
+        if u' == u then Constr.map aux t
+        else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},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 +364,8 @@ 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=_},_,_) ->
-      let s = LSet.fold LSet.add (Instance.levels univs) s in
+    | Case (_, u, _, _, _,_ ,_) ->
+      let s = LSet.fold LSet.add (Instance.levels u) s in
       Constr.fold aux 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..bb5125f5ed 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+module CVars = Vars
+
 open Pp
 open CErrors
 open Util
@@ -33,6 +35,78 @@ type detyping_flags = {
   flg_isgoal : bool;
 }
 
+(** Reimplementation of kernel case expansion functions in more lenient way *)
+module RobustExpand :
+sig
+val return_clause : Environ.env -> Evd.evar_map -> Ind.t ->
+  EInstance.t -> EConstr.t array -> EConstr.case_return -> rel_context * EConstr.t
+val branch : Environ.env -> Evd.evar_map -> Construct.t ->
+  EInstance.t -> EConstr.t array -> EConstr.case_branch -> rel_context * EConstr.t
+end =
+struct
+open CVars
+open Declarations
+open Univ
+open Constr
+
+let instantiate_context u subst nas ctx =
+  let rec instantiate i ctx = match ctx with
+  | [] -> []
+  | 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
+  let () = if not (Int.equal (Array.length nas) (List.length ctx)) then raise Exit in
+  instantiate (Array.length nas - 1) ctx
+
+let return_clause env sigma ind u params (nas, p) =
+  try
+    let u = EConstr.Unsafe.to_instance u in
+    let params = EConstr.Unsafe.to_constr_array params in
+    let () = if not @@ Environ.mem_mind (fst ind) env then raise Exit in
+    let mib = Environ.lookup_mind (fst ind) env in
+    let mip = mib.mind_packets.(snd ind) in
+    let paramdecl = subst_instance_context u mib.mind_params_ctxt in
+    let paramsubst = subst_of_rel_context_instance paramdecl (Array.to_list params) 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 (ind, inst), args)
+    in
+    let realdecls = LocalAssum (Context.anonR, self) :: realdecls in
+    let realdecls = instantiate_context u paramsubst nas realdecls in
+    List.map EConstr.of_rel_decl realdecls, p
+  with e when CErrors.noncritical e ->
+    let dummy na = LocalAssum (na, EConstr.mkProp) in
+    List.rev (Array.map_to_list dummy nas), p
+
+let branch env sigma (ind, i) u params (nas, br) =
+  try
+    let u = EConstr.Unsafe.to_instance u in
+    let params = EConstr.Unsafe.to_constr_array params in
+    let () = if not @@ Environ.mem_mind (fst ind) env then raise Exit in
+    let mib = Environ.lookup_mind (fst ind) env in
+    let mip = mib.mind_packets.(snd ind) in
+    let paramdecl = subst_instance_context u mib.mind_params_ctxt in
+    let paramsubst = subst_of_rel_context_instance paramdecl (Array.to_list params) 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 ctx = instantiate_context u subst nas ctx in
+    List.map EConstr.of_rel_decl ctx, br
+  with e when CErrors.noncritical e ->
+    let dummy na = LocalAssum (na, EConstr.mkProp) in
+    List.rev (Array.map_to_list dummy nas), br
+
+end
+
 module Avoid :
 sig
   type t
@@ -241,16 +315,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 +325,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
@@ -393,30 +457,27 @@ let update_name sigma na ((_,(e,_)),c) =
   | _ ->
       na
 
-let get_domain env sigma c =
-  let (_,t,_) = EConstr.destProd sigma (Reductionops.whd_all env sigma (Retyping.get_type_of env sigma c)) in
-  t
-
-let rec decomp_branch tags nal flags (avoid,env as e) sigma c =
-  match tags with
-  | [] -> (List.rev nal,(e,c))
-  | b::tags ->
+let decomp_branch flags e sigma (ctx, c) =
+  let n = List.length ctx in
+  let rec aux i nal (avoid, env as e) c =
+    if Int.equal i 0 then (List.rev nal,(e,c))
+    else
       let decl, c, let_in =
-        match EConstr.kind sigma (strip_outer_cast sigma c), b with
-        | Lambda (na,t,c),false -> LocalAssum (na,t), c, true
-        | LetIn (na,b,t,c),true -> LocalDef (na,b,t), c, false
-        | _, false ->
-          let na = make_annot (Name default_dependent_ident) Sorts.Relevant (* dummy *) in
-          LocalAssum (na, get_domain (snd env) sigma c), applist (lift 1 c, [mkRel 1]), false
-        | _, true ->
-          let na = make_annot Anonymous Sorts.Relevant (* dummy *) in
-          LocalDef (na, mkProp (* dummy *), type1), lift 1 c, false
+        match EConstr.kind sigma c with
+        | Lambda (na,t,c) -> LocalAssum (na,t), c, true
+        | LetIn (na,b,t,c) -> LocalDef (na,b,t), c, false
+        | _ -> assert false
     in
     let na',avoid' = compute_name sigma ~let_in ~pattern:true flags avoid env (get_name decl) c in
-    decomp_branch tags (na'::nal) flags
-      (avoid', add_name (set_name na' decl) env) sigma c
+    aux (i - 1) (na'::nal) (avoid', add_name (set_name na' decl) env) c
+  in
+  aux n [] e (EConstr.it_mkLambda_or_LetIn c ctx)
 
-let rec build_tree na isgoal e sigma ci cl =
+let rec build_tree na isgoal e sigma (ci, u, pms, cl) =
+  let map i br =
+    RobustExpand.branch (snd (snd e)) sigma (ci.ci_ind, i + 1) u pms br
+  in
+  let cl = Array.mapi map cl in
   let mkpat n rhs pl =
     let na = update_name sigma na rhs in
     na, DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,na) in
@@ -429,12 +490,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 *) ->
-        let clauses = build_tree na isgoal e sigma ci cl in
+        computable sigma p (* FIXME: can do better *) ->
+        let clauses = build_tree na isgoal e sigma (ci, u, pms, cl) in
         List.flatten
           (List.map (fun (ids,pat,rhs) ->
               let lines = align_tree nal isgoal rhs sigma in
@@ -447,7 +508,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
         List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat
 
 and contract_branch isgoal e sigma (cdn,mkpat,rhs) =
-  let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in
+  let nal,rhs = decomp_branch isgoal e sigma rhs in
   let mat = align_tree nal isgoal rhs sigma in
   List.map (fun (ids,hd,rhs) ->
       let na, pat = mkpat rhs hd in
@@ -457,15 +518,10 @@ and contract_branch isgoal e sigma (cdn,mkpat,rhs) =
 (* Transform internal representation of pattern-matching into list of *)
 (* clauses                                                            *)
 
-let is_nondep_branch sigma c l =
-  try
-    (* FIXME: do better using tags from l *)
-    let sign,ccl = decompose_lam_n_decls sigma (List.length l) c in
-    noccur_between sigma 1 (Context.Rel.length sign) ccl
-  with e when CErrors.noncritical e -> (* Not eta-expanded or not reduced *)
-    false
+let is_nondep_branch sigma (nas, ccl) =
+  noccur_between sigma 1 (Array.length nas) ccl
 
-let extract_nondep_branches test c b l =
+let extract_nondep_branches b l =
   let rec strip l r =
     match DAst.get r, l with
       | r', [] -> r
@@ -473,7 +529,7 @@ let extract_nondep_branches test c b l =
       | GLetIn (_,_,_,t), true::l -> strip l t
       (* FIXME: do we need adjustment? *)
       | _,_ -> assert false in
-  if test c l then Some (strip l b) else None
+  strip l b
 
 let it_destRLambda_or_LetIn_names l c =
   let rec aux l nal c =
@@ -498,13 +554,14 @@ let it_destRLambda_or_LetIn_names l c =
               | _ -> DAst.make @@ GApp (c,[a]))
   in aux l [] c
 
-let detype_case computable detype detype_eqns testdep avoid ci p iv c bl =
+let detype_case computable detype detype_eqns avoid env sigma (ci, univs, params, p, iv, c, bl) =
   let synth_type = synthetize_type () in
   let tomatch = detype c in
   let tomatch = match iv with
     | NoInvert -> tomatch
-    | CaseInvert {univs;args} ->
-      let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
+    | CaseInvert {indices} ->
+      (* XXX use holes instead of params? *)
+      let t = mkApp (mkIndU (ci.ci_ind,univs), Array.append params indices) in
       DAst.make @@ GCast (tomatch, CastConv (detype t))
   in
   let alias, aliastyp, pred=
@@ -512,6 +569,8 @@ let detype_case computable detype detype_eqns testdep avoid ci p iv c bl =
     then
       Anonymous, None, None
     else
+      let (ctx, p) = RobustExpand.return_clause (snd env) sigma ci.ci_ind univs params p in
+      let p = EConstr.it_mkLambda_or_LetIn p ctx in
       let p = detype p in
       let nl,typ = it_destRLambda_or_LetIn_names ci.ci_pp_info.ind_tags p in
       let n,typ = match DAst.get typ with
@@ -540,21 +599,29 @@ let detype_case computable detype detype_eqns testdep avoid ci p iv c bl =
   let constagsl = ci.ci_pp_info.cstr_tags in
   match tag, aliastyp with
   | LetStyle, None ->
+      let map i br =
+        let (ctx, body) = RobustExpand.branch (snd env) sigma (ci.ci_ind, i + 1) univs params br in
+        EConstr.it_mkLambda_or_LetIn body ctx
+      in
+      let bl = Array.mapi map bl in
       let bl' = Array.map detype bl in
       let (nal,d) = it_destRLambda_or_LetIn_names constagsl.(0) bl'.(0) in
       GLetTuple (nal,(alias,pred),tomatch,d)
   | IfStyle, None ->
-      let bl' = Array.map detype bl in
-      let nondepbrs =
-        Array.map3 (extract_nondep_branches testdep) bl bl' constagsl in
-      if Array.for_all ((!=) None) nondepbrs then
-        GIf (tomatch,(alias,pred),
-             Option.get nondepbrs.(0),Option.get nondepbrs.(1))
+      if Array.for_all (fun br -> is_nondep_branch sigma br) bl then
+        let map i br =
+          let ctx, body = RobustExpand.branch (snd env) sigma (ci.ci_ind, i + 1) univs params br in
+          EConstr.it_mkLambda_or_LetIn body ctx
+        in
+        let bl = Array.mapi map bl in
+        let bl' = Array.map detype bl in
+        let nondepbrs = Array.map2 extract_nondep_branches bl' constagsl in
+        GIf (tomatch,(alias,pred), nondepbrs.(0), nondepbrs.(1))
       else
-        let eqnl = detype_eqns constructs constagsl bl in
+        let eqnl = detype_eqns constructs constagsl (ci, univs, params, bl) in
         GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
-      let eqnl = detype_eqns constructs constagsl bl in
+      let eqnl = detype_eqns constructs constagsl (ci, univs, params, bl) in
       GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let rec share_names detype flags n l avoid env sigma c t =
@@ -788,12 +855,12 @@ 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 case = (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
-          ci p iv c bl
+          (detype_eqns d flags avoid env sigma comp)
+          avoid env sigma case
     | Fix (nvn,recdef) -> detype_fix (detype d) flags avoid env sigma nvn recdef
     | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef
     | Int i -> GInt i
@@ -805,18 +872,21 @@ and detype_r d flags avoid env sigma t =
       let u = detype_instance sigma u in
       GArray(u, t, def, ty)
 
-and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
+and detype_eqns d flags avoid env sigma computable constructs consnargsl bl =
   try
     if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
-    let mat = build_tree Anonymous flags (avoid,env) sigma ci bl in
+    let mat = build_tree Anonymous flags (avoid,env) sigma bl in
     List.map (fun (ids,pat,((avoid,env),c)) ->
         CAst.make (Id.Set.elements ids,[pat],detype d flags avoid env sigma c))
       mat
   with e when CErrors.noncritical e ->
+    let (ci, u, pms, bl) = bl in
     Array.to_list
-      (Array.map3 (detype_eqn d flags avoid env sigma) constructs consnargsl bl)
+      (Array.map3 (detype_eqn d flags avoid env sigma u pms) constructs consnargsl bl)
 
-and detype_eqn d flags avoid env sigma constr construct_nargs branch =
+and detype_eqn d flags avoid env sigma u pms constr construct_nargs br =
+  let ctx, body = RobustExpand.branch (snd env) sigma constr u pms br in
+  let branch = EConstr.it_mkLambda_or_LetIn body ctx in
   let make_pat decl avoid env b ids =
     if force_wildcard () && noccurn sigma 1 b then
       DAst.make @@ PatVar Anonymous,avoid,(add_name (set_name Anonymous decl) env),ids
@@ -824,39 +894,24 @@ and detype_eqn d flags avoid env sigma constr construct_nargs branch =
       let na,avoid' = compute_name sigma ~let_in:false ~pattern:true flags avoid env (get_name decl) b in
       DAst.make (PatVar na),avoid',(add_name (set_name na decl) env),add_vname ids na
   in
-  let rec buildrec ids patlist avoid env l b =
-    match EConstr.kind sigma b, l with
-      | _, [] -> CAst.make @@
+  let rec buildrec ids patlist avoid env n b =
+    if Int.equal n 0 then
+      CAst.make @@
         (Id.Set.elements ids,
          [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)],
          detype d flags avoid env sigma b)
-      | Lambda (x,t,b), false::l ->
+    else match EConstr.kind sigma b with
+      | Lambda (x,t,b) ->
             let pat,new_avoid,new_env,new_ids = make_pat (LocalAssum (x,t)) avoid env b ids in
-            buildrec new_ids (pat::patlist) new_avoid new_env l b
+            buildrec new_ids (pat::patlist) new_avoid new_env (pred n) b
 
-      | LetIn (x,b,t,b'), true::l ->
+      | LetIn (x,b,t,b') ->
             let pat,new_avoid,new_env,new_ids = make_pat (LocalDef (x,b,t)) avoid env b' ids in
-            buildrec new_ids (pat::patlist) new_avoid new_env l b'
-
-      | Cast (c,_,_), l ->    (* Oui, il y a parfois des cast *)
-            buildrec ids patlist avoid env l c
-
-      | _, true::l ->
-            let pat = DAst.make @@ PatVar Anonymous in
-            buildrec ids (pat::patlist) avoid env l b
-
-      | _, false::l ->
-            (* eta-expansion : n'arrivera plus lorsque tous les
-               termes seront construits à partir de la syntaxe Cases *)
-            (* nommage de la nouvelle variable *)
-            let new_b = applist (lift 1 b, [mkRel 1]) in
-            let typ = get_domain (snd env) sigma b in
-            let pat,new_avoid,new_env,new_ids =
-              make_pat (LocalAssum (make_annot Anonymous Sorts.Relevant (* dummy *),typ)) avoid env new_b ids in
-            buildrec new_ids (pat::patlist) new_avoid new_env l new_b
+            buildrec new_ids (pat::patlist) new_avoid new_env (pred n) b'
 
+      | _ -> assert false
   in
-  buildrec Id.Set.empty [] avoid env construct_nargs branch
+  buildrec Id.Set.empty [] avoid env (List.length ctx) branch
 
 and detype_binder d flags bk avoid env sigma decl c =
   let na = get_name decl in
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..d02b015604 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -344,11 +344,7 @@ let get_projections = Environ.get_projections
 
 let make_case_invert env (IndType (((ind,u),params),indices)) ci =
   if Typeops.should_invert_case env ci
-  then
-    let univs = EConstr.EInstance.make u in
-    let params = Array.map_of_list EConstr.of_constr params in
-    let args = Array.append params (Array.of_list indices) in
-    CaseInvert {univs;args}
+  then CaseInvert {indices=Array.of_list indices}
   else NoInvert
 
 let make_case_or_project env sigma indt ci pred c branches =
@@ -356,8 +352,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 +744,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..92e412a537 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -320,13 +320,13 @@ and nf_atom_type env sigma atom =
   | Acase(ans,accu,p,bs) ->
       let a,ta = nf_accu_type env sigma accu in
       let ((mind,_),u as ind),allargs = find_rectype_a env ta in
-      let iv = if Typeops.should_invert_case env ans.asw_ci then
-          CaseInvert {univs=u; args=allargs}
-        else NoInvert
-      in
       let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
       let nparams = mib.mind_nparams in
       let params,realargs = Array.chop nparams allargs in
+      let iv = if Typeops.should_invert_case env ans.asw_ci then
+          CaseInvert {indices=realargs}
+        else NoInvert
+      in
       let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
       let pT =
         hnf_prod_applist_assum env nparamdecls
@@ -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..3da75f67b9 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 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 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
+  if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then
+    (* No let-bindings *)
+    let subst = List.rev args in
+    Vars.substl subst (snd br)
+  else
+    (* For backwards compat with unification, we do not reduce the let-bindings
+       upfront. *)
+    let ctx = expand_branch env sigma u pms (ind, i) br in
+    applist (it_mkLambda_or_LetIn (snd br) ctx, args)
+
 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..59bc4a8b72 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 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..5b8b367ff2 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,20 +383,23 @@ 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
         let sigma = match iv with
           | NoInvert -> sigma
-          | CaseInvert {univs;args} ->
-            let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
+          | CaseInvert {indices} ->
+            let args = Array.append pms indices in
+            let t = mkApp (mkIndU (ci.ci_ind,u), args) in
             let sigma, tj = execute env sigma t in
             let sigma, tj = type_judgment env sigma tj in
             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..cf6d581066 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -284,10 +284,10 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       let tcase = build_case_type p realargs c in
       let ci = Inductiveops.make_case_info env ind relevance RegularStyle in
       let iv = if Typeops.should_invert_case env ci then
-          CaseInvert {univs=u; args=allargs}
+          CaseInvert {indices=realargs}
         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..8b31c07f5e 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)
 
@@ -479,13 +478,7 @@ and treat_case ~check env sigma ci lbrty lf acc' =
   | App (f,cl) -> (f, cl)
   | _ -> (c,[||]) in
   Array.fold_left3
-    (fun (lacc,sigma,bacc) ty fi l ->
-        if isMeta (strip_outer_cast fi) then
-          (* Support for non-eta-let-expanded Meta as found in *)
-          (* destruct/case with an non eta-let expanded elimination scheme *)
-          let (r,_,s,fi') = mk_refgoals ~check env sigma lacc ty fi in
-          r,s,(fi'::bacc)
-        else
+    (fun (lacc,sigma,bacc) ty fi n ->
         (* Deal with a branch in expanded form of the form
            Case(ci,p,c,[|eta-let-exp(Meta);...;eta-let-exp(Meta)|]) as
            if it were not so, so as to preserve compatibility with when
@@ -494,7 +487,6 @@ and treat_case ~check env sigma ci lbrty lf acc' =
            CAUTION: it does not deal with the general case of eta-zeta
            reduced branches having a form different from Meta, as it
            would be theoretically the case with third-party code *)
-        let n = List.length l in
         let ctx, body = Term.decompose_lam_n_decls n fi in
         let head, args = decompose_app_vect body in
         (* Strip cast because clenv_cast_meta adds a cast when the branch is
@@ -503,8 +495,7 @@ and treat_case ~check env sigma ci lbrty lf acc' =
         let head = strip_outer_cast head in
         if isMeta head then begin
           assert (args = Context.Rel.to_extended_vect mkRel 0 ctx);
-          let head' = lift (-n) head in
-          let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head' in
+          let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head in
           let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in
           (r,s,fi'::bacc)
         end
@@ -513,7 +504,7 @@ and treat_case ~check env sigma ci lbrty lf acc' =
           let sigma, t'ty = goal_type_of ~check env sigma fi in
           let sigma = check_conv_leq_goal ~check env sigma fi t'ty ty in
           (lacc,sigma,fi::bacc))
-    (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
+    (acc',sigma,[]) lbrty lf ci.ci_cstr_ndecls
 
 let convert_hyp ~check ~reorder env sigma d =
   let id = NamedDecl.get_id d in
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 31873ea6b0..39959d6fb8 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 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 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/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/closed/bug_3166.v
index baf87631f0..3b3375fdd8 100644
--- a/test-suite/bugs/opened/bug_3166.v
+++ b/test-suite/bugs/closed/bug_3166.v
@@ -80,5 +80,5 @@ Goal forall T (x y : T) (p : x = y), True.
         ) as H0.
   compute in H0.
   change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
-  Fail pose proof (fun k => @eq_trans _ _ _ k H0).
+  pose proof (fun k => @eq_trans _ _ _ k H0).
 Abort.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 984ac4e527..6fd4d37ab4 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -50,10 +50,11 @@ f =
 fun H : B =>
 match H with
 | AC x =>
-    let b0 := b in
-    (if b0 as b return (P b -> True)
-     then fun _ : P true => Logic.I
-     else fun _ : P false => Logic.I) x
+    (fun x0 : P b =>
+     let b0 := b in
+     (if b0 as b return (P b -> True)
+      then fun _ : P true => Logic.I
+      else fun _ : P false => Logic.I) x0) x
 end
      : B -> True
 The command has indeed failed with message:
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 4cc9d99c64..72cac900cd 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -24,7 +24,7 @@ Ltac2 Type case.
 
 Ltac2 Type case_invert := [
 | NoInvert
-| CaseInvert (instance,constr array)
+| CaseInvert (constr array)
 ].
 
 Ltac2 Type kind := [
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 8663691c0a..64a2b24404 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -109,15 +109,14 @@ let to_rec_declaration (nas, cs) =
 
 let of_case_invert = let open Constr in function
   | NoInvert -> ValInt 0
-  | CaseInvert {univs;args} ->
-    v_blk 0 [|of_instance univs; of_array of_constr args|]
+  | CaseInvert {indices} ->
+    v_blk 0 [|of_array of_constr indices|]
 
 let to_case_invert = let open Constr in function
   | ValInt 0 -> NoInvert
-  | ValBlk (0, [|univs;args|]) ->
-    let univs = to_instance univs in
-    let args = to_array to_constr args in
-    CaseInvert {univs;args}
+  | ValBlk (0, [|indices|]) ->
+    let indices = to_array to_constr indices in
+    CaseInvert {indices}
   | _ -> CErrors.anomaly Pp.(str "unexpected value shape")
 
 let of_result f = function
@@ -378,6 +377,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 +434,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 +474,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 +533,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