Merge PR #11027: Cleanup post #10647 (expose comind universe handling)

Reviewed-by: ppedrot

18 files changed, 94 insertions, 162 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index d20eea7874..06ee4fcc7a 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -61,7 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     mind_entry_params = mb.mind_params_ctxt;
     mind_entry_inds;
     mind_entry_universes;
-    mind_entry_variance = mb.mind_variance;
+    mind_entry_cumulative= Option.has_some mb.mind_variance;
     mind_entry_private = mb.mind_private;
   }
 
diff --git a/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh
new file mode 100644
index 0000000000..bb65beb043
--- /dev/null
+++ b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh
@@ -0,0 +1,19 @@
+if [ "$CI_PULL_REQUEST" = "11027" ] || [ "$CI_BRANCH" = "cleanup-comind-univ" ]; then
+
+    elpi_CI_REF=expose-comind-univ
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=expose-comind-univ
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    paramcoq_CI_REF=expose-comind-univ
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+    mtac2_CI_REF=expose-comind-univ
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
+
+    rewriter_CI_REF=cleanup-comind-univ
+    rewriter_CI_GITURL=https://github.com/SkySkimmer/rewriter
+
+
+fi
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 9d7387c7ad..261a3510d6 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -315,10 +315,6 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
     let ctx = List.rev mip.mind_arity_ctxt in
       mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
 
-let dummy_variance = let open Entries in function
-  | Monomorphic_entry _ -> assert false
-  | Polymorphic_entry (_,uctx) -> Array.make (Univ.UContext.size uctx) Univ.Variance.Irrelevant
-
 let cook_inductive { Opaqueproof.modlist; abstract } mib =
   let open Entries in
   let (section_decls, subst, abs_uctx) = abstract in
@@ -333,10 +329,6 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
       let auctx = Univ.AUContext.repr auctx in
       subst, Polymorphic_entry (nas, auctx)
   in
-  let variance = match mib.mind_variance with
-    | None -> None
-    | Some _ -> Some (dummy_variance ind_univs)
-  in
   let cache = RefTable.create 13 in
   let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in
   let inds =
@@ -363,7 +355,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
     mind_entry_params = params';
     mind_entry_inds = inds';
     mind_entry_private = mib.mind_private;
