From 3984f3c1db51f7b788ad49eafb7647774e8d1f53 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Jun 2018 14:04:25 +0200
Subject: Make Environ.globals abstract.

---
 kernel/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 12c82e20de..caa935506d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -918,7 +918,7 @@ let register_inline kn senv =
   if not (evaluable_constant kn senv.env) then
     CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected");
   let env = senv.env in
-  let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in
+  let cb = lookup_constant kn env in
   let cb = {cb with const_inline_code = true} in
   let env = add_constant kn cb env in { senv with env}
 
-- 
cgit v1.2.3


From e7e3714f0fd0e791501acccca3317ed8175c4815 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 22 Jun 2018 14:08:49 +0200
Subject: Deprecate Environ.retroknowledge function in favor of the projection

---
 kernel/safe_typing.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index caa935506d..f87ec9e023 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -897,9 +897,11 @@ let typing senv = Typeops.infer (env_of_senv senv)
 
 (** {6 Retroknowledge / native compiler } *)
 
+[@@@ocaml.warning "-3"]
 (** universal lifting, used for the "get" operations mostly *)
 let retroknowledge f senv =
   Environ.retroknowledge f (env_of_senv senv)
+[@@@ocaml.warning "+3"]
 
 let register field value by_clause senv =
   (* todo : value closed, by_clause safe, by_clause of the proper type*)
-- 
cgit v1.2.3