Imported Upstream version 8.5~beta3+dfsg

1 files changed, 9 insertions, 5 deletions

diff --git a/library/global.ml b/library/global.ml
index 875097e4..6002382c 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -19,6 +19,7 @@ module GlobalSafeEnv : sig
   val safe_env : unit -> Safe_typing.safe_environment
   val set_safe_env : Safe_typing.safe_environment -> unit
   val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
+  val is_joined_environment : unit -> bool
 
 end = struct
 
@@ -27,6 +28,9 @@ let global_env = ref Safe_typing.empty_environment
 let join_safe_environment ?except () =
   global_env := Safe_typing.join_safe_environment ?except !global_env
 
+let is_joined_environment () =
+  Safe_typing.is_joined_environment !global_env
+  
 let () =
   Summary.declare_summary global_env_summary_name
     { Summary.freeze_function = (function
@@ -50,6 +54,7 @@ end
 let safe_env = GlobalSafeEnv.safe_env
 let join_safe_environment ?except () =
   GlobalSafeEnv.join_safe_environment ?except ()
+let is_joined_environment = GlobalSafeEnv.is_joined_environment
 
 let env () = Safe_typing.env_of_safe_env (safe_env ())
 
@@ -73,13 +78,12 @@ let globalize_with_summary fs f =
 let i2l = Label.of_id
 
 let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
-let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_named_def d = globalize (Safe_typing.push_named_def d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
-let push_context_set c = globalize0 (Safe_typing.push_context_set c)
-let push_context c = globalize0 (Safe_typing.push_context c)
+let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
+let push_context b c = globalize0 (Safe_typing.push_context b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
-let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type)
 let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
 let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
@@ -245,7 +249,7 @@ let current_dirpath () =
 
 let with_global f = 
   let (a, ctx) = f (env ()) (current_dirpath ()) in
-    push_context_set ctx; a
+    push_context_set false ctx; a
 
 (* spiwack: register/unregister functions for retroknowledge *)
 let register field value by_clause =