From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- library/global.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'library/global.ml') 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 = -- cgit v1.2.3