diff options
| author | Pierre-Marie Pédrot | 2014-03-07 20:50:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-07 21:00:02 +0100 |
| commit | dd2a0175e3e35e5488c6f3b8a68c68845cbfcfd3 (patch) | |
| tree | 2b61640b942b39650dec17ca077f28b5363aa843 /kernel/safe_typing.ml | |
| parent | 89e59b9a578fa761ebc12e3a8e01c3b838301266 (diff) | |
Using Hashmaps by default in constant and inductive maps. This changes fold and
iter order, but it seems nobody was relying on it (contrarily to the string case).
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 670e115af8..bf758b96b1 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) = Constants.find kn env.env_globals.env_constants in + let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in - let new_constants = Constants.add kn (cb,r) env.env_globals.env_constants in + let new_constants = Cmap_env.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 } |
