Adapt w.r.t. coq/coq#18935.

src/covering.ml

@@ -444,10 +444,9 @@ let unify_type env evars before id ty after =
     let ind, params = dest_ind_family indf in
     let vs = List.map (Tacred.whd_simpl envb !evars) args in
     let params = List.map (Tacred.whd_simpl envb !evars) params in
-    let cstrs = Inductiveops.type_of_constructors envb (from_peuniverses !evars ind) in
+    let cstrs = Inductiveops.type_of_constructors envb ind in
     let cstrs = 
       Array.mapi (fun i ty ->
-          let ty = of_constr ty in
           let ty = prod_applist !evars ty params in
           let ctx, ty = decompose_prod_decls !evars ty in
           let ctx = 

src/eqdec.ml

@@ -58,10 +58,10 @@ let inductive_info sigma ((mind, _ as ind),u) =
     let induct = ((mind, i),u) in
     let indname = Nametab.basename_of_global (GlobRef.IndRef (mind,i)) in
     let indapp = applist (mkIndU induct, paramargs) in
-    let arities = arities_of_constructors env (from_peuniverses sigma induct) in
+    let arities = arities_of_constructors env induct in
      let constrs =
       Array.map (fun ty -> 
-	let _, rest = decompose_prod_n_decls sigma nparams (EConstr.of_constr ty) in
+	let _, rest = decompose_prod_n_decls sigma nparams ty in
 	let constrty = Vars.substl subst rest in
 	decompose_prod_decls sigma constrty)
 	arities

src/equations_common.ml

@@ -1054,7 +1054,7 @@ let decompose_appvect sigma t =
 
 let dest_ind_family fam =
   let ind, fam = Inductiveops.dest_ind_family fam in
-  to_peuniverses ind, List.map of_constr fam
+  ind, fam
 
 (* XXX: EConstr-versions fo these functions really needed XXX *)
 let to_constr = to_constr ~abort_on_undefined_evars:false

src/noconf.ml

@@ -57,8 +57,7 @@ let mk_eq env env' evd args args' =
 let derive_no_confusion ~pm env sigma0 ~poly (ind,u as indu) =
   let evd = ref sigma0 in
   let mindb, oneind = Global.lookup_inductive ind in
-  let pi = (fst indu, EConstr.EInstance.kind !evd (snd indu)) in
-  let _, inds = Reduction.dest_arity env (Inductiveops.type_of_inductive env pi) in
+  let _, inds = Reductionops.dest_arity env sigma0 (Inductiveops.type_of_inductive env indu) in
   let ctx = List.map of_rel_decl oneind.mind_arity_ctxt in
   let ctx = subst_instance_context u ctx in
   let ctx = smash_rel_context ctx in
@@ -96,7 +95,7 @@ let derive_no_confusion ~pm env sigma0 ~poly (ind,u as indu) =
     | Sorts.InSet -> mkSet
     | Sorts.InType | Sorts.InQSort ->
       (* In that case the noConfusion principle lives at the level of the type. *)
-      let sort = EConstr.mkSort (ESorts.make inds) in
+      let sort = EConstr.mkSort inds in
       let sigma, s =
         Evarsolve.refresh_universes ~status:Evd.univ_flexible ~onlyalg:true
           (Some false) env !evd sort

src/noconf_hom.ml

@@ -108,8 +108,7 @@ let derive_noConfusion_package ~pm env sigma ~poly (ind,u as indu) indid ~prefix
 
 let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =
   let mindb, oneind = Global.lookup_inductive ind in
-  let pi = (fst indu, EConstr.EInstance.kind sigma0 (snd indu)) in
-  let _, inds = Reduction.dest_arity env (Inductiveops.type_of_inductive env pi) in
+  let _, inds = Reductionops.dest_arity env sigma0 (Inductiveops.type_of_inductive env indu) in
   let ctx = List.map of_rel_decl oneind.mind_arity_ctxt in
   let ctx = subst_instance_context (snd indu) ctx in
   let ctx = smash_rel_context ctx in
@@ -132,8 +131,8 @@ let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =
   let sigma, s =
     match Lazy.force logic_sort with
     | Sorts.InType | Sorts.InSet | Sorts.InQSort -> (* In that case noConfusion lives at the level of the inductive family *)
-      let sort = EConstr.mkSort (ESorts.make inds) in
-      let is_level = match inds with
+      let sort = EConstr.mkSort inds in
+      let is_level = match ESorts.kind sigma0 inds with
       | Sorts.Prop | Sorts.SProp | Sorts.Set -> true
       | Sorts.Type u | Sorts.QSort (_, u) -> Univ.Universe.is_level u
       in
@@ -153,7 +152,7 @@ let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =
   in
   let _lenindices = List.length argsctx in
   let ctxmap = Context_map.id_subst fullbinders in
-  let constructors = Inductiveops.arities_of_constructors env pi in
+  let constructors = Inductiveops.arities_of_constructors env indu in
   let sigma, sigT = get_fresh sigma coq_sigma in
   let sigma, sigI = get_fresh sigma coq_sigmaI in
   let sigma, eqT = get_fresh sigma logic_eq_type in
@@ -162,7 +161,6 @@ let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =
         DAst.make Syntax.(PUVar (Name.get_id (get_name decl), Generated))) ctx
   in
   let mk_clause i ty =
-    let ty = EConstr.of_constr ty in
     let paramsctx, concl = decompose_prod_n_decls sigma params ty in
     let _, ctxpars = List.chop args ctx in
     let ctxvars = List.map (fun decl -> mkVar (Name.get_id (get_name decl))) ctxpars in

src/sigma_types.ml

