Merge PR coq#20095: Refactor record.ml

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

dev/ci/user-overlays/20095-SkySkimmer-record-share-ind.sh

@@ -0,0 +1,3 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi record-share-ind 20095
+
+overlay metacoq https://github.com/SkySkimmer/metacoq record-share-ind 20095

vernac/comInductive.ml

@@ -528,13 +528,14 @@ let variance_of_entry ~cumulative ~variances uctx =
       assert (lvs <= lus);
       Some (Array.append variances (Array.make (lus - lvs) None))
 
-let interp_mutual_inductive_constr ~sigma ~flags ~udecl ~variances ~ctx_params ~indnames ~arities_explicit ~arities ~template_syntax ~constructors ~env_ar_params ~private_ind =
+let interp_mutual_inductive_constr ~sigma ~flags ~udecl ~variances ~ctx_params ~indnames ~arities_explicit ~arities ~template_syntax ~constructors ~env_ar ~private_ind =
   let {
     poly;
     cumulative;
     template;
     finite;
   } = flags in
+  let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
   (* Compute renewed arities *)
   let ctor_args =  List.map (fun (_,tys) ->
       List.map (fun ty ->
@@ -707,7 +708,6 @@ let interp_mutual_inductive_gen env0 ~flags udecl (uparamsl,paramsl,indl) notati
   let indimpls = List.map (fun iimpl -> useruimpls @ iimpl) indimpls in
   let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in
   let env_ar = push_types env0 indnames relevances fullarities in
-  let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
   (* Try further to solve evars, and instantiate them *)
   let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in
   let impls =
@@ -717,7 +717,7 @@ let interp_mutual_inductive_gen env0 ~flags udecl (uparamsl,paramsl,indl) notati
       indimpls cimpls
   in
   let arities_explicit = List.map (fun ar -> ar.ind_arity_explicit) indl in
-  let default_dep_elim, mie, binders, ctx = interp_mutual_inductive_constr ~flags ~sigma ~ctx_params ~udecl ~variances ~arities_explicit ~arities ~template_syntax ~constructors ~env_ar_params ~private_ind ~indnames in
+  let default_dep_elim, mie, binders, ctx = interp_mutual_inductive_constr ~flags ~sigma ~ctx_params ~udecl ~variances ~arities_explicit ~arities ~template_syntax ~constructors ~env_ar ~private_ind ~indnames in
   (default_dep_elim, mie, binders, impls, ctx)
 
 
@@ -896,8 +896,6 @@ let make_cases ind =
 module Internal =
 struct
 
-let inductive_levels = inductive_levels
-
 let error_differing_params = error_differing_params
 
 end

vernac/comInductive.mli

@@ -89,8 +89,9 @@ val interp_mutual_inductive_constr
   -> arities:EConstr.t list
   -> template_syntax:syntax_allows_template_poly list
   -> constructors:(Names.Id.t list * EConstr.constr list) list
-  -> env_ar_params:Environ.env
-  (** Environment with the inductives and parameters in the rel_context *)
+  (** Names and types of constructors, not including parameters (as in kernel entries) *)
+  -> env_ar:Environ.env
+  (** Environment with the inductives in the rel_context *)
   -> private_ind:bool
   -> DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * UnivNames.universe_binders * Univ.ContextSet.t
 
@@ -126,25 +127,9 @@ val variance_of_entry
 
 module Internal :
 sig
-  (** Returns the modified arities (the result sort may be replaced by Prop).
-      Should be called with minimized universes. *)
-  val inductive_levels
-    : Environ.env
-    -> Evd.evar_map
-    -> poly:bool
-    -> indnames:Names.Id.t list
-    -> arities_explicit:bool list
-    (* whether the arities were explicit from the user (for auto Prop lowering) *)
-    -> EConstr.constr list
-    (* arities *)
-    -> EConstr.rel_context list list
-    (* constructors *)
-    -> Evd.evar_map * (DeclareInd.default_dep_elim list * EConstr.t list)
-
   val error_differing_params
     : kind:string
     -> (Names.lident * Vernacexpr.inductive_params_expr)
     -> (Names.lident * Vernacexpr.inductive_params_expr)
     -> 'a
-
 end

vernac/declareInd.ml

@@ -183,7 +183,7 @@ let { Goptions.get = default_prop_dep_elim } =
 
 type default_dep_elim = DefaultElim | PropButDepElim
 
-let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) ?typing_flags ?(indlocs=[]) ?default_dep_elim mie ubinders impls =
+let declare_mutual_inductive_with_eliminations ?typing_flags ?(indlocs=[]) ?default_dep_elim mie ubinders impls =
   (* spiwack: raises an error if the structure is supposed to be non-recursive,
         but isn't *)
   begin match mie.mind_entry_finite with

vernac/declareInd.mli

@@ -21,8 +21,7 @@ type indlocs = (Loc.t option * Loc.t option list) list
 (** Inductive type and constructor locs, for .glob and src loc info *)
 
 val declare_mutual_inductive_with_eliminations
-  : ?primitive_expected:bool
-  -> ?typing_flags:Declarations.typing_flags
+  : ?typing_flags:Declarations.typing_flags
   -> ?indlocs:indlocs
   -> ?default_dep_elim:default_dep_elim list
   -> Entries.mutual_inductive_entry (* Inductive types declaration *)