diff options
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 23 |
1 files changed, 7 insertions, 16 deletions
diff --git a/library/global.ml b/library/global.ml index 43097dc5d..ce37dfecf 100644 --- a/library/global.ml +++ b/library/global.ml @@ -8,7 +8,6 @@ open Names open Environ -open Decl_kinds (** We introduce here the global environment of the system, and we declare it as a synchronized table. *) @@ -21,6 +20,7 @@ module GlobalSafeEnv : sig 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 + val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag end = struct @@ -31,9 +31,9 @@ let join_safe_environment ?except () = let is_joined_environment () = Safe_typing.is_joined_environment !global_env - -let () = - Summary.declare_summary global_env_summary_name + +let global_env_summary_tag = + Summary.declare_summary_tag global_env_summary_name { Summary.freeze_function = (function | `Yes -> join_safe_environment (); !global_env | `No -> !global_env @@ -52,6 +52,8 @@ let set_safe_env e = global_env := e end +let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag + let safe_env = GlobalSafeEnv.safe_env let join_safe_environment ?except () = GlobalSafeEnv.join_safe_environment ?except () @@ -231,18 +233,7 @@ let universes_of_global env r = let universes_of_global gr = universes_of_global (env ()) gr -(** Global universe names *) -type universe_names = - (polymorphic * Univ.Level.t) Id.Map.t * Id.t Univ.LMap.t - -let global_universes = - Summary.ref ~name:"Global universe names" - ((Id.Map.empty, Univ.LMap.empty) : universe_names) - -let global_universe_names () = !global_universes -let set_global_universe_names s = global_universes := s - -let is_polymorphic r = +let is_polymorphic r = let env = env() in match r with | VarRef id -> false |