@@ -222,8 +222,7 @@ let signature_class evd =
 
 let build_sig_of_ind env sigma (ind,u as indu) =
   let (mib, oib as _mind) = Inductive.lookup_mind_specif env ind in
-  let ctx = inductive_alldecls env (from_peuniverses sigma indu) in
-  let ctx = List.map of_rel_decl ctx in
+  let ctx = inductive_alldecls env indu in
   let ctx = EConstr.Vars.smash_rel_context ctx in
   let lenpars = mib.mind_nparams_rec in
   let lenargs = List.length ctx - lenpars in
@@ -515,18 +514,16 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref)
   let after, rel_decl, before = Context_map.split_context (pred rel) ctx in
   let rel_ty = Context.Rel.Declaration.get_type rel_decl in
   let rel_ty = Vars.lift rel rel_ty in
-  let rel_t = Constr.mkRel rel in
+  let rel_t = EConstr.mkRel rel in
   (* Fetch some information about the type of the variable being eliminated. *)
-  let pind, args = Inductive.find_inductive env (to_constr ~abort_on_undefined_evars:false !evd rel_ty) in
-  let mib, oib = Global.lookup_pinductive pind in
+  let pind, args = Inductiveops.find_inductive env !evd rel_ty in
+  let mib, oib = Global.lookup_inductive (fst pind) in
   let params, indices = List.chop mib.mind_nparams args in
   (* The variable itself will be treated for all purpose as one of its indices. *)
   let indices = indices @ [rel_t] in
   let indfam = Inductiveops.make_ind_family (pind, params) in
   let arity_ctx = Inductiveops.make_arity_signature env !evd true indfam in
   let rev_arity_ctx = List.rev arity_ctx in
-  let params = List.map of_constr params in
-  let indices = List.map of_constr indices in
 
   (* Firstly, we need to analyze each index to decide if we should introduce
    * an equality for it or not. *)
@@ -741,9 +738,9 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref)
   let goal = it_mkLambda_or_LetIn goal fresh_ctx in
   let params = List.map (to_constr ~abort_on_undefined_evars:false !evd) params in
   let goal' = to_constr ~abort_on_undefined_evars:false !evd goal in
-  let branches_ty = Inductive.build_branches_type pind (mib, oib) params goal' in
+  let branches_ty = Inductive.build_branches_type (from_peuniverses !evd pind) (mib, oib) params goal' in
   (* Refresh the inductive family. *)
-  let indfam = Inductiveops.make_ind_family (pind, params) in
+  let indfam = Inductiveops.make_ind_family (pind, List.map EConstr.of_constr params) in
   let branches_info = Inductiveops.get_constructors env indfam in
   let full_subst =
     let (ctx', pats, ctx) = Context_map.id_subst ctx in
@@ -758,16 +755,13 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref)
     (* This summary is under context [ctx']. *)
     let indices = summary.Inductiveops.cs_concl_realargs in
     let params = Array.of_list summary.Inductiveops.cs_params in
-    let params = Array.map of_constr params in
-    let indices = Array.map of_constr indices in
-    let term = EConstr.mkConstructU (to_peuniverses summary.Inductiveops.cs_cstr) in
+    let term = EConstr.mkConstructU (summary.Inductiveops.cs_cstr) in
     let term = EConstr.mkApp (term, params) in
     let term = Vars.lift (summary.Inductiveops.cs_nargs) term in
     let term = EConstr.mkApp (term, Context.Rel.instance EConstr.mkRel 0 summary.Inductiveops.cs_args) in
     (* Indices are typed under [args @ ctx'] *)
     let indices = (Array.to_list indices) @ [term] in
     let args = summary.Inductiveops.cs_args in
-    let args = List.map of_rel_decl args in
     (* Substitute the indices in [cuts_ctx]. *)
     let rev_indices = List.rev indices in
     let pats_indices = List.map (Context_map.pat_of_constr env !evd) rev_indices in

src/simplify.ml

@@ -347,13 +347,13 @@ let build_app_infer_concl (env : Environ.env) (evd : Evd.evar_map ref) ((ctx, ty
       | Names.GlobRef.IndRef ind ->
         let pind = Equations_common.evd_comb1 (Evd.fresh_inductive_instance env) evd ind in
         let tf = Constr.mkIndU pind in
-        let ty = Inductiveops.type_of_inductive env pind in
-        of_constr tf, of_constr ty
+        let ty = Inductiveops.type_of_inductive env (to_peuniverses pind) in
+        of_constr tf, ty
       | Names.GlobRef.ConstructRef cstr ->
         let pcstr = Equations_common.evd_comb1 (Evd.fresh_constructor_instance env) evd cstr in
         let tf = Constr.mkConstructU pcstr in
-        let ty = Inductiveops.type_of_constructor env pcstr in
-        of_constr tf, of_constr ty
+        let ty = Inductiveops.type_of_constructor env (Util.on_snd EInstance.make pcstr) in
+        of_constr tf, ty
   in
   let rec aux ty args =
     match kind !evd ty, args with

src/splitting.ml

@@ -643,7 +643,7 @@ let term_of_tree env0 isevar sort tree =
 
       (* Build the case. *)
       let case_info = Inductiveops.make_case_info env (fst pind) Constr.RegularStyle in
-      let indty = Inductiveops.find_rectype env !evd (mkApp (mkIndU pind, Array.map_of_list EConstr.of_constr args)) in
+      let indty = Inductiveops.find_rectype env !evd (mkApp (mkIndU pind, Array.of_list args)) in
       let case = Inductiveops.make_case_or_project env !evd indty case_info
           (case_ty, elim_relevance) rel_t branches in
       let term = EConstr.mkApp (case, Array.of_list to_apply) in