aboutsummaryrefslogtreecommitdiff
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-03-07 20:50:30 +0100
committerPierre-Marie Pédrot2014-03-07 21:00:02 +0100
commitdd2a0175e3e35e5488c6f3b8a68c68845cbfcfd3 (patch)
tree2b61640b942b39650dec17ca077f28b5363aa843 /kernel/safe_typing.ml
parent89e59b9a578fa761ebc12e3a8e01c3b838301266 (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.ml4
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 }