From dd2a0175e3e35e5488c6f3b8a68c68845cbfcfd3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 7 Mar 2014 20:50:30 +0100 Subject: 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). --- kernel/safe_typing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/safe_typing.ml') 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 } -- cgit v1.2.3