diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml | 10 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 3 | ||||
| -rw-r--r-- | kernel/typeops.ml | 32 | ||||
| -rw-r--r-- | kernel/typeops.mli | 5 |
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. } *) |