Proper nametab handling of global universe names

They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced

1 files changed, 4 insertions, 0 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
index c06ce2446..f74f29b2c 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -45,6 +45,8 @@ sig
   val var : int -> t
 
   val var_index : t -> int option
+
+  val name : t -> (Names.DirPath.t * int) option
 end
 
 type universe_level = Level.t
@@ -121,6 +123,8 @@ sig
 
   val exists : (Level.t * int -> bool) -> t -> bool
   val for_all : (Level.t * int -> bool) -> t -> bool
+
+  val map : (Level.t * int -> 'a) -> t -> 'a list
 end
 
 type universe = Universe.t