Change the representation of kernel case.

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

23 files changed, 281 insertions, 157 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d2859b1b4e..6370bd4f9a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1165,17 +1165,16 @@ let rec ungeneralize sigma n ng body =
   | LetIn (na,b,t,c) ->
       (* We traverse an alias *)
       mkLetIn (na,b,t,ungeneralize sigma (n+1) ng c)
-  | Case (ci,p,iv,c,brs) ->
+  | Case (ci,u,pms,p,iv,c,brs) ->
       (* We traverse a split *)
       let p =
-        let sign,p = decompose_lam_assum sigma p in
+        let (nas, p) = p in
         let sign2,p = decompose_prod_n_assum sigma ng p in
-        let p = prod_applist sigma p [mkRel (n+List.length sign+ng)] in
-        it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in
-      mkCase (ci,p,iv,c,Array.map2 (fun q c ->
-        let sign,b = decompose_lam_n_decls sigma q c in
-        it_mkLambda_or_LetIn (ungeneralize sigma (n+q) ng b) sign)
-        ci.ci_cstr_ndecls brs)
+        let p = prod_applist sigma p [mkRel (n+Array.length nas+ng)] in
+        nas, it_mkProd_or_LetIn p sign2
+      in
+      let map (nas, br) = nas, ungeneralize sigma (n + Array.length nas) ng br in
+      mkCase (ci, u, pms, p, iv, c, Array.map map brs)
   | App (f,args) ->
       (* We traverse an inner generalization *)
       assert (isCase sigma f);
@@ -1195,12 +1194,9 @@ let rec is_dependent_generalization sigma ng body =
   | LetIn (na,b,t,c) ->
       (* We traverse an alias *)
       is_dependent_generalization sigma ng c
-  | Case (ci,p,iv,c,brs) ->
+  | Case (ci,u,pms,p,iv,c,brs) ->
       (* We traverse a split *)
-      Array.exists2 (fun q c ->
-        let _,b = decompose_lam_n_decls sigma q c in
-        is_dependent_generalization sigma ng b)
-        ci.ci_cstr_ndecls brs
+      Array.exists (fun (_, b) -> is_dependent_generalization sigma ng b) brs
   | App (g,args) ->
       (* We traverse an inner generalization *)
       assert (isCase sigma g);
@@ -1759,7 +1755,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
     let good = List.filter (fun (_,u,_) -> is_conv_leq !!env sigma t u) subst in
     match good with
     | [] ->
-      map_constr_with_full_binders sigma (push_binder sigma) aux x t
+      map_constr_with_full_binders !!env sigma (push_binder sigma) aux x t
     | (_, _, u) :: _ -> (* u is in extenv *)
       let vl = List.map pi1 good in
       let ty =
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index bada2c3a60..7930c3d634 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -76,8 +76,7 @@ type cbv_value =
 and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
-  | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert
-            * case_info * cbv_value subs * cbv_stack
+  | CASE of Univ.Instance.t * constr array * case_return * case_branch array * Constr.case_invert * case_info * cbv_value subs * cbv_stack
   | PROJ of Projection.t * cbv_stack
 
 (* les vars pourraient etre des constr,
@@ -143,7 +142,7 @@ let rec stack_concat stk1 stk2 =
   match stk1 with
       TOP -> stk2
     | APP(v,stk1') -> APP(v,stack_concat stk1' stk2)
-    | CASE(c,b,iv,i,s,stk1') -> CASE(c,b,iv,i,s,stack_concat stk1' stk2)
+    | CASE(u,pms,c,b,iv,i,s,stk1') -> CASE(u,pms,c,b,iv,i,s,stack_concat stk1' stk2)
     | PROJ (p,stk1') -> PROJ (p,stack_concat stk1' stk2)
 
 (* merge stacks when there is no shifts in between *)
@@ -357,9 +356,9 @@ let rec reify_stack t = function
   | TOP -> t
   | APP (args,st) ->
       reify_stack (mkApp(t,Array.map reify_value args)) st
-  | CASE (ty,br,iv,ci,env,st) ->
+  | CASE (u,pms,ty,br,iv,ci,env,st) ->
       reify_stack
-        (mkCase (ci, ty, iv, t, br))
+        (mkCase (ci, u, pms, ty, iv, t,br))
         st
   | PROJ (p, st) ->
        reify_stack (mkProj (p, t)) st
@@ -410,6 +409,29 @@ let rec subs_consn v i n s =
   if Int.equal i n then s
   else subs_consn v (i + 1) n (subs_cons v.(i) s)
 
+(* TODO: share the common parts with EConstr *)
+let expand_branch env u pms (ind, i) br =
+  let open Declarations in
+  let nas, _br = br.(i - 1) in
+  let (mib, mip) = Inductive.lookup_mind_specif env ind in
+  let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list pms) in
+  let subst = paramsubst @ Inductive.ind_subst (fst ind) mib u in
+  let (ctx, _) = mip.mind_nf_lc.(i - 1) in
+  let (ctx, _) = List.chop mip.mind_consnrealdecls.(i - 1) ctx in
+  Inductive.instantiate_context u subst nas ctx
+
+let cbv_subst_of_rel_context_instance mkclos sign args env =
+  let rec aux subst sign l =
+    let open Context.Rel.Declaration in
+    match sign, l with
+    | LocalAssum _ :: sign', a::args' -> aux (subs_cons a subst) sign' args'
+    | LocalDef (_,c,_)::sign', args' ->
+        aux (subs_cons (mkclos subst c) subst) sign' args'
+    | [], [] -> subst
+    | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.")
+  in aux env (List.rev sign) (Array.to_list args)
+
 (* The main recursive functions
  *
  * Go under applications and cases/projections (pushed in the stack),
@@ -429,7 +451,7 @@ let rec norm_head info env t stack =
                         they could be computed when getting out of the stack *)
       let nargs = Array.map (cbv_stack_term info TOP env) args in
       norm_head info env head (stack_app nargs stack)
-  | Case (ci,p,iv,c,v) -> norm_head info env c (CASE(p,v,iv,ci,env,stack))
+  | Case (ci,u,pms,p,iv,c,v) -> norm_head info env c (CASE(u,pms,p,v,iv,ci,env,stack))
   | Cast (ct,_,_) -> norm_head info env ct stack
 
   | Proj (p, c) ->
@@ -557,16 +579,33 @@ and cbv_stack_value info env = function
         cbv_stack_term info stk envf redfix
 
     (* constructor in a Case -> IOTA *)
-    | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,iv,ci,env,stk)))
+    | (CONSTR(((sp,n),_),[||]), APP(args,CASE(u,pms,_p,br,iv,ci,env,stk)))
             when red_set info.reds fMATCH ->
