Moving Universes to the engine/ folder.

Before this patch, this module was a member of the library folder, which had
little to do with its actual use. A tiny part relative to global registering
of universe names has been effectively moved to the Global module.

1 files changed, 12 insertions, 0 deletions

diff --git a/library/global.ml b/library/global.ml
index e748434d2..5fa710b36 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -8,6 +8,7 @@
 
 open Names
 open Environ
+open Decl_kinds
 
 (** We introduce here the global environment of the system,
     and we declare it as a synchronized table. *)
@@ -229,6 +230,17 @@ let universes_of_global env r =
 let universes_of_global gr = 
   universes_of_global (env ()) gr
 
+(** Global universe names *)
+type universe_names = 
+  (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
+
+let global_universes =
+  Summary.ref ~name:"Global universe names"
+  ((Idmap.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 env = env() in 
   match r with