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

4 files changed, 18 insertions, 32 deletions

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. } *)