diff options
Diffstat (limited to 'kernel/typing.ml')
| -rw-r--r-- | kernel/typing.ml | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/kernel/typing.ml b/kernel/typing.ml index 0b236ce44c..b9ef2893a2 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -249,6 +249,9 @@ let lookup_mind = lookup_mind let lookup_mind_specif = lookup_mind_specif let lookup_meta = lookup_meta +(* Insertion of variables (named and de Bruijn'ed). They are now typed before + being added to the environment. *) + let push_rel_or_var push (id,c) env = let (j,u) = safe_machine env c in let env' = set_universes u env in @@ -259,6 +262,14 @@ let push_var nvar env = push_rel_or_var push_var nvar env let push_rel nrel env = push_rel_or_var push_rel nrel env +let push_vars vars env = + List.fold_left (fun env nvar -> push_var nvar env) env vars + +let push_rels vars env = + List.fold_left (fun env nvar -> push_rel nvar env) env vars + +(* Insertion of constants and parameters in environment. *) + let add_constant sp ce env = let (jb,u) = safe_machine env ce.const_entry_body in let env' = set_universes u env in @@ -294,11 +305,7 @@ let add_parameter sp c env = in Environ.add_constant sp cb env' -let push_vars vars env = - List.fold_left (fun env nvar -> push_var nvar env) env vars - -let push_rels vars env = - List.fold_left (fun env nvar -> push_rel nvar env) env vars +(* Insertion of inductive types. *) let check_type_constructs env_params univ nparams lc = let check_one env c = @@ -334,6 +341,7 @@ let add_mind sp mie env = type judgment = unsafe_judgment + (*s Machines with information. *) type information = Logic | Inf of unsafe_judgment |