+        let nargs = Array.length args - ci.ci_npar in
         let cargs =
-          Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
-        cbv_stack_term info (stack_app cargs stk) env br.(n-1)
+          Array.sub args ci.ci_npar nargs in
+        let env =
+          if (Int.equal ci.ci_cstr_ndecls.(n - 1) ci.ci_cstr_nargs.(n - 1)) then (* no lets *)
+            subs_consn cargs 0 nargs env
+          else
+            let mkclos env c = cbv_stack_term info TOP env c in
+            let ctx = expand_branch info.env u pms (sp, n) br in
+            cbv_subst_of_rel_context_instance mkclos ctx cargs env
+        in
+        cbv_stack_term info stk env (snd br.(n-1))
 
     (* constructor of arity 0 in a Case -> IOTA *)
-    | (CONSTR(((_,n),u),[||]), CASE(_,br,_,_,env,stk))
+    | (CONSTR(((sp, n), _),[||]), CASE(u,pms,_,br,_,ci,env,stk))
             when red_set info.reds fMATCH ->
-                    cbv_stack_term info stk env br.(n-1)
+        let env =
+          if (Int.equal ci.ci_cstr_ndecls.(n - 1) ci.ci_cstr_nargs.(n - 1)) then (* no lets *)
+            env
+          else
+            let mkclos env c = cbv_stack_term info TOP env c in
+            let ctx = expand_branch info.env u pms (sp, n) br in
+            cbv_subst_of_rel_context_instance mkclos ctx [||] env
+        in
+        cbv_stack_term info stk env (snd br.(n-1))
 
     (* constructor in a Projection -> IOTA *)
     | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk)))
@@ -640,10 +679,31 @@ let rec apply_stack info t = function
   | TOP -> t
   | APP (args,st) ->
       apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st
-  | CASE (ty,br,iv,ci,env,st) ->
+  | CASE (u,pms,ty,br,iv,ci,env,st) ->
+    (* FIXME: Prevent this expansion by caching whether an inductive contains let-bindings *)
+    let (_, ty, _, _, br) = Inductive.expand_case info.env (ci, u, pms, ty, iv, mkProp, br) in
+    let ty =
+      let (_, mip) = Inductive.lookup_mind_specif info.env ci.ci_ind in
+      Term.decompose_lam_n_decls (mip.Declarations.mind_nrealdecls + 1) ty
+    in
+    let mk_br c n = Term.decompose_lam_n_decls n c in
+    let br = Array.map2 mk_br br ci.ci_cstr_ndecls in
+    let map_ctx (nas, c) =
+      let open Context.Rel.Declaration in
+      let fold decl e = match decl with
+      | LocalAssum _ -> subs_lift e
+      | LocalDef (_, b, _) ->
+        let b = cbv_stack_term info TOP e b in
+        (* The let-binding persists, so we have to shift *)
+        subs_shft (1, subs_cons b e)
+      in
+      let env = List.fold_right fold nas env in
+      let nas = Array.of_list (List.rev_map get_annot nas) in
+      (nas, cbv_norm_term info env c)
+    in
       apply_stack info
-        (mkCase (ci, cbv_norm_term info env ty, iv, t,
-                    Array.map (cbv_norm_term info env) br))
+        (mkCase (ci, u, Array.map (cbv_norm_term info env) pms, map_ctx ty, iv, t,
+                    Array.map map_ctx br))
         st
   | PROJ (p, st) ->
        apply_stack info (mkProj (p, t)) st
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 409f4c0f70..4d81678200 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -42,8 +42,7 @@ type cbv_value =
 and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
-  | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert
-            * case_info * cbv_value subs * cbv_stack
+  | CASE of Univ.Instance.t * constr array * case_return * case_branch array * Constr.case_invert * case_info * cbv_value subs * cbv_stack
   | PROJ of Projection.t * cbv_stack
 
 val shift_value : int -> cbv_value -> cbv_value
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 0e69b814c7..c77feeafbb 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -351,7 +351,9 @@ let matches_core env sigma allow_bound_rels
           sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
-      | PIf (a1,b1,b1'), Case (ci,_,_,a2,[|b2;b2'|]) ->
+      | PIf (a1,b1,b1'), Case (ci, u2, pms2, p2, iv, a2, ([|b2;b2'|] as br2)) ->
+          let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in
+          let b2, b2' = match br2 with [|b2; b2'|] -> b2, b2' | _ -> assert false in
           let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in
           let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in
           let n = Context.Rel.length ctx_b2 in
@@ -367,7 +369,8 @@ let matches_core env sigma allow_bound_rels
           else
             raise PatternMatchingFailure
 
-      | PCase (ci1,p1,a1,br1), Case (ci2,p2,_,a2,br2) ->
+      | PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) ->
+          let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
           let n2 = Array.length br2 in
           let () = match ci1.cip_ind with
           | None -> ()
@@ -504,12 +507,30 @@ let sub_match ?(closed=true) env sigma pat c =
        | [app';c] -> mk_ctx (mkApp (app',[|c|]))
        | _ -> assert false in
      try_aux [(env, app); (env, Array.last lc)] mk_ctx next
-  | Case (ci,hd,iv,c1,lc) ->
+  | Case (ci,u,pms,hd0,iv,c1,lc0) ->
+      let (mib, mip) = Inductive.lookup_mind_specif env ci.ci_ind in
+      let (_, hd, _, _, br) = expand_case env sigma (ci, u, pms, hd0, iv, c1, lc0) in
+      let hd =
+        let (ctx, hd) = decompose_lam_assum sigma hd in
+        (push_rel_context ctx env, hd)
+      in
+      let map i br =
+        let decls = mip.Declarations.mind_consnrealdecls.(i) in
+        let (ctx, c) = decompose_lam_n_decls sigma decls br in
+        (push_rel_context ctx env, c)
+      in
+      let lc = Array.to_list (Array.mapi map br) in
       let next_mk_ctx = function
-      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,iv,c1,Array.of_list lc))
+      | c1 :: rem ->
+        let pms, rem = List.chop (Array.length pms) rem in
+        let pms = Array.of_list pms in
+        let hd, lc = match rem with [] -> assert false | x :: l -> (x, l) in
+        let hd = (fst hd0, hd) in
+        let map_br (nas, _) br = (nas, br) in
+        mk_ctx (mkCase (ci,u,pms,hd,iv,c1,Array.map2 map_br lc0 (Array.of_list lc)))
       | _ -> assert false
       in