-    mind_entry_variance = variance;
+    mind_entry_cumulative = Option.has_some mib.mind_variance;
     mind_entry_universes = ind_univs
   }
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index b50c3ebbc3..8d930b521c 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -50,7 +50,7 @@ type mutual_inductive_entry = {
   mind_entry_params : Constr.rel_context;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_universes : universes_entry;
-  mind_entry_variance : Univ.Variance.t array option;
+  mind_entry_cumulative : bool;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
   mind_entry_private : bool option;
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index c91cb39fe2..982bc49927 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -61,64 +61,6 @@ let mind_check_names mie =
 
 
 (************************************************************************)
-(************************** Cumulativity checking************************)
-(************************************************************************)
-
-(* Check arities and constructors *)
-let check_subtyping_arity_constructor env subst arcn numparams is_arity =
-  let numchecked = ref 0 in
-  let basic_check ev tp =
-    if !numchecked < numparams then () else Reduction.conv_leq ev tp (subst tp);
-    numchecked := !numchecked + 1
-  in
-  let check_typ typ typ_env =
-    match typ with
-    | LocalAssum (_, typ') ->
-      begin
-       try
-          basic_check typ_env typ'; Environ.push_rel typ typ_env
-        with Reduction.NotConvertible ->
-          CErrors.anomaly ~label:"bad inductive subtyping relation"
-            Pp.(str "Invalid subtyping relation")
-      end
-    | _ -> CErrors.anomaly Pp.(str "")
-  in
-  let typs, codom = Reduction.dest_prod env arcn in
-  let last_env = Context.Rel.fold_outside check_typ typs ~init:env in
-  if not is_arity then basic_check last_env codom else ()
-
-let check_cumulativity univs variances env_ar params data =
-  let uctx = match univs with
-    | Monomorphic_entry _ -> raise (InductiveError BadUnivs)
-    | Polymorphic_entry (_,uctx) -> uctx
-  in
-  let instance = UContext.instance uctx in
-  if Instance.length instance != Array.length variances then raise (InductiveError BadUnivs);
-  let numparams = Context.Rel.nhyps params in
-  let new_levels = Array.init (Instance.length instance)
-      (fun i -> Level.(make (UGlobal.make DirPath.empty i)))
-  in
-  let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
-      LMap.empty (Instance.to_array instance) new_levels
-  in
-  let dosubst = Vars.subst_univs_level_constr lmap in
-  let instance_other = Instance.of_array new_levels in
-  let constraints_other = Univ.subst_univs_level_constraints lmap (UContext.constraints uctx) in
-  let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-  let env = Environ.push_context uctx_other env_ar in
-  let subtyp_constraints =
-    Univ.enforce_leq_variance_instances variances
-      instance instance_other
-      Constraint.empty
-  in
-  let env = Environ.add_constraints subtyp_constraints env in
-  (* process individual inductive types: *)
-  List.iter (fun (arity,lc) ->
-        check_subtyping_arity_constructor env dosubst arity numparams true;
-        Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc)
-    data
-
-(************************************************************************)
 (************************** Type checking *******************************)
 (************************************************************************)
 
@@ -389,11 +331,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
         data, Some None
   in
 
-  let () = match mie.mind_entry_variance with
-    | None -> ()
-    | Some variances ->
-      check_cumulativity mie.mind_entry_universes variances env_ar params (List.map pi1 data)
-  in
+  (* TODO pass only the needed bits *)
+  let variance = InferCumulativity.infer_inductive env mie in
 
   (* Abstract universes *)
   let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
@@ -408,4 +347,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
     Environ.push_rel_context ctx env
   in
 
-  env_ar_par, univs, mie.mind_entry_variance, record, params, Array.of_list data
+  env_ar_par, univs, variance, record, params, Array.of_list data
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 550c81ed82..77abe6b410 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -216,19 +216,11 @@ let infer_inductive env mie =
   let open Entries in
   let params = mie.mind_entry_params in
   let entries = mie.mind_entry_inds in
-  let variances =
-    match mie.mind_entry_variance with
-    | None -> None
-    | Some _ ->
-      let uctx = match mie.mind_entry_universes with
-        | Monomorphic_entry _ -> assert false
-        | Polymorphic_entry (_,uctx) -> uctx
-      in
-      try Some (infer_inductive_core env params entries uctx)
-      with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
-  in
-  { mie with mind_entry_variance = variances }
-
-let dummy_variance = let open Entries in function
-  | Monomorphic_entry _ -> assert false
-  | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant
+  if not mie.mind_entry_cumulative then None
+  else
+    let uctx = match mie.mind_entry_universes with
+      | Monomorphic_entry _ -> assert false
+      | Polymorphic_entry (_,uctx) -> uctx
+    in
+    try Some (infer_inductive_core env params entries uctx)
+    with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index a234e334d1..2bddfe21e2 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -9,6 +9,4 @@
 (************************************************************************)
 
 val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
-  Entries.mutual_inductive_entry
-
-val dummy_variance : Entries.universes_entry -> Univ.Variance.t array
+  Univ.Variance.t array option
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 2b83c2d868..f1e994b337 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -42,9 +42,9 @@ Type_errors
 Modops
 Inductive
 Typeops
+InferCumulativity
 IndTyping
 Indtypes
-InferCumulativity
 Cooking
 Term_typing
 Subtyping
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 759feda9ab..d04f43f5bd 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1015,7 +1015,6 @@ let close_section senv =
   | `Inductive (ind, mib) ->
     let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
     let mie = Cooking.cook_inductive info mib in
-    let mie = InferCumulativity.infer_inductive senv.env mie in
     let _, senv = add_mind (MutInd.label ind) mie senv in
     senv
   in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index ca5c8b30c2..98d14f3d33 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1930,7 +1930,7 @@ let build_morphism_signature env sigma m =
   let evd = solve_constraints env !evd in
   let evd = Evd.minimize_universes evd in
   let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
-  Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m);
+  Pretyping.check_evars env evd (EConstr.of_constr m);
   Evd.evar_universe_context evd, m
 
 let default_morphism sign m =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4925f3e5fa..44b3d59287 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -288,16 +288,18 @@ let check_extra_evars_are_solved env current_sigma frozen = match frozen with
 
 (* [check_evars] fails if some unresolved evar remains *)
 
-let check_evars env initial_sigma sigma c =
+let check_evars env ?initial sigma c =
   let rec proc_rec c =
     match EConstr.kind sigma c with
     | Evar (evk, _) ->
-      if not (Evd.mem initial_sigma evk) then
-        let (loc,k) = evar_source evk sigma in
-        begin match k with
-          | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
-          | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None
-        end
+      (match initial with
+       | Some initial when Evd.mem initial evk -> ()
+       | _ ->
+         let (loc,k) = evar_source evk sigma in
+         begin match k with
+           | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
+           | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None
+         end)
     | _ -> EConstr.iter sigma proc_rec c
   in proc_rec c
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index f9da568c75..4aaf1376ad 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -115,9 +115,10 @@ val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
 val check_evars_are_solved :
   program_mode:bool -> env -> ?initial:evar_map -> (* current map: *) evar_map -> unit
 
-(** [check_evars env initial_sigma extended_sigma c] fails if some
-   new unresolved evar remains in [c] *)
-val check_evars : env -> evar_map -> evar_map -> constr -> unit
+(** [check_evars env ?initial sigma c] fails if some unresolved evar
+   remains in [c] which isn't in [initial] (any unresolved evar if
+   [initial] not provided) *)
+val check_evars : env -> ?initial:evar_map -> evar_map -> constr -> unit
 
 (**/**)
 (** Internal of Pretyping... *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index eb50a2a67c..7b3797119a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1289,8 +1289,7 @@ let prepare_hint check env init (sigma,c) =
       mkNamedLambda (make_annot id Sorts.Relevant) t (iter (replace_term sigma evar (mkVar id) c)) in
   let c' = iter c in
     let env = Global.env () in
-    let empty_sigma = Evd.from_env env in
-    if check then Pretyping.check_evars env empty_sigma sigma c';
+    if check then Pretyping.check_evars env sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     (c', diff)
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 0333b73ffe..c9b5144299 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -410,7 +410,7 @@ let do_instance_resolve_TC termtype sigma env =
   (* Beware of this step, it is required as to minimize universes. *)
   let sigma = Evd.minimize_universes sigma in
   (* Check that the type is free of evars now. *)
-  Pretyping.check_evars env (Evd.from_env env) sigma termtype;
+  Pretyping.check_evars env sigma termtype;
   termtype, sigma
 
 let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index a001420f74..8a403e5a03 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -255,7 +255,7 @@ let context ~poly l =
   let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
   (* Note, we must use the normalized evar from now on! *)
   let sigma = Evd.minimize_universes sigma in
-  let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
+  let ce t = Pretyping.check_evars env sigma t in
   let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in
   (* reorder, evar-normalize and add implicit status *)
   let ctx = List.rev_map (fun d ->
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 2aee9bd47f..b603c54026 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -255,7 +255,7 @@ let inductive_levels env evd arities inds =
   in
   let cstrs_levels, min_levels, sizes =
     CList.split3
-      (List.map2 (fun (_,tys,_) (arity,(ctx,du)) ->
+      (List.map2 (fun (_,tys) (arity,(ctx,du)) ->
         let len = List.length tys in
         let minlev = Sorts.univ_of_sort du in
         let minlev =
@@ -323,18 +323,18 @@ let check_named {CAst.loc;v=na} = match na with
   let msg = str "Parameters must be named." in
   user_err ?loc  msg
 
-let template_polymorphism_candidate env ~ctor_levels uctx params concl =
+let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl =
   match uctx with
   | Entries.Monomorphic_entry uctx ->
     let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
     if not concltemplate then false
+    else if not template_check then true
     else
-      let template_check = Environ.check_template env in
       let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
       let params, conclunivs =
         IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu
       in
-      not (template_check && Univ.LSet.is_empty conclunivs)
+      not (Univ.LSet.is_empty conclunivs)
   | Entries.Polymorphic_entry _ -> false
 
 let check_param = function
@@ -350,33 +350,28 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = Univ.LSet.empty in
   let uvars = Context.Rel.(fold_outside (Declaration.fold_constr merge_universes_of_constr) ctx_params ~init:uvars) in
   let uvars = List.fold_right merge_universes_of_constr arities uvars in
-  let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
+  let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
-let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_params ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
+let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
   (* Compute renewed arities *)
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
-  let constructors = List.map (on_pi2 (List.map nf)) constructors in
+  let constructors = List.map (on_snd (List.map nf)) constructors in
   let arities = List.map EConstr.(to_constr sigma) arities in
   let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in
   let sigma, arities = inductive_levels env_ar_params sigma arities constructors in
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
   let arities = List.map (on_snd nf) arities in
-  let constructors = List.map (on_pi2 (List.map nf)) constructors in
+  let constructors = List.map (on_snd (List.map nf)) constructors in
   let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
   let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in
   let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in
   let uctx = Evd.check_univ_decl ~poly sigma udecl in
-  List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities;
-  Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
-  List.iter (fun (_,ctyps,_) ->
-    List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
-    constructors;
 
   (* Build the inductive entries *)
-  let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) ->
+  let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) ->
       let template_candidate () =
         templatearity ||
         let ctor_levels =
@@ -390,7 +385,7 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
           List.fold_left (fun levels c -> add_levels c levels)
             param_levels ctypes
         in
-        template_polymorphism_candidate env0 ~ctor_levels uctx ctx_params concl
+        template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl
       in
       let template = match template with
         | Some template ->
@@ -408,7 +403,6 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
       })
       indnames arities arityconcl constructors
   in
-  let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in
   (* Build the mutual inductive entry *)
   let mind_ent =
     { mind_entry_params = ctx_params;
@@ -417,12 +411,10 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
       mind_entry_inds = entries;
       mind_entry_private = if private_ind then Some false else None;
       mind_entry_universes = uctx;
-      mind_entry_variance = variance;
+      mind_entry_cumulative = poly && cumulative;
     }
   in
-  (if poly && cumulative then
-      InferCumulativity.infer_inductive env_ar mind_ent
-   else mind_ent), Evd.universe_binders sigma
+  mind_ent, Evd.universe_binders sigma
 
 let interp_params env udecl uparamsl paramsl =
   let sigma, udecl = interp_univ_decl_opt env udecl in
@@ -492,9 +484,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
     List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs))
     @ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in
   let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in
+  let cimpls = List.map pi3 constructors in
   let constructors = List.map (fun (cnames,ctypes,cimpls) ->
-                         (cnames,List.map generalize_constructor ctypes,cimpls))
-                       constructors
+      (cnames,List.map generalize_constructor ctypes))
+      constructors
   in
   let ctx_params = ctx_params @ ctx_uparams in
   let userimpls = useruimpls @ userimpls in
@@ -505,11 +498,12 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   (* Try further to solve evars, and instantiate them *)
   let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in
   let impls =
-    List.map2 (fun indimpls (_,_,cimpls) ->
+    List.map2 (fun indimpls cimpls ->
         indimpls, List.map (fun impls ->
-            userimpls @ impls) cimpls) indimpls constructors
+            userimpls @ impls) cimpls)
+      indimpls cimpls
   in
-  let mie, pl = interp_mutual_inductive_constr ~env0 ~template ~sigma ~env_params ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
+  let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
   (mie, pl, impls)
 
 
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index ef05b213d8..cc104b3762 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -49,24 +49,22 @@ val declare_mutual_inductive_with_eliminations
   -> Names.MutInd.t
   [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
 
-val interp_mutual_inductive_constr :
-  env0:Environ.env ->
-  sigma:Evd.evar_map ->
-  template:bool option ->
-  udecl:UState.universe_decl ->
-  env_ar:Environ.env ->
-  env_params:Environ.env ->
-  ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list ->
-  indnames:Names.Id.t list ->
-  arities:EConstr.t list ->
-  arityconcl:(bool * EConstr.ESorts.t) option list ->
-  constructors:(Names.Id.t list * Constr.constr list * 'a list list) list ->
-  env_ar_params:Environ.env ->
-  cumulative:bool ->
-  poly:bool ->
-  private_ind:bool ->
-  finite:Declarations.recursivity_kind ->
-  Entries.mutual_inductive_entry * UnivNames.universe_binders
+val interp_mutual_inductive_constr
+  : sigma:Evd.evar_map
+  -> template:bool option
+  -> udecl:UState.universe_decl
+  -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list
+  -> indnames:Names.Id.t list
+  -> arities:EConstr.t list
+  -> arityconcl:(bool * EConstr.ESorts.t) option list
+  -> constructors:(Names.Id.t list * Constr.constr list) list
+  -> env_ar_params:Environ.env
+  (** Environment with the inductives and parameters in the rel_context *)
+  -> cumulative:bool
+  -> poly:bool
+  -> private_ind:bool
+  -> finite:Declarations.recursivity_kind
+  -> Entries.mutual_inductive_entry * UnivNames.universe_binders
 
 (************************************************************************)
 (** Internal API, exported for Record                                   *)
@@ -78,17 +76,17 @@ val should_auto_template : Id.t -> bool -> bool
    inductive under consideration. *)
 
 val template_polymorphism_candidate
-  : Environ.env
+  : template_check:bool
   -> ctor_levels:Univ.LSet.t
   -> Entries.universes_entry
   -> Constr.rel_context
   -> Sorts.t option
   -> bool
-(** [template_polymorphism_candidate env ~ctor_levels uctx params
+(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params
    conclsort] is [true] iff an inductive with params [params],
    conclusion [conclsort] and universe levels appearing in the
    constructor arguments [ctor_levels] would be definable as template
    polymorphic. It should have at least one universe in its
    monomorphic universe context that can be made parametric in its
-   conclusion sort, if one is given. If the [Template Check] flag is
+   conclusion sort, if one is given. If the [template_check] flag is
    false we just check that the conclusion sort is not small. *)
diff --git a/vernac/record.ml b/vernac/record.ml
index d85b71df44..ea10e06d02 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -202,7 +202,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
   in
   let univs = Evd.check_univ_decl ~poly sigma decl in
   let ubinders = Evd.universe_binders sigma in
-  let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in
+  let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in
   let () = List.iter (iter_constr ce) (List.rev newps) in
   ubinders, univs, template, newps, imps, ans
 
@@ -411,7 +411,6 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
     | Polymorphic_entry (nas, ctx) ->
       true, Polymorphic_entry (nas, ctx)
   in
-  let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance ctx) else None in
   let binder_name =
     match name with
     | None ->
@@ -447,7 +446,8 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
                univs)
             param_levels fields
         in
-        ComInductive.template_polymorphism_candidate (Global.env ()) ~ctor_levels univs params
+        let template_check = Environ.check_template (Global.env ()) in
+        ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params
           (Some (Sorts.sort_of_univ min_univ))
       in
       match template with
@@ -477,10 +477,9 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
       mind_entry_inds = blocks;
       mind_entry_private = None;
       mind_entry_universes = univs;
-      mind_entry_variance = variance;
+      mind_entry_cumulative = poly && cumulative;
     }
   in
-  let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
   let impls = List.map (fun _ -> paramimpls, []) record_data in
   let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls
       ~primitive_expected:!primitive_flag