diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 15 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
2 files changed, 17 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 62e2d46a85..636644ec3a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -771,3 +771,18 @@ let j_type j = j.uj_type let safe_infer senv = infer (env_of_senv senv) let typing senv = Typeops.typing (env_of_senv senv) + +(* This function serves only for inlining constants in native compiler for now, +but it is meant to become a replacement for environ.register *) +let register_inline kn senv = + if not (evaluable_constant kn senv.env) then + Errors.error "Register inline: an evaluable constant is expected"; + let env = pre_env senv.env in + let (cb,r) = Cmap_env.find kn env.Pre_env.env_globals.Pre_env.env_constants in + let cb = {cb with const_inline_code = true} in + let new_constants = + Cmap_env.add kn (cb,r) env.Pre_env.env_globals.Pre_env.env_constants + in + let new_globals = { env.Pre_env.env_globals with Pre_env.env_constants = new_constants } in + let env = { env with Pre_env.env_globals = new_globals } in + { senv with env = env_of_pre_env env } diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 31bb8143e9..7ca0333833 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -136,3 +136,5 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a val register : safe_environment -> field -> Retroknowledge.entry -> constr -> safe_environment + +val register_inline : constant -> safe_environment -> safe_environment |