Merge PR #8684: Remove a few circumvolutions around parameters of inductive entries

9 files changed, 31 insertions, 57 deletions

diff --git a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh
new file mode 100644
index 0000000000..98530c825a
--- /dev/null
+++ b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "8684" ] || [ "$CI_BRANCH" = "kernel-entries-cleanup" ]; then
+
+    Elpi_CI_REF=kernel-entries-cleanup
+    Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+    Equations_CI_REF=kernel-entries-cleanup
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 0e44a8b467..21b2e85e8f 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Names
-open CErrors
 open Util
 open Term
 open Constr
@@ -17,17 +15,10 @@ open Vars
 open Declarations
 open Cooking
 open Entries
-open Context.Rel.Declaration
 
 (********************************)
 (* Discharging mutual inductive *)
 
-let detype_param =
-  function
-  | LocalAssum (Name id, p) -> id, LocalAssumEntry p
-  | LocalDef (Name id, p,_) -> id, LocalDefEntry p
-  | _ -> anomaly (Pp.str "Unnamed inductive local variable.")
-
 (* Replace
 
      Var(y1)..Var(yq):C1..Cq |- Ij:Bj
@@ -57,7 +48,7 @@ let abstract_inductive decls nparamdecls inds =
 (* To be sure to be the same as before, should probably be moved to process_inductive *)
   let params' = let (_,arity,_,_,_) = List.hd inds' in
 		let (params,_) = decompose_prod_n_assum nparamdecls' arity in
-                List.map detype_param params
+    params
   in
   let ind'' =
   List.map
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 94248ad26b..c5bcd74072 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -16,14 +16,6 @@ open Constr
    constants/axioms, mutual inductive definitions, modules and module
    types *)
 
-
-(** {6 Local entries } *)
-
-type local_entry =
-  | LocalDefEntry of constr
-  | LocalAssumEntry of constr
-
-
 (** {6 Declaration of inductive types. } *)
 
 (** Assume the following definition in concrete syntax:
@@ -54,7 +46,7 @@ type mutual_inductive_entry = {
       record in their respective projections. Not used by the kernel.
       Some None: non-primitive record *)
   mind_entry_finite : Declarations.recursivity_kind;
-  mind_entry_params : (Id.t * local_entry) list;
+  mind_entry_params : Constr.rel_context;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_universes : inductive_universes;
   (* universe constraints and the constraints for subtyping of
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b976469ff7..0346026aa4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -271,7 +271,8 @@ let typecheck_inductive env mie =
     | Polymorphic_ind_entry ctx -> push_context ctx env
     | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
   in
-  let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
+  let env_params = check_context env' mie.mind_entry_params in
+  let paramsctxt = mie.mind_entry_params in
   (* We first type arity of each inductive definition *)
   (* This allows building the environment of arities and to share *)
   (* the set of constraints *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3481d3bedb..1bb2d3c79c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -515,25 +515,19 @@ let infer_v env cv =
 
 (* Typing of several terms. *)
 
-let infer_local_decl env id = function
-  | Entries.LocalDefEntry c ->
-      let () = check_wellformed_universes env c in
-      let t = execute env c in
-      RelDecl.LocalDef (Name id, c, t)
-  | Entries.LocalAssumEntry c ->
-      let () = check_wellformed_universes env c in
-      let t = execute env c in
-      RelDecl.LocalAssum (Name id, check_assumption env c t)
-
-let infer_local_decls env decls =
-  let rec inferec env = function
-  | (id, d) :: l ->
-      let (env, l) = inferec env l in
-      let d = infer_local_decl env id d in
-        (push_rel d env, Context.Rel.add d l)
-  | [] -> (env, Context.Rel.empty)
-  in
-  inferec env decls
+let check_context env rels =
+  let open Context.Rel.Declaration in
+  Context.Rel.fold_outside (fun d env ->
+    match d with
+      | LocalAssum (_,ty) ->
+        let _ = infer_type env ty in
+        push_rel d env
+      | LocalDef (_,bd,ty) ->
+        let j1 = infer env bd in
+        let _ = infer_type env ty in
+        conv_leq false env j1.uj_type ty;
+        push_rel d env)
+    rels ~init:env
 
 let judge_of_prop = make_judge mkProp type1
 let judge_of_set = make_judge mkSet type1
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 1fd070d9d5..d24002065b 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -12,7 +12,6 @@ open Names
 open Constr
 open Univ
 open Environ
-open Entries
 
 (** {6 Typing functions (not yet tagged as safe) }
 
@@ -27,8 +26,8 @@ val infer      : env -> constr       -> unsafe_judgment
 val infer_v    : env -> constr array -> unsafe_judgment array
 val infer_type : env -> types        -> unsafe_type_judgment
 
-val infer_local_decls :
-  env -> (Id.t * local_entry) list -> (env * Constr.rel_context)
+val check_context :
+  env -> Constr.rel_context -> env
 
 (** {6 Basic operations of the typing machine. } *)
 
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index a56a8314e6..422a05c19a 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -196,7 +196,7 @@ let infer_inductive env mie =
         Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances)
           LMap.empty uarray
       in
-      let env, _ = Typeops.infer_local_decls env params in
+      let env = Typeops.check_context env params in
       let variances = List.fold_left (fun variances entry ->
           let variances = infer_arity_constructor true
               env variances entry.mind_entry_arity
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 885a22b209..5ff3032ec4 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -102,10 +102,6 @@ let mk_mltype_data sigma env assums arity indname =
   let is_ml_type = is_sort env sigma arity in
   (is_ml_type,indname,assums)
 
-let prepare_param = function
-  | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t
-  | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b
-
 (** Make the arity conclusion flexible to avoid generating an upper bound universe now,
     only if the universe does not appear anywhere else.
     This is really a hack to stay compatible with the semantics of template polymorphic
@@ -463,7 +459,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   in
   (* Build the mutual inductive entry *)
   let mind_ent =
-    { mind_entry_params = List.map prepare_param ctx_params;
+    { mind_entry_params = ctx_params;
       mind_entry_record = None;
       mind_entry_finite = finite;
       mind_entry_inds = entries;
diff --git a/vernac/record.ml b/vernac/record.ml
index 3ba360fee4..7a4c38e972 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -191,14 +191,6 @@ let typecheck_params_and_fields finite def poly pl ps records =
   let ans = List.map2 map data typs in
   ubinders, univs, template, newps, imps, ans
 
-let degenerate_decl decl =
-  let id = match RelDecl.get_name decl with
-    | Name id -> id
-    | Anonymous -> anomaly (Pp.str "Unnamed record variable.") in
-  match decl with
-    | LocalAssum (_,t) -> (id, LocalAssumEntry t)
-    | LocalDef (_,b,_) -> (id, LocalDefEntry b)
-
 type record_error =
   | MissingProj of Id.t * Id.t list
   | BadTypedProj of Id.t * env * Type_errors.type_error
@@ -437,7 +429,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
   in
   let blocks = List.mapi mk_block record_data in
   let mie =
-    { mind_entry_params = List.map degenerate_decl params;
+    { mind_entry_params = params;
       mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
       mind_entry_finite = finite;
       mind_entry_inds = blocks;