1 files changed, 11 insertions, 8 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 23145b1629..d02b015604 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -245,6 +245,14 @@ let inductive_alldecls env (ind,u) =
 let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u)
 [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"]
 
+let inductive_alltags env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  Context.Rel.to_tags mip.mind_arity_ctxt
+
+let constructor_alltags env (ind,j) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  Context.Rel.to_tags (fst mip.mind_nf_lc.(j-1))
+
 let constructor_has_local_defs env (indsp,j) =
   let (mib,mip) = Inductive.lookup_mind_specif env indsp in
   let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in
@@ -336,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 =
@@ -348,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
@@ -741,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