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.

8 files changed, 25 insertions, 24 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index 9cc6d9109..53cbbd73e 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,5 +1,6 @@
 Logic_monad
 Namegen
+Universes
 UState
 Evd
 Sigma
diff --git a/library/universes.ml b/engine/universes.ml
index 0ccb6b8d2..6d683b859 100644
--- a/library/universes.ml
+++ b/engine/universes.ml
@@ -15,19 +15,8 @@ open Univ
 open Globnames
 open Decl_kinds
 
-(** 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 pr_with_global_universes l = 
-  try Nameops.pr_id (LMap.find l (snd !global_universes))
+  try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ())))
   with Not_found -> Level.pr l
 
 (** Local universe names of polymorphic references *)
diff --git a/library/universes.mli b/engine/universes.mli
index d3a271b8d..0aeea91cd 100644
--- a/library/universes.mli
+++ b/engine/universes.mli
@@ -17,13 +17,6 @@ val is_set_minimization : unit -> bool
 
 (** Universes *)
 
-(** Global universe name <-> level mapping *)
-type universe_names = 
-  (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
-
-val global_universe_names : unit -> universe_names
-val set_global_universe_names : universe_names -> unit
-
 val pr_with_global_universes : Level.t -> Pp.std_ppcmds
 
 (** Local universe name <-> level mapping *)
diff --git a/library/declare.ml b/library/declare.ml
index 8298ddbc8..31c9c24bc 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -455,7 +455,7 @@ let declare_universe_context poly ctx =
 type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
 
 let cache_universes (p, l) =
-  let glob = Universes.global_universe_names () in
+  let glob = Global.global_universe_names () in
   let glob', ctx =
     List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
         ((Idmap.add id (p, lev) idl,
@@ -464,7 +464,7 @@ let cache_universes (p, l) =
       (glob, Univ.ContextSet.empty) l
   in
   cache_universe_context (p, ctx);
-  Universes.set_global_universe_names glob'
+  Global.set_global_universe_names glob'
 
 let input_universes : universe_decl -> Libobject.obj =
   declare_object
@@ -519,7 +519,7 @@ let do_constraint poly l =
                      (str "Cannot declare constraints on anonymous universes")
     | GType (Some (loc, id)) ->
        let id = Id.of_string id in
-       let names, _ = Universes.global_universe_names () in
+       let names, _ = Global.global_universe_names () in
        try loc, Idmap.find id names
        with Not_found ->
          user_err ~loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id)
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
diff --git a/library/global.mli b/library/global.mli
index 247ca20b4..a4a38ce84 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -96,6 +96,13 @@ val constraints_of_constant_body :
 val universes_of_constant_body :
   Declarations.constant_body -> Univ.universe_context
 
+(** Global universe name <-> level mapping *)
+type universe_names = 
+  (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
+
+val global_universe_names : unit -> universe_names
+val set_global_universe_names : universe_names -> unit
+
 (** {6 Compiled libraries } *)
 
 val start_library : DirPath.t -> module_path
diff --git a/library/library.mllib b/library/library.mllib
index 920657365..df4f73503 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -5,7 +5,6 @@ Libobject
 Summary
 Nametab
 Global
-Universes
 Lib
 Declaremods
 Loadpath
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2f13121ad..8f369a811 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -188,7 +188,7 @@ let _ =
 						  
 (** Miscellaneous interpretation functions *)
 let interp_universe_level_name evd (loc,s) =
-  let names, _ = Universes.global_universe_names () in
+  let names, _ = Global.global_universe_names () in
     if CString.string_contains s "." then
       match List.rev (CString.split '.' s) with
       | [] -> anomaly (str"Invalid universe name " ++ str s)