diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-05 21:39:39 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-05 21:39:39 +0100 |
commit | 00df486efd76070b6c3673071050565e0ed4466e (patch) | |
tree | ef98cd2acfee9bcbea02d664833bb4a586fa4f87 /kernel/safe_typing.ml | |
parent | 2a0d260c9c80c07844605fcb6844bb9cfdfeb0fd (diff) |
Using HMaps in Safe_env.environments, hopefully improving performances.
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r-- | kernel/safe_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bf758b96b..670e115af 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -766,9 +766,9 @@ 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.env_globals.env_constants in + let (cb,r) = Constants.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in - let new_constants = Cmap_env.add kn (cb,r) env.env_globals.env_constants in + let new_constants = Constants.add kn (cb,r) env.env_globals.env_constants in let new_globals = { env.env_globals with env_constants = new_constants } in let env = { env with env_globals = new_globals } in { senv with env = env_of_pre_env env } |