From 00df486efd76070b6c3673071050565e0ed4466e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Mar 2014 21:39:39 +0100
Subject: Using HMaps in Safe_env.environments, hopefully improving
 performances.

---
 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 bf758b96b1..670e115af8 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 }
-- 
cgit v1.2.3