-      let sub = (env, c1) :: (env, hd) :: subargs env lc in
+      let sub = (env, c1) :: Array.fold_right (fun c accu -> (env, c) :: accu) pms (hd :: lc) in
       try_aux sub next_mk_ctx next
   | Fix (indx,(names,types,bodies as recdefs)) ->
     let nb_fix = Array.length types in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 402a6f6ed3..27b193f144 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -241,16 +241,9 @@ let print_primproj_params =
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)
 
-let computable sigma p k =
+let computable sigma (nas, ccl) =
     (* We first remove as many lambda as the arity, then we look
-       if it remains a lambda for a dependent elimination. This function
-       works for normal eta-expanded term. For non eta-expanded or
-       non-normal terms, it may affirm the pred is synthetisable
-       because of an undetected ultimate dependent variable in the second
-       clause, or else, it may affirm the pred non synthetisable
-       because of a non normal term in the fourth clause.
-       A solution could be to store, in the MutCase, the eta-expanded
-       normal form of pred to decide if it depends on its variables
+       if it remains a lambda for a dependent elimination.
 
        Lorsque le prédicat est dépendant de manière certaine, on
        ne déclare pas le prédicat synthétisable (même si la
@@ -258,10 +251,7 @@ let computable sigma p k =
        sinon on perd la réciprocité de la synthèse (qui, lui,
        engendrera un prédicat non dépendant) *)
 
-  let sign,ccl = decompose_lam_assum sigma p in
-  Int.equal (Context.Rel.length sign) (k + 1)
-  &&
-  noccur_between sigma 1 (k+1) ccl
+  noccur_between sigma 1 (Array.length nas) ccl
 
 let lookup_name_as_displayed env sigma t s =
   let rec lookup avoid n c = match EConstr.kind sigma c with
@@ -429,11 +419,12 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
   | [] -> [Id.Set.empty,[],rhs]
   | na::nal ->
     match EConstr.kind sigma c with
-    | Case (ci,p,iv,c,cl) when
+    | Case (ci,u,pms,p,iv,c,cl) when
         eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e))))
         && not (Int.equal (Array.length cl) 0)
         && (* don't contract if p dependent *)
-        computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
+        computable sigma p (* FIXME: can do better *) ->
+        let (ci, _, _, _, cl) = EConstr.expand_case (snd (snd e)) sigma (ci, u, pms, p, iv, c, cl) in
         let clauses = build_tree na isgoal e sigma ci cl in
         List.flatten
           (List.map (fun (ids,pat,rhs) ->
@@ -788,8 +779,9 @@ and detype_r d flags avoid env sigma t =
         GRef (GlobRef.IndRef ind_sp, detype_instance sigma u)
     | Construct (cstr_sp,u) ->
         GRef (GlobRef.ConstructRef cstr_sp, detype_instance sigma u)
-    | Case (ci,p,iv,c,bl) ->
-        let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
+    | Case (ci,u,pms,p,iv,c,bl) ->
+        let comp = computable sigma p in
+        let (ci, p, iv, c, bl) = EConstr.expand_case (snd env) sigma (ci, u, pms, p, iv, c, bl) in
         detype_case comp (detype d flags avoid env sigma)
           (detype_eqns d flags avoid env sigma ci comp)
           (is_nondep_branch sigma) avoid
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4b0974ae03..990e84e5a7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -206,7 +206,7 @@ let occur_rigidly flags env evd (evk,_) t =
       if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true
       else Reducible
     | Rel _ | Var _ -> Reducible
-    | Case (_,_,_,c,_) ->
+    | Case (_,_,_,_,_,c,_) ->
       (match aux c with
       | Rigid b -> Rigid b
       | _ -> Reducible)
@@ -381,7 +381,10 @@ let rec ise_stack2 no_app env evd f sk1 sk2 =
       else None, x in
     match revsk1, revsk2 with
     | [], [] -> None, Success i
-    | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
+    | Stack.Case (ci1,u1,pms1,t1,iv1,c1)::q1, Stack.Case (ci2,u2,pms2,t2,iv2,c2)::q2 ->
+      let dummy = mkProp in
+      let (_, t1, _, _, c1) = EConstr.expand_case env evd (ci1,u1,pms1,t1,iv1,dummy,c1) in
+      let (_, t2, _, _, c2) = EConstr.expand_case env evd (ci2,u2,pms2,t2,iv2,dummy,c2) in
       begin
         match ise_and i [
           (fun i -> f env i CONV t1 t2);
@@ -418,7 +421,10 @@ let rec exact_ise_stack2 env evd f sk1 sk2 =
   let rec ise_rev_stack2 i revsk1 revsk2 =
     match revsk1, revsk2 with
     | [], [] -> Success i
-    | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
+    | Stack.Case (ci1,u1,pms1,t1,iv1,c1)::q1, Stack.Case (ci2,u2,pms2,t2,iv2,c2)::q2 ->
+      let dummy = mkProp in
+      let (_, t1, _, _, c1) = EConstr.expand_case env evd (ci1,u1,pms1,t1,iv1,dummy,c1) in
+      let (_, t2, _, _, c2) = EConstr.expand_case env evd (ci2,u2,pms2,t2,iv2,dummy,c2) in
       ise_and i [
       (fun i -> ise_rev_stack2 i q1 q2);
       (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);
@@ -1278,7 +1284,7 @@ let apply_on_subterm env evd fixed f test c t =
     if occur_evars !evdref !fixedref t then
       match EConstr.kind !evdref t with
       | Evar (ev, args) when Evar.Set.mem ev !fixedref -> t
-      | _ -> map_constr_with_binders_left_to_right !evdref
+      | _ -> map_constr_with_binders_left_to_right env !evdref
               (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
               applyrec acc t
     else
@@ -1293,7 +1299,7 @@ let apply_on_subterm env evd fixed f test c t =
                 evdref := evd'; t')
      else (
        if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed");
-       map_constr_with_binders_left_to_right !evdref
+       map_constr_with_binders_left_to_right env !evdref
         (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
         applyrec acc t))
   in
@@ -1383,7 +1389,7 @@ let thin_evars env sigma sign c =
        if not (Id.Set.mem id ctx) then raise (TypingFailed !sigma)
        else t
     | _ ->
-       map_constr_with_binders_left_to_right !sigma
+       map_constr_with_binders_left_to_right env !sigma
         (fun d (env,acc) -> (push_rel d env, acc+1))
         applyrec (env,acc) t
   in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f9f6f74a66..cb3eef9df0 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -232,7 +232,7 @@ let recheck_applications unify flags env evdref t =
        else ()
      in aux 0 fty
     | _ ->
-       iter_with_full_binders !evdref (fun d env -> push_rel d env) aux env t
+       iter_with_full_binders env !evdref (fun d env -> push_rel d env) aux env t
   in aux env t
 
 
@@ -304,7 +304,7 @@ let noccur_evar env evd evk c =
         | LocalAssum _ -> ()
         | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (EConstr.of_constr b)))
   | Proj (p,c) -> occur_rec true acc c
-  | _ -> iter_with_full_binders evd (fun rd (k,env) -> (succ k, push_rel rd env))
+  | _ -> iter_with_full_binders env evd (fun rd (k,env) -> (succ k, push_rel rd env))
     (occur_rec check_types) acc c
   in
   try occur_rec false (0,env) c; true with Occur -> false
@@ -490,14 +490,14 @@ let expansion_of_var sigma aliases x =
   | Some a, _ -> (true, Alias.repr sigma a)
   | None, a :: _ -> (true, Some a)
 
-let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t with
+let rec expand_vars_in_term_using env sigma aliases t = match EConstr.kind sigma t with
   | Rel n -> of_alias (normalize_alias sigma aliases (RelAlias n))
   | Var id -> of_alias (normalize_alias sigma aliases (VarAlias id))
   | _ ->
-    let self aliases c = expand_vars_in_term_using sigma aliases c in
-    map_constr_with_full_binders sigma (extend_alias sigma) self aliases t
+    let self aliases c = expand_vars_in_term_using env sigma aliases c in
+    map_constr_with_full_binders env sigma (extend_alias sigma) self aliases t
 
-let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env sigma)
+let expand_vars_in_term env sigma = expand_vars_in_term_using env sigma (make_alias_map env sigma)
 
 let free_vars_and_rels_up_alias_expansion env sigma aliases c =
   let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
@@ -533,7 +533,7 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c =
     | Const _ | Ind _ | Construct _ ->
         acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2
     | _ ->
-        iter_with_full_binders sigma
+        iter_with_full_binders env sigma
           (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
           frec (aliases,depth) c
   in
@@ -1645,7 +1645,7 @@ let rec invert_definition unify flags choose imitate_defs
             let candidates =
               try
                 let t =
-                  map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+                  map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1)
                     imitate envk t in
                 (* Less dependent solutions come last *)
                 l@[t]
@@ -1659,7 +1659,7 @@ let rec invert_definition unify flags choose imitate_defs
               evar'')
         | None ->
            (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
-          map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
+          map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1)
                                         imitate envk t
   in
   let rhs = whd_beta env evd rhs (* heuristic *) in
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 52e3364109..9f84b7683f 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -73,7 +73,7 @@ type 'a testing_function = {
    (b,l), b=true means no occurrence except the ones in l and b=false,
    means all occurrences except the ones in l *)
 
-let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
+let replace_term_occ_gen_modulo env sigma occs like_first test bywhat cl occ t =
   let count = ref (Locusops.initialize_occurrence_counter occs) in
   let nested = ref false in
   let add_subst pos t subst =
@@ -107,23 +107,23 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
     with NotUnifiable _ ->
       subst_below k t
   and subst_below k t =
-    map_constr_with_binders_left_to_right sigma (fun d k -> k+1) substrec k t
+    map_constr_with_binders_left_to_right env sigma (fun d k -> k+1) substrec k t
   in
   let t' = substrec 0 t in
   (!count, t')
 
-let replace_term_occ_modulo evd occs test bywhat t =
+let replace_term_occ_modulo env evd occs test bywhat t =
   let occs',like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
   proceed_with_occurrences
-    (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t
+    (replace_term_occ_gen_modulo env evd occs' like_first test bywhat None) occs' t
 
-let replace_term_occ_decl_modulo evd occs test bywhat d =
+let replace_term_occ_decl_modulo env evd occs test bywhat d =
   let (plocs,hyploc),like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (replace_term_occ_gen_modulo evd plocs like_first test bywhat)
+       (replace_term_occ_gen_modulo env evd plocs like_first test bywhat)
        hyploc)
     plocs d
 
@@ -145,7 +145,7 @@ let make_eq_univs_test env evd c =
 let subst_closed_term_occ env evd occs c t =
   let test = make_eq_univs_test env evd c in
   let bywhat () = mkRel 1 in
-  let t' = replace_term_occ_modulo evd occs test bywhat t in
+  let t' = replace_term_occ_modulo env evd occs test bywhat t in
     t', test.testing_state
 
 let subst_closed_term_occ_decl env evd occs c d =
@@ -155,6 +155,6 @@ let subst_closed_term_occ_decl env evd occs c d =
   let bywhat () = mkRel 1 in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (fun _ -> replace_term_occ_gen_modulo evd plocs like_first test bywhat None)
+       (fun _ -> replace_term_occ_gen_modulo env evd plocs like_first test bywhat None)
        hyploc) plocs d,
   test.testing_state
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 1ddae01e2b..c71cb207ab 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -43,13 +43,13 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
     matching subterms at the indicated occurrences [occl] with [mk
     ()]; it turns a NotUnifiable exception raised by the testing
     function into a SubtermUnificationError. *)
-val replace_term_occ_modulo : evar_map -> occurrences or_like_first ->
+val replace_term_occ_modulo : env -> evar_map -> occurrences or_like_first ->
   'a testing_function -> (unit -> constr) -> constr -> constr
 
 (** [replace_term_occ_decl_modulo] is similar to
     [replace_term_occ_modulo] but for a named_declaration. *)
 val replace_term_occ_decl_modulo :
-  evar_map ->
+  env -> evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
   'a testing_function -> (unit -> constr) ->
   named_declaration -> named_declaration
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index a012f1cb15..f6e45613e1 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -76,7 +76,7 @@ and kind_of_head env t =
   | App (c,al) -> aux k (Array.to_list al @ l) c b
   | Proj (p,c) -> RigidHead RigidOther
 
-  | Case (_,_,_,c,_) -> aux k [] c true
+  | Case (_,_,_,_,_,c,_) -> aux k [] c true
   | Int _ | Float _ | Array _ -> ConstructorHead
   | Fix ((i,j),_) ->
       let n = i.(j) in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 5ffd919312..dd7cf8abaa 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -122,12 +122,24 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
         | None ->
           let iv = make_case_invert env (find_rectype env sigma (EConstr.of_constr (lift 1 depind))) ci in
           let iv = EConstr.Unsafe.to_case_invert iv in
-          mkCase (ci, lift ndepar p, iv, mkRel 1, Termops.rel_vect ndepar k)
+          let ncons = Array.length mip.mind_consnames in
+          let mk_branch i =
+            (* eta-expansion to please branch contraction *)
+            let ft = get_type (lookup_rel (ncons - i) env) in
+            (* we need that to get the generated names for the branch *)
+            let (ctx, _) = decompose_prod_assum ft in
+            let n = mkRel (List.length ctx + 1) in
+            let args = Context.Rel.to_extended_vect mkRel 0 ctx in
+            let br = it_mkLambda_or_LetIn (mkApp (n, args)) ctx in
+            lift (ndepar + ncons - i - 1) br
+          in
+          let br = Array.init ncons mk_branch in
+          mkCase (Inductive.contract_case env (ci, lift ndepar p,  iv, mkRel 1, br))
         | Some ps ->
           let term =
             mkApp (mkRel 2,
-                   Array.map
-                   (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
+                    Array.map
+                    (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
             if dep then
               let ty = mkApp (mkRel 3, [| mkRel 1 |]) in
                 mkCast (term, DEFAULTcast, ty)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index bd875cf68b..04feae35d8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -356,8 +356,7 @@ let make_case_or_project env sigma indt ci pred c branches =
   let IndType (((ind,_),_),_) = indt in
   let projs = get_projections env ind in
   match projs with
-  | None ->
-    mkCase (ci, pred, make_case_invert env indt ci, c, branches)
+  | None -> (mkCase (EConstr.contract_case env sigma (ci, pred, make_case_invert env indt ci, c, branches)))
   | Some ps ->
      assert(Array.length branches == 1);
      let na, ty, t = destLambda sigma pred in
@@ -749,6 +748,6 @@ let control_only_guard env sigma c =
   in
   let rec iter env c =
     check_fix_cofix env c;
-    EConstr.iter_with_full_binders sigma EConstr.push_rel iter env c
+    EConstr.iter_with_full_binders env sigma EConstr.push_rel iter env c
   in
   iter env c
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 3705d39280..8e83814fa0 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -213,7 +213,7 @@ val make_case_or_project :
   (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
 
 val make_case_invert : env -> inductive_type -> case_info
-  -> (EConstr.constr,EConstr.EInstance.t) case_invert
+  -> EConstr.case_invert
 
 (*i Compatibility
 val make_default_case_info : env -> case_style -> inductive -> case_info
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index d06d6e01d1..8da615acfc 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -343,7 +343,8 @@ and nf_atom_type env sigma atom =
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type p realargs a in
-      mkCase(ans.asw_ci, p, iv, a, branchs), tcase
+      let ci = ans.asw_ci in
+      mkCase (Inductive.contract_case env (ci, p, iv, a, branchs)), tcase
   | Afix(tt,ft,rp,s) ->
       let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in
       let tt = Array.map fst tt and rt = Array.map snd tt in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b259945d9e..47097a0e32 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -202,7 +202,8 @@ let pattern_of_constr env sigma t =
       | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
       | _ ->
         PMeta None)
-    | Case (ci,p,_,a,br) ->
+    | Case (ci, u, pms, p, iv, a, br) ->
+        let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p, iv, a, br) in
         let cip =
           { cip_style = ci.ci_pp_info.style;
             cip_ind = Some ci.ci_ind;
@@ -213,7 +214,7 @@ let pattern_of_constr env sigma t =
           (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c)
         in
         PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
-               Array.to_list (Array.mapi branch_of_constr br))
+                Array.to_list (Array.mapi branch_of_constr br))
     | Fix (lni,(lna,tl,bl)) ->
        let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
        let env' = Array.fold_left2 push env lna tl in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9dbded75ba..e86a8a28c9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1043,7 +1043,7 @@ struct
       if not record then
         let f = it_mkLambda_or_LetIn f fsign in
         let ci = make_case_info !!env (ind_of_ind_type indt) rci LetStyle in
-          mkCase (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|])
+          mkCase (EConstr.contract_case !!env sigma (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|]))
       else it_mkLambda_or_LetIn f fsign
     in
     (* Make dependencies from arity signature impossible *)
@@ -1159,7 +1159,7 @@ struct
         let pred = nf_evar sigma pred in
         let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val pred in
         let ci = make_case_info !!env (fst ind) rci IfStyle in
-          mkCase (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|])
+        mkCase (EConstr.contract_case !!env sigma (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|]))
       in
       let cj = { uj_val = v; uj_type = p } in
       discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 52f60fbc5e..85214eb245 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -177,9 +177,12 @@ sig
   type 'a app_node
   val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
+  type 'a case_stk =
+    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
+  | Case of 'a case_stk
   | Proj of Projection.t
   | Fix of ('a, 'a) pfixpoint * 'a t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
@@ -230,9 +233,12 @@ struct
                      )
 
 
+  type 'a case_stk =
+    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
+  | Case of 'a case_stk
   | Proj of Projection.t
   | Fix of ('a, 'a) pfixpoint * 'a t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
@@ -245,9 +251,9 @@ struct
     let pr_c x = hov 1 (pr_c x) in
     match member with
     | App app -> str "ZApp" ++ pr_app_node pr_c app
-    | Case (_,_,_,br) ->
+    | Case (_,_,_,_,_,br) ->
        str "ZCase(" ++
-         prvect_with_sep (pr_bar) pr_c br
+         prvect_with_sep (pr_bar) (fun (_, c) -> pr_c c) br
        ++ str ")"
     | Proj p  ->
       str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
@@ -284,7 +290,7 @@ struct
         ([],[]) -> Int.equal bal 0
       | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2
       | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2
-      | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) ->
+      | (Case _ :: s1, Case _::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
       | (Proj (p)::s1, Proj(p2)::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
@@ -304,8 +310,9 @@ struct
         let t1,l1 = decomp_node_last n1 q1 in
         let t2,l2 = decomp_node_last n2 q2 in
         aux (f o t1 t2) l1 l2
-      | Case (_,t1,_,a1) :: q1, Case (_,t2,_,a2) :: q2 ->
-        aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2
+      | Case ((_,_,pms1,(_, t1),_,a1)) :: q1, Case ((_,_,pms2, (_, t2),_,a2)) :: q2 ->
+        let f' o (_, t1) (_, t2) = f o t1 t2 in
+        aux (Array.fold_left2 f' (f (Array.fold_left2 f o pms1 pms2) t1 t2) a1 a2) q1 q2
       | Proj (p1) :: q1, Proj (p2) :: q2 ->
         aux o q1 q2
       | Fix ((_,(_,a1,b1)),s1) :: q1, Fix ((_,(_,a2,b2)),s2) :: q2 ->
@@ -320,8 +327,8 @@ struct
                                | App (i,a,j) ->
                                   let le = j - i + 1 in
                                   App (0,Array.map f (Array.sub a i le), le-1)
-                               | Case (info,ty,iv,br) ->
-                                 Case (info, f ty, map_invert f iv, Array.map f br)
+                               | Case (info,u,pms,ty,iv,br) ->
+                                  Case (info, u, Array.map f pms, on_snd f ty, iv, Array.map (on_snd f) br)
                                | Fix ((r,(na,ty,bo)),arg) ->
                                   Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg)
                                | Primitive (p,c,args,kargs) ->
@@ -408,7 +415,7 @@ struct
                 then a
                 else Array.sub a i (j - i + 1) in
        zip (mkApp (f, a'), s)
-    | f, (Case (ci,rt,iv,br)::s) -> zip (mkCase (ci,rt,iv,f,br), s)
+    | f, (Case (ci,u,pms,rt,iv,br)::s) -> zip (mkCase (ci,u,pms,rt,iv,f,br), s)
   | f, (Fix (fix,st)::s) -> zip
     (mkFix fix, st @ (append_app [|f|] s))
   | f, (Proj (p)::s) -> zip (mkProj (p,f),s)
@@ -469,13 +476,13 @@ let strong_with_flags whdfun flags env sigma t =
       | d -> d in
     push_rel d env in
   let rec strongrec env t =
-    map_constr_with_full_binders sigma
+    map_constr_with_full_binders env sigma
       push_rel_check_zeta strongrec env (whdfun flags env sigma t) in
   strongrec env t
 
 let strong whdfun env sigma t =
   let rec strongrec env t =
-    map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in
+    map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in
   strongrec env t
 
 (*************************************)
@@ -702,6 +709,20 @@ let debug_RAKAM =
     ~key:["Debug";"RAKAM"]
     ~value:false
 
+let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
+  let args = Stack.tail ci.ci_npar args in
+  let args = Option.get (Stack.list_of_app_stack args) in
+  let br = lf.(i - 1) in
+  let subst =
+    if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then
+      (* No let-bindings *)
+      List.rev args
+    else
+      let ctx = expand_branch env sigma u pms (ind, i) br in
+      subst_of_rel_context_instance ctx args
+  in
+  Vars.substl subst (snd br)
+
 let rec whd_state_gen flags env sigma =
   let open Context.Named.Declaration in
   let rec whrec (x, stack) : state =
@@ -785,8 +806,8 @@ let rec whd_state_gen flags env sigma =
         | _ -> fold ())
       | _ -> fold ())
 
-    | Case (ci,p,iv,d,lf) ->
-      whrec (d, Stack.Case (ci,p,iv,lf) :: stack)
+    | Case (ci,u,pms,p,iv,d,lf) ->
+      whrec (d, Stack.Case (ci,u,pms,p,iv,lf) :: stack)
 
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
@@ -794,13 +815,14 @@ let rec whd_state_gen flags env sigma =
       |Some (bef,arg,s') ->
         whrec (arg, Stack.Fix(f,bef)::s'))
 
-    | Construct ((ind,c),u) ->
+    | Construct (cstr ,u) ->
       let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
       let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(ci, _, _, lf)::s') when use_match ->
-          whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+        |args, (Stack.Case case::s') when use_match ->
+          let r = apply_branch env sigma cstr args case in
+          whrec (r, s')
         |args, (Stack.Proj (p)::s') when use_match ->
           whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
         |args, (Stack.Fix (f,s')::s'') when use_fix ->
@@ -850,7 +872,7 @@ let rec whd_state_gen flags env sigma =
   whrec
 
 (** reduction machine without global env and refold machinery *)
-let local_whd_state_gen flags _env sigma =
+let local_whd_state_gen flags env sigma =
   let rec whrec (x, stack) =
     let c0 = EConstr.kind sigma x in
     let s = (EConstr.of_kind c0, stack) in
@@ -882,8 +904,8 @@ let local_whd_state_gen flags _env sigma =
     | Proj (p,c) when CClosure.RedFlags.red_projection flags p ->
       (whrec (c, Stack.Proj (p) :: stack))
 
-    | Case (ci,p,iv,d,lf) ->
-      whrec (d, Stack.Case (ci,p,iv,lf) :: stack)
+    | Case (ci,u,pms,p,iv,d,lf) ->
+      whrec (d, Stack.Case (ci,u,pms,p,iv,lf) :: stack)
 
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
@@ -896,13 +918,14 @@ let local_whd_state_gen flags _env sigma =
         Some c -> whrec (c,stack)
       | None -> s)
 
-    | Construct ((ind,c),u) ->
+    | Construct (cstr, u) ->
       let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
       let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(ci, _, _, lf)::s') when use_match ->
-          whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+        |args, (Stack.Case case :: s') when use_match ->
+          let r = apply_branch env sigma cstr args case in
+          whrec (r, s')
         |args, (Stack.Proj (p) :: s') when use_match ->
           whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
         |args, (Stack.Fix (f,s')::s'') when use_fix ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ae93eb48b4..e60def72f6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -57,9 +57,12 @@ module Stack : sig
 
   val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
+  type 'a case_stk =
+    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
+  | Case of 'a case_stk
   | Proj of Projection.t
   | Fix of ('a, 'a) pfixpoint * 'a t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 34bcd0982c..064990f6bf 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -129,7 +129,8 @@ let retype ?(polyprop=true) sigma =
     | Evar ev -> existential_type sigma ev
     | Ind (ind, u) -> EConstr.of_constr (rename_type_of_inductive env (ind, EInstance.kind sigma u))
     | Construct (cstr, u) -> EConstr.of_constr (rename_type_of_constructor env (cstr, EInstance.kind sigma u))
-    | Case (_,p,_iv,c,lf) ->
+    | Case (ci,u,pms,p,iv,c,lf) ->
+        let (_,p,iv,c,lf) = EConstr.expand_case env sigma (ci,u,pms,p,iv,c,lf) in
         let Inductiveops.IndType(indf,realargs) =
           let t = type_of env c in
           try Inductiveops.find_rectype env sigma t
@@ -309,7 +310,7 @@ let relevance_of_term env sigma c =
       | Const (c,_) -> Relevanceops.relevance_of_constant env c
       | Ind _ -> Sorts.Relevant
       | Construct (c,_) -> Relevanceops.relevance_of_constructor env c
-      | Case (ci, _, _, _, _) -> ci.ci_relevance
+      | Case (ci, _, _, _, _, _, _) -> ci.ci_relevance
       | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
       | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
       | Proj (p, _) -> Relevanceops.relevance_of_projection env p
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 411fb0cd89..01819a650b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -296,8 +296,8 @@ let compute_consteval_direct env sigma ref =
       | Fix fix when not onlyproj ->
           (try check_fix_reversibility sigma labs l fix
           with Elimconst -> NotAnElimination)
-      | Case (_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
-      | Case (_,_,_,d,_) -> srec env n labs true d
+      | Case (_,_,_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
+      | Case (_,_,_,_,_,d,_) -> srec env n labs true d
       | Proj (p, d) when isRel sigma d -> EliminationProj n
       | _ -> NotAnElimination
   in
@@ -478,29 +478,36 @@ let contract_cofix_use_function env sigma f
     sigma (nf_beta env sigma bodies.(bodynum))
 
 type 'a miota_args = {
-  mP      : constr;     (** the result type *)
+  mU      : EInstance.t; (* Universe instance of the return clause *)
+  mParams : constr array; (* Parameters of the inductive *)
+  mP      : case_return;     (* the result type *)
   mconstr : constr;     (** the constructor *)
   mci     : case_info;  (** special info to re-build pattern *)
   mcargs  : 'a list;    (** the constructor's arguments *)
-  mlf     : 'a array }  (** the branch code vector *)
+  mlf     : 'a pcase_branch array }  (** the branch code vector *)
 
-let reduce_mind_case sigma mia =
+let reduce_mind_case env sigma mia =
   match EConstr.kind sigma mia.mconstr with
-    | Construct ((ind_sp,i),u) ->
-(*      let ncargs = (fst mia.mci).(i-1) in*)
+    | Construct ((_, i as cstr), u) ->
         let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
-        applist (mia.mlf.(i-1),real_cargs)
+        let br = mia.mlf.(i - 1) in
+        let ctx = EConstr.expand_branch env sigma mia.mU mia.mParams cstr br in
+        let br = it_mkLambda_or_LetIn (snd br) ctx in
+        applist (br, real_cargs)
     | CoFix cofix ->
         let cofix_def = contract_cofix sigma cofix in
         (* XXX Is NoInvert OK here? *)
-        mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
+        mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
 let reduce_mind_case_use_function func env sigma mia =
   match EConstr.kind sigma mia.mconstr with
-    | Construct ((ind_sp,i),u) ->
+    | Construct ((_, i as cstr),u) ->
         let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
-        applist (mia.mlf.(i-1), real_cargs)
+        let br = mia.mlf.(i - 1) in
+        let ctx = EConstr.expand_branch env sigma mia.mU mia.mParams cstr br in
+        let br = it_mkLambda_or_LetIn (snd br) ctx in
+        applist (br, real_cargs)
     | CoFix (bodynum,(names,_,_) as cofix) ->
         let build_cofix_name =
           if isConst sigma func then
@@ -526,8 +533,7 @@ let reduce_mind_case_use_function func env sigma mia =
             fun _ -> None in
         let cofix_def =
           contract_cofix_use_function env sigma build_cofix_name cofix in
-        (* Is NoInvert OK here? *)
-        mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
+        mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
 
@@ -728,9 +734,9 @@ and whd_simpl_stack env sigma =
       | LetIn (n,b,t,c) -> redrec (Vars.substl [b] c, stack)
       | App (f,cl) -> assert false (* see push_app above *)
       | Cast (c,_,_) -> redrec (c, stack)
-      | Case (ci,p,iv,c,lf) ->
+      | Case (ci,u,pms,p,iv,c,lf) ->
           (try
-            redrec (special_red_case env sigma (ci,p,iv,c,lf), stack)
+            redrec (special_red_case env sigma (ci,u,pms,p,iv,c,lf), stack)
           with
               Redelimination -> s')
       | Fix fix ->
@@ -842,15 +848,15 @@ and reduce_proj env sigma c =
           let proj_narg = Projection.npars proj + Projection.arg proj in
           List.nth cargs proj_narg
         | _ -> raise Redelimination)
-    | Case (n,p,iv,c,brs) ->
+    | Case (n,u,pms,p,iv,c,brs) ->
       let c' = redrec c in
-      let p = (n,p,iv,c',brs) in
+      let p = (n,u,pms,p,iv,c',brs) in
         (try special_red_case env sigma p
          with Redelimination -> mkCase p)
     | _ -> raise Redelimination
   in redrec c
 
-and special_red_case env sigma (ci, p, iv, c, lf) =
+and special_red_case env sigma (ci, u, pms, p, iv, c, lf) =
   let rec redrec s =
     let (constr, cargs) = whd_simpl_stack env sigma s in
     match match_eval_ref env sigma constr cargs with
@@ -860,14 +866,14 @@ and special_red_case env sigma (ci, p, iv, c, lf) =
       | Some gvalue ->
         if reducible_mind_case sigma gvalue then
           reduce_mind_case_use_function constr env sigma
-          {mP=p; mconstr=gvalue; mcargs=cargs;
+          {mP=p; mU = u; mParams = pms; mconstr=gvalue; mcargs=cargs;
            mci=ci; mlf=lf}
         else
           redrec (gvalue, cargs))
     | None ->
       if reducible_mind_case sigma constr then
-        reduce_mind_case sigma
-          {mP=p; mconstr=constr; mcargs=cargs;
+        reduce_mind_case env sigma
+          {mP=p; mU = u; mParams = pms; mconstr=constr; mcargs=cargs;
           mci=ci; mlf=lf}
       else
         raise Redelimination
@@ -915,7 +921,7 @@ let try_red_product env sigma c =
           let open Context.Rel.Declaration in
           mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b)
       | LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t)
-      | Case (ci,p,iv,d,lf) -> simpfun (mkCase (ci,p,iv,redrec env d,lf))
+      | Case (ci,u,pms,p,iv,d,lf) -> simpfun (mkCase (ci,u,pms,p,iv,redrec env d,lf))
       | Proj (p, c) ->
         let c' =
           match EConstr.kind sigma c with
@@ -1062,7 +1068,7 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
       (* Still the same projection, we ignore the change in parameters *)
       mkProj (p, a')
     else mkApp (app', [| a' |])
-  | _ -> map_constr_with_binders_left_to_right sigma g f acc c
+  | _ -> map_constr_with_binders_left_to_right env sigma g f acc c
 
 let e_contextually byhead (occs,c) f = begin fun env sigma t ->
   let count = ref (Locusops.initialize_occurrence_counter occs) in
@@ -1131,7 +1137,7 @@ let substlin env sigma evalref occs c =
         count := count';
         if ok then value u else c
       | None ->
-        map_constr_with_binders_left_to_right sigma
+        map_constr_with_binders_left_to_right env sigma
           (fun _ () -> ())
           substrec () c
   in
@@ -1295,9 +1301,9 @@ let one_step_reduce env sigma c =
       | App (f,cl) -> redrec (f, (Array.to_list cl)@stack)
       | LetIn (_,f,_,cl) -> (Vars.subst1 f cl,stack)
       | Cast (c,_,_) -> redrec (c,stack)
-      | Case (ci,p,iv,c,lf) ->
+      | Case (ci,u,pms,p,iv,c,lf) ->
           (try
-             (special_red_case env sigma (ci,p,iv,c,lf), stack)
+             (special_red_case env sigma (ci,u,pms,p,iv,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
           (try match reduce_fix env sigma fix stack with
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e3e5244a8c..b0ce4fd63a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -178,7 +178,7 @@ let type_case_branches env sigma (ind,largs) pj c =
   let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
   sigma, (lc, ty, Sorts.relevance_of_sort ps)
 
-let judge_of_case env sigma ci pj iv cj lfj =
+let judge_of_case env sigma case ci pj iv cj lfj =
   let ((ind, u), spec) =
     try find_mrectype env sigma cj.uj_type
     with Not_found -> error_case_not_inductive env sigma cj in
@@ -189,7 +189,7 @@ let judge_of_case env sigma ci pj iv cj lfj =
   let () = if (match iv with | NoInvert -> false | CaseInvert _ -> true) != should_invert_case env ci
     then Type_errors.error_bad_invert env
   in
-  sigma, { uj_val  = mkCase (ci, pj.uj_val, iv, cj.uj_val, Array.map j_val lfj);
+  sigma, { uj_val  = mkCase case;
            uj_type = rslty }
 
 let check_type_fixpoint ?loc env sigma lna lar vdefj =
@@ -383,7 +383,9 @@ let rec execute env sigma cstr =
         let sigma, ty = type_of_constructor env sigma ctor in
         sigma, make_judge cstr ty
 
-    | Case (ci,p,iv,c,lf) ->
+    | Case (ci, u, pms, p, iv, c, lf) ->
+        let case = (ci, u, pms, p, iv, c, lf) in
+        let (ci, p, iv, c, lf) = EConstr.expand_case env sigma case in
         let sigma, cj = execute env sigma c in
         let sigma, pj = execute env sigma p in
         let sigma, lfj = execute_array env sigma lf in
@@ -396,7 +398,7 @@ let rec execute env sigma cstr =
             let sigma = check_actual_type env sigma cj tj.utj_val in
             sigma
         in
-        judge_of_case env sigma ci pj iv cj lfj
+        judge_of_case env sigma case ci pj iv cj lfj
 
     | Fix ((vn,i as vni),recdef) ->
         let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3d3010d1a4..a845fc3246 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -563,7 +563,7 @@ let is_rigid_head sigma flags t =
   | Construct _ | Int _ | Float _ | Array _ -> true
   | Fix _ | CoFix _ -> true
   | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _
-    | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _, _)
+    | Lambda _ | LetIn _ | App (_, _) | Case _
     | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
 
 let force_eqs c =
@@ -652,7 +652,7 @@ let rec is_neutral env sigma ts t =
       not (TransparentState.is_transparent_variable ts id)
     | Rel n -> true
     | Evar _ | Meta _ -> true
-    | Case (_, p, _, c, _) -> is_neutral env sigma ts c
+    | Case (_, _, _, _, _, c, _) -> is_neutral env sigma ts c
     | Proj (p, c) -> is_neutral env sigma ts c
     | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> false
     | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
@@ -853,7 +853,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
                unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2
              | _ -> raise ex)
 
-        | Case (ci1,p1,_,c1,cl1), Case (ci2,p2,_,c2,cl2) ->
+        | Case (ci1, u1, pms1, p1, iv1, c1, cl1), Case (ci2, u2, pms2, p2, iv2, c2, cl2) ->
+          let (ci1, p1, iv1, c1, cl1) = EConstr.expand_case env sigma (ci1, u1, pms1, p1, iv1, c1, cl1) in
+          let (ci2, p2, iv2, c2, cl2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv2, c2, cl2) in
             (try
              if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN);
              let opt' = {opt with at_top = true; with_types = false} in
@@ -1678,7 +1680,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         (push_named_context_val d sign,depdecls)
     | (AllOccurrences | AtLeastOneOccurrence), InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
-        let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in
+        let newdecl = replace_term_occ_decl_modulo env sigma occ test mkvarid d in
         if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl
            && not (indirectly_dependent sigma c d depdecls)
         then
@@ -1689,7 +1691,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
           (push_named_context_val newdecl sign, newdecl :: depdecls)
     | occ ->
         (* There are specific occurrences, hence not like first *)
-        let newdecl = replace_term_occ_decl_modulo sigma (AtOccs occ) test mkvarid d in
+        let newdecl = replace_term_occ_decl_modulo env sigma (AtOccs occ) test mkvarid d in
         (push_named_context_val newdecl sign, newdecl :: depdecls) in
   try
     let sign,depdecls =
@@ -1699,7 +1701,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       | NoOccurrences -> concl
       | occ ->
           let occ = if likefirst then LikeFirst else AtOccs occ in
-          replace_term_occ_modulo sigma occ test mkvarid concl
+          replace_term_occ_modulo env sigma occ test mkvarid concl
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in
@@ -1787,11 +1789,11 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
                  matchrec c1
                with ex when precatchable_exception ex ->
                  matchrec c2)
-          | Case(_,_,_,c,lf) -> (* does not search in the predicate *)
+          | Case(_,_,_,_,_,c,lf) -> (* does not search in the predicate *)
                (try
                  matchrec c
                with ex when precatchable_exception ex ->
-                 iter_fail matchrec lf)
+                 iter_fail matchrec (Array.map snd lf))
           | LetIn(_,c1,_,c2) ->
                (try
                  matchrec c1
@@ -1881,8 +1883,8 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
                 let c2 = args.(n-1) in
                 bind (matchrec c1) (matchrec c2)
 
-            | Case(_,_,_,c,lf) -> (* does not search in the predicate *)
-                bind (matchrec c) (bind_iter matchrec lf)
+            | Case(_,_,_,_,_,c,lf) -> (* does not search in the predicate *)
+                bind (matchrec c) (bind_iter matchrec (Array.map snd lf))
 
             | Proj (p,c) -> matchrec c
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 1420401875..314cada2d7 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -287,7 +287,7 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
           CaseInvert {univs=u; args=allargs}
         else NoInvert
       in
-      nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk
+      nf_stk env sigma (mkCase (Inductive.contract_case env (ci, p, iv, c, branchs))) tcase stk
   | Zproj p :: stk ->
      assert (from = 0) ;
      let p' = Projection.make p true in