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

24 files changed, 377 insertions, 224 deletions

diff --git a/API/API.mli b/API/API.mli
index e320e496c..9d1585d60 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1861,6 +1861,60 @@ end
 (* Modules from intf/                                                   *)
 (************************************************************************)
 
+module Libnames :
+sig
+
+  open Util
+  open Names
+
+  type full_path
+  val pr_path : full_path -> Pp.t
+  val make_path : Names.DirPath.t -> Names.Id.t -> full_path
+  val eq_full_path : full_path -> full_path -> bool
+  val repr_path : full_path -> Names.DirPath.t * Names.Id.t
+  val dirpath : full_path -> Names.DirPath.t
+  val path_of_string : string -> full_path
+
+  type qualid
+  val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid
+  val qualid_eq : qualid -> qualid -> bool
+  val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t
+  val pr_qualid : qualid -> Pp.t
+  val string_of_qualid : qualid -> string
+  val qualid_of_string : string -> qualid
+  val qualid_of_path : full_path -> qualid
+  val qualid_of_dirpath : Names.DirPath.t -> qualid
+  val qualid_of_ident : Names.Id.t -> qualid
+
+  type reference =
+    | Qualid of qualid Loc.located
+    | Ident of Names.Id.t Loc.located
+  val loc_of_reference : reference -> Loc.t option
+  val qualid_of_reference : reference -> qualid Loc.located
+  val pr_reference : reference -> Pp.t
+
+  val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool
+  val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t
+  val dirpath_of_string : string -> Names.DirPath.t
+  val pr_dirpath : Names.DirPath.t -> Pp.t
+  [@@ocaml.deprecated "Alias for DirPath.print"]
+
+  val string_of_path : full_path -> string
+
+  val basename : full_path -> Names.Id.t
+
+  type object_name = full_path * Names.KerName.t
+  type object_prefix = {
+    obj_dir : DirPath.t;
+    obj_mp  : ModPath.t;
+    obj_sec : DirPath.t;
+  }
+
+  module Dirset : Set.S with type elt = DirPath.t
+  module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
+  module Spmap  : CSig.MapS with type key = full_path
+end
+
 module Misctypes :
 sig
   type evars_flag = bool
@@ -1883,10 +1937,15 @@ sig
     | GSet  (** representation of [Set] literal *)
     | GType of 'a (** representation of [Type] literal *)
 
-  type level_info = Names.Name.t Loc.located option
+  type 'a universe_kind =
+    | UAnonymous
+    | UUnknown
+    | UNamed of 'a
+
+  type level_info = Libnames.reference universe_kind
   type glob_level = level_info glob_sort_gen
 
-  type sort_info = Names.Name.t Loc.located list
+  type sort_info = (Libnames.reference * int) option list
   type glob_sort = sort_info glob_sort_gen
 
   type ('a, 'b) gen_universe_decl = {
@@ -2039,60 +2098,6 @@ sig
   [@@ocaml.deprecated "alias of API.Names"]
 end
 
-module Libnames :
-sig
-
-  open Util
-  open Names
-
-  type full_path
-  val pr_path : full_path -> Pp.t
-  val make_path : Names.DirPath.t -> Names.Id.t -> full_path
-  val eq_full_path : full_path -> full_path -> bool
-  val repr_path : full_path -> Names.DirPath.t * Names.Id.t
-  val dirpath : full_path -> Names.DirPath.t
-  val path_of_string : string -> full_path
-
-  type qualid
-  val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid
-  val qualid_eq : qualid -> qualid -> bool
-  val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t
-  val pr_qualid : qualid -> Pp.t
-  val string_of_qualid : qualid -> string
-  val qualid_of_string : string -> qualid
-  val qualid_of_path : full_path -> qualid
-  val qualid_of_dirpath : Names.DirPath.t -> qualid
-  val qualid_of_ident : Names.Id.t -> qualid
-
-  type reference =
-    | Qualid of qualid Loc.located
-    | Ident of Names.Id.t Loc.located
-  val loc_of_reference : reference -> Loc.t option
-  val qualid_of_reference : reference -> qualid Loc.located
-  val pr_reference : reference -> Pp.t
-
-  val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool
-  val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t
-  val dirpath_of_string : string -> Names.DirPath.t
-  val pr_dirpath : Names.DirPath.t -> Pp.t
-  [@@ocaml.deprecated "Alias for DirPath.print"]
-
-  val string_of_path : full_path -> string
-
-  val basename : full_path -> Names.Id.t
-
-  type object_name = full_path * Names.KerName.t
-  type object_prefix = {
-    obj_dir : DirPath.t;
-    obj_mp  : ModPath.t;
-    obj_sec : DirPath.t;
-  }
-
-  module Dirset : Set.S with type elt = DirPath.t
-  module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
-  module Spmap  : CSig.MapS with type key = full_path
-end
-
 module Globnames :
 sig
 
@@ -2754,10 +2759,10 @@ sig
   type universe_binders
   type universe_opt_subst
   val fresh_inductive_instance : Environ.env -> Names.inductive -> Constr.pinductive Univ.in_universe_context_set
-  val new_Type : Names.DirPath.t -> Constr.types
+  val new_Type : unit -> Constr.types
   val type_of_global : Globnames.global_reference -> Constr.types Univ.in_universe_context_set
   val constr_of_global : Globnames.global_reference -> Constr.t
-  val new_univ_level : Names.DirPath.t -> Univ.Level.t
+  val new_univ_level : unit -> Univ.Level.t
   val new_sort_in_family : Sorts.family -> Sorts.t
   val pr_with_global_universes : Univ.Level.t -> Pp.t
   val pr_universe_opt_subst : universe_opt_subst -> Pp.t
diff --git a/engine/termops.ml b/engine/termops.ml
index 07fe90222..a71bdff31 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -288,6 +288,7 @@ let has_no_evar sigma =
   with Exit -> false
 
 let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
+let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l
 
 let pr_evar_universe_context ctx =
   let open UState in
diff --git a/engine/termops.mli b/engine/termops.mli
index c9a530076..c1600abe8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -271,6 +271,8 @@ val is_Prop : Evd.evar_map -> constr -> bool
 val is_Set : Evd.evar_map -> constr -> bool
 val is_Type : Evd.evar_map -> constr -> bool
 
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference
+
 (** Combinators on judgments *)
 
 val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
diff --git a/engine/uState.ml b/engine/uState.ml
index 4e30640e4..511d55328 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -263,13 +263,15 @@ let constrain_variables diff ctx =
   in
   { ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
   
-
-let pr_uctx_level uctx = 
+let reference_of_level uctx =
   let map, map_rev = uctx.uctx_names in 
     fun l ->
-      try Id.print (Option.get (Univ.LMap.find l map_rev).uname)
+      try Libnames.Ident (Loc.tag @@ Option.get (Univ.LMap.find l map_rev).uname)
       with Not_found | Option.IsNone ->
-        Universes.pr_with_global_universes l
+        Universes.reference_of_level l
+
+let pr_uctx_level uctx l =
+  Libnames.pr_reference (reference_of_level uctx l)
 
 type universe_decl =
   (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
@@ -430,7 +432,7 @@ let emit_side_effects eff u =
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
-  let u = Universes.new_univ_level (Global.current_dirpath ()) in
+  let u = Universes.new_univ_level () in
   let ctx' = Univ.ContextSet.add_universe u ctx in
   let uctx', pred =
     match rigid with
diff --git a/engine/uState.mli b/engine/uState.mli
index 16fba41e0..2c39e85f7 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -154,3 +154,4 @@ val update_sigma_env : t -> Environ.env -> t
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
+val reference_of_level : t -> Univ.Level.t -> Libnames.reference
diff --git a/engine/universes.ml b/engine/universes.ml
index 5ac1bc685..93696b4ca 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -14,10 +14,37 @@ open Constr
 open Environ
 open Univ
 open Globnames
-
-let pr_with_global_universes l =
-  try Id.print (LMap.find l (snd (Global.global_universe_names ())))
-  with Not_found -> Level.pr l
+open Nametab
+
+let reference_of_level l =
+  match Level.name l with
+  | Some (d, n as na)  ->
+     let qid =
+       try Nametab.shortest_qualid_of_universe na
+       with Not_found ->
+         let name = Id.of_string_soft (string_of_int n) in
+         Libnames.make_qualid d name
+     in Libnames.Qualid (Loc.tag @@ qid)
+  | None -> Libnames.Ident (Loc.tag @@ Id.of_string_soft (Level.to_string l))
+
+let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
+
+(** Global universe information outside the kernel, to handle
+    polymorphic universe names in sections that have to be discharged. *)
+
+let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
+
+let add_global_universe u p =
+  match Level.name u with
+  | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
+  | None -> ()
+
+let is_polymorphic l =
+  match Level.name l with
+  | Some n ->
+     (try Nametab.UnivIdMap.find n !universe_map
+      with Not_found -> false)
+  | None -> false
 
 (** Local universe names of polymorphic references *)
 
@@ -53,12 +80,14 @@ let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj
     rebuild_function = (fun x -> x); }
 
 let register_universe_binders ref ubinders =
-  (* Add the polymorphic (section) universes *)
   let open Names in
-  let ubinders = Id.Map.fold (fun id (poly,lvl) ubinders ->
-      if poly then Id.Map.add id lvl ubinders
-      else ubinders)
-      (fst (Global.global_universe_names ())) ubinders
+  (* Add the polymorphic (section) universes *)
+  let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
+    let qid = Nametab.shortest_qualid_of_universe lvl in
+    let level = Level.make (fst lvl) (snd lvl) in
+    if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
+    else ubinders)
+    !universe_map ubinders
   in
   if not (Id.Map.is_empty ubinders)
   then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
@@ -236,14 +265,17 @@ let eq_constr_universes_proj env m n =
     res, !cstrs
 
 (* Generator of levels *)
-let new_univ_level, set_remote_new_univ_level =
+type universe_id = DirPath.t * int
+
+let new_univ_id, set_remote_new_univ_id =
   RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
-    ~build:(fun n -> Univ.Level.make (Global.current_dirpath ()) n)
+    ~build:(fun n -> Global.current_dirpath (), n)
 
-let new_univ_level _ = new_univ_level ()
-  (* Univ.Level.make db (new_univ_level ()) *)
+let new_univ_level () =
+  let dp, id = new_univ_id () in
+  Univ.Level.make dp id
 
-let fresh_level () = new_univ_level (Global.current_dirpath ())
+let fresh_level () = new_univ_level ()
 
 (* TODO: remove *)
 let new_univ dp = Univ.Universe.make (new_univ_level dp)
@@ -251,7 +283,7 @@ let new_Type dp = mkType (new_univ dp)
 let new_Type_sort dp = Type (new_univ dp)
 
 let fresh_universe_instance ctx =
-  let init _ = new_univ_level (Global.current_dirpath ()) in
+  let init _ = new_univ_level () in
   Instance.of_array (Array.init (AUContext.size ctx) init)
 
 let fresh_instance_from_context ctx =
@@ -262,7 +294,7 @@ let fresh_instance_from_context ctx =
 let fresh_instance ctx =
   let ctx' = ref LSet.empty in
   let init _ =
-    let u = new_univ_level (Global.current_dirpath ()) in
+    let u = new_univ_level () in
     ctx' := LSet.add u !ctx'; u
   in
   let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
diff --git a/engine/universes.mli b/engine/universes.mli
index 1401c4ee8..fc9278eb5 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -18,6 +18,13 @@ val is_set_minimization : unit -> bool
 (** Universes *)
 
 val pr_with_global_universes : Level.t -> Pp.t
+val reference_of_level : Level.t -> Libnames.reference
+
+(** Global universe information outside the kernel, to handle
+    polymorphic universes in sections that have to be discharged. *)
+val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+
+val is_polymorphic : Level.t -> bool
 
 (** Local universe name <-> level mapping *)
 
@@ -40,14 +47,17 @@ val universe_binders_with_opt_names : Globnames.global_reference ->
   Univ.Level.t list -> univ_name_list option -> universe_binders
 
 (** The global universe counter *)
-val set_remote_new_univ_level : Level.t RemoteCounter.installer
+type universe_id = DirPath.t * int
+
+val set_remote_new_univ_id : universe_id RemoteCounter.installer
 
 (** Side-effecting functions creating new universe levels. *)
 
-val new_univ_level : DirPath.t -> Level.t
-val new_univ : DirPath.t -> Universe.t
-val new_Type : DirPath.t -> types
-val new_Type_sort : DirPath.t -> Sorts.t
+val new_univ_id : unit -> universe_id
+val new_univ_level : unit -> Level.t
+val new_univ : unit -> Universe.t
+val new_Type : unit -> types
+val new_Type_sort : unit -> Sorts.t
 
 val new_global_univ : unit -> Universe.t in_universe_context_set
 val new_sort_in_family : Sorts.family -> Sorts.t
diff --git a/interp/declare.ml b/interp/declare.ml
index 1b4645aff..8fc959b0f 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -453,28 +453,51 @@ let input_universe_context : universe_context_decl -> Libobject.obj =
 let declare_universe_context poly ctx =
   Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
 
-(* Discharged or not *)
-type universe_decl = polymorphic * Universes.universe_binders
-
-let cache_universes (p, l) =
-  let glob = Global.global_universe_names () in
-  let glob', ctx =
-    Id.Map.fold (fun id lev ((idl,lid),ctx) ->
-        ((Id.Map.add id (p, lev) idl,
-          Univ.LMap.add lev id lid),
-         Univ.ContextSet.add_universe lev ctx))
-      l (glob, Univ.ContextSet.empty)
-  in
-  cache_universe_context (p, ctx);
-  Global.set_global_universe_names glob'
+(** Global universes are not substitutive objects but global objects
+   bound at the *library* or *module* level. The polymorphic flag is
+   used to distinguish universes declared in polymorphic sections, which
+   are discharged and do not remain in scope. *)
+
+type universe_decl = polymorphic * Nametab.universe_id
+
+let add_universe p (dp, i) =
+  let level = Univ.Level.make dp i in
+  let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
+  Global.push_context_set p ctx;
+  Universes.add_global_universe level p;
+  if p then Lib.add_section_context ctx
+
+let check_exists sp =
+  let depth = sections_depth () in
+  let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in
+  if Nametab.exists_universe sp then alreadydeclared (Id.print (basename sp) ++ str " already exists")
+  else ()
 
-let input_universes : universe_decl -> Libobject.obj =
+let cache_universe ((sp, _), (poly, id)) =
+  let () = check_exists sp in
+  let () = Nametab.push_universe (Nametab.Until 1) sp id in
+    add_universe poly id
+
+let load_universe i ((sp, _), (poly, id)) =
+  let () = Nametab.push_universe (Nametab.Until i) sp id in
+  add_universe poly id
+
+let open_universe i ((sp, _), (poly, id)) =
+  let () = Nametab.push_universe (Nametab.Exactly i) sp id in
+  ()(** add_universe p id Necessary ? *)
+
+let input_universe : universe_decl -> Libobject.obj =
   declare_object
     { (default_object "Global universe name state") with
-      cache_function = (fun (na, pi) -> cache_universes pi);
-      load_function = (fun _ (_, pi) -> cache_universes pi);
+      cache_function = cache_universe;
+      load_function = load_universe;
+      open_function = open_universe;
       discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
-      classify_function = (fun a -> Keep a) }
+      subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
+      classify_function = (fun a -> Substitute a) }
+
+let add_universe poly (id, lev) =
+  ignore(Lib.add_leaf id (input_universe (poly, lev)))
 
 let do_universe poly l =
   let in_section = Lib.sections_are_opened () in
@@ -484,11 +507,11 @@ let do_universe poly l =
                    (str"Cannot declare polymorphic universes outside sections")
   in
   let l =
-    List.fold_left (fun acc (l, id) ->
-	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
-              Id.Map.add id lev acc) Id.Map.empty l
+    List.map (fun (l, id) ->
+      let lev = Universes.new_univ_id () in
+      (id, lev)) l
   in
-    Lib.add_anonymous_leaf (input_universes (poly, l))
+  List.iter (add_universe poly) l
 
 type constraint_decl = polymorphic * Univ.constraints
 
@@ -510,20 +533,15 @@ let input_constraints : constraint_decl -> Libobject.obj =
       discharge_function = discharge_constraints;
       classify_function = (fun a -> Keep a) }
 
+let loc_of_glob_level = function
+  | Misctypes.GType (Misctypes.UNamed n) -> Libnames.loc_of_reference n
+  | _ -> None
+
 let do_constraint poly l =
-  let open Misctypes in
   let u_of_id x =
-    match x with
-    | GProp -> Loc.tag (false, Univ.Level.prop)
-    | GSet  -> Loc.tag (false, Univ.Level.set)
-    | GType None | GType (Some (_, Anonymous)) ->
-       user_err ~hdr:"Constraint"
-                     (str "Cannot declare constraints on anonymous universes")
-    | GType (Some (loc, Name id)) ->
-       let names, _ = Global.global_universe_names () in
-       try loc, Id.Map.find id names
-       with Not_found ->
-         user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ Id.print id)
+    let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
+    let loc = loc_of_glob_level x in
+    loc, Universes.is_polymorphic level, level
   in
   let in_section = Lib.sections_are_opened () in
   let () =
@@ -541,7 +559,7 @@ let do_constraint poly l =
                     ++ str "Polymorphic Constraint instead")
   in
   let constraints = List.fold_left (fun acc (l, d, r) ->
-     let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in
+     let ploc, p, lu = u_of_id l and rloc, p', ru = u_of_id r in
      check_poly ?loc:ploc p rloc p';
      Univ.Constraint.add (lu, d, ru) acc)
     Univ.Constraint.empty l
diff --git a/interp/declare.mli b/interp/declare.mli
index d50d37368..31883c9d7 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -87,6 +87,5 @@ val exists_name : Id.t -> bool
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
 val do_universe : polymorphic -> Id.t Loc.located list -> unit
-val do_constraint : polymorphic ->
-  (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
-  unit
+val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
+                    unit
diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index 87484ccd5..33e961419 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -48,13 +48,19 @@ type 'a glob_sort_gen =
   | GProp (** representation of [Prop] literal *)
   | GSet  (** representation of [Set] literal *)
   | GType of 'a (** representation of [Type] literal *)
-type sort_info = Name.t Loc.located list
-type level_info = Name.t Loc.located option
 
-type glob_sort = sort_info glob_sort_gen
+type 'a universe_kind =
+  | UAnonymous
+  | UUnknown
+  | UNamed of 'a
+
+type level_info = Libnames.reference universe_kind
 type glob_level = level_info glob_sort_gen
 type glob_constraint = glob_level * Univ.constraint_type * glob_level
 
+type sort_info = (Libnames.reference * int) option list
+type glob_sort = sort_info glob_sort_gen
+
 (** A synonym of [Evar.t], also defined in Term *)
 
 type existential_key = Evar.t
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 64afb95d5..8cf9028fb 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -192,6 +192,10 @@ module Level = struct
 
   let make m n = make (Level (n, Names.DirPath.hcons m))
 
+  let name u =
+    match data u with
+    | Level (n, d) -> Some (d, n)
+    | _ -> None
 end
 
 (** Level maps *)
@@ -337,19 +341,16 @@ struct
        returning [SuperSame] if they refer to the same level at potentially different
        increments or [SuperDiff] if they are different. The booleans indicate if the
        left expression is "smaller" than the right one in both cases. *)
-    let super (u,n as x) (v,n' as y) =
+    let super (u,n) (v,n') =
       let cmp = Level.compare u v in
 	if Int.equal cmp 0 then SuperSame (n < n')
 	else
-	  match x, y with
-	  | (l,0), (l',0) ->
-	     let open RawLevel in
-	     (match Level.data l, Level.data l' with
-	      | Prop, Prop -> SuperSame false
-	      | Prop, _ -> SuperSame true
-	      | _, Prop -> SuperSame false
-	      | _, _ -> SuperDiff cmp)
-	  | _, _ -> SuperDiff cmp
+          let open RawLevel in
+          match Level.data u, n, Level.data v, n' with
+          | Prop, _, Prop, _ -> SuperSame (n < n')
+          | Prop, 0, _, _ -> SuperSame true
+          | _, _, Prop, 0 -> SuperSame false
+          | _, _, _, _ -> SuperDiff cmp
 
     let to_string (v, n) =
       if Int.equal n 0 then Level.to_string v
@@ -499,6 +500,7 @@ struct
 
   let smartmap = List.smartmap
 
+  let map = List.map
 end
 
 type universe = Universe.t
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
diff --git a/library/global.ml b/library/global.ml
index 43097dc5d..03d7612a4 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. *)
@@ -231,18 +230,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
diff --git a/library/global.mli b/library/global.mli
index 51fe53181..1d68d1082 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -102,13 +102,6 @@ val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option
 val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
 (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
 
-(** Global universe name <-> level mapping *)
-type universe_names = 
-  (Decl_kinds.polymorphic * Univ.Level.t) Id.Map.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 -> ModPath.t
diff --git a/library/nametab.ml b/library/nametab.ml
index 222c4cedc..84225f863 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -302,6 +302,16 @@ module DirTab = Make(DirPath')(GlobDir)
 type dirtab = DirTab.t
 let the_dirtab = ref (DirTab.empty : dirtab)
 
+type universe_id = DirPath.t * int
+
+module UnivIdEqual =
+struct
+  type t = universe_id
+  let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+end
+module UnivTab = Make(FullPath)(UnivIdEqual)
+type univtab = UnivTab.t
+let the_univtab = ref (UnivTab.empty : univtab)
 
 (* Reversed name tables ***************************************************)
 
@@ -318,6 +328,21 @@ let the_modrevtab = ref (MPmap.empty : mprevtab)
 type mptrevtab = full_path MPmap.t
 let the_modtyperevtab = ref (MPmap.empty : mptrevtab)
 
+module UnivIdOrdered =
+struct
+  type t = universe_id
+  let hash (d, i) = i + DirPath.hash d
+  let compare (d, i) (d', i') =
+    let c = Int.compare i i' in
+    if Int.equal c 0 then DirPath.compare d d'
+    else c
+end
+
+module UnivIdMap = HMap.Make(UnivIdOrdered)
+
+type univrevtab = full_path UnivIdMap.t
+let the_univrevtab = ref (UnivIdMap.empty : univrevtab)
+
 (* Push functions *********************************************************)
 
 (* This is for permanent constructions (never discharged -- but with
@@ -362,6 +387,11 @@ let push_dir vis dir dir_ref =
   | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab
   | _ -> ()
 
+(* This is for global universe names *)
+
+let push_universe vis sp univ =
+  the_univtab := UnivTab.push vis sp univ !the_univtab;
+  the_univrevtab := UnivIdMap.add univ sp !the_univrevtab
 
 (* Locate functions *******************************************************)
 
@@ -382,6 +412,8 @@ let locate_syndef qid = match locate_extended qid with
 let locate_modtype qid = MPTab.locate qid !the_modtypetab
 let full_name_modtype qid = MPTab.user_name qid !the_modtypetab
 
+let locate_universe qid = UnivTab.locate qid !the_univtab
+
 let locate_dir qid = DirTab.locate qid !the_dirtab
 
 let locate_module qid =
@@ -447,6 +479,8 @@ let exists_module = exists_dir
 
 let exists_modtype sp = MPTab.exists sp !the_modtypetab
 
+let exists_universe kn = UnivTab.exists kn !the_univtab
+
 (* Reverse locate functions ***********************************************)
 
 let path_of_global ref =
@@ -469,6 +503,9 @@ let dirpath_of_module mp =
 let path_of_modtype mp =
   MPmap.find mp !the_modtyperevtab
 
+let path_of_universe mp =
+  UnivIdMap.find mp !the_univrevtab
+
 (* Shortest qualid functions **********************************************)
 
 let shortest_qualid_of_global ctx ref =
@@ -490,6 +527,10 @@ let shortest_qualid_of_modtype kn =
   let sp = MPmap.find kn !the_modtyperevtab in
     MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab
 
+let shortest_qualid_of_universe kn =
+  let sp = UnivIdMap.find kn !the_univrevtab in
+    UnivTab.shortest_qualid Id.Set.empty sp !the_univtab
+
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as e ->
@@ -508,24 +549,28 @@ let global_inductive r =
 (********************************************************************)
 (* Registration of tables as a global table and rollback            *)
 
-type frozen = ccitab * dirtab * mptab
-    * globrevtab * mprevtab * mptrevtab
+type frozen = ccitab * dirtab * mptab * univtab
+    * globrevtab * mprevtab * mptrevtab * univrevtab
 
 let freeze _ : frozen =
   !the_ccitab,
   !the_dirtab,
   !the_modtypetab,
+  !the_univtab,
   !the_globrevtab,
   !the_modrevtab,
-  !the_modtyperevtab
+  !the_modtyperevtab,
+  !the_univrevtab
 
-let unfreeze (ccit,dirt,mtyt,globr,modr,mtyr) =
+let unfreeze (ccit,dirt,mtyt,univt,globr,modr,mtyr,univr) =
   the_ccitab := ccit;
   the_dirtab := dirt;
   the_modtypetab := mtyt;
+  the_univtab := univt;
   the_globrevtab := globr;
   the_modrevtab := modr;
-  the_modtyperevtab := mtyr
+  the_modtyperevtab := mtyr;
+  the_univrevtab := univr
 
 let _ =
   Summary.declare_summary "names"
diff --git a/library/nametab.mli b/library/nametab.mli
index c02447a7c..77fafa100 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -78,6 +78,12 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
 
+type universe_id = DirPath.t * int
+
+module UnivIdMap : CMap.ExtS with type key = universe_id
+
+val push_universe : visibility -> full_path -> universe_id -> unit
+
 (** {6 The following functions perform globalization of qualified names } *)
 
 (** These functions globalize a (partially) qualified name or fail with
@@ -91,6 +97,7 @@ val locate_modtype : qualid -> ModPath.t
 val locate_dir : qualid -> global_dir_reference
 val locate_module : qualid -> ModPath.t
 val locate_section : qualid -> DirPath.t
+val locate_universe : qualid -> universe_id
 
 (** These functions globalize user-level references into global
    references, like [locate] and co, but raise a nice error message
@@ -119,6 +126,7 @@ val exists_modtype : full_path -> bool
 val exists_dir : DirPath.t -> bool
 val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
 val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
+val exists_universe : full_path -> bool
 
 (** {6 These functions locate qualids into full user names } *)
 
@@ -138,6 +146,10 @@ val path_of_global : global_reference -> full_path
 val dirpath_of_module : ModPath.t -> DirPath.t
 val path_of_modtype : ModPath.t -> full_path
 
+(** A universe_id might not be registered with a corresponding user name.
+    @raise Not_found if the universe was not introduced by the user. *)
+val path_of_universe : universe_id -> full_path
+
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
 
@@ -158,6 +170,7 @@ val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid
 val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ModPath.t -> qualid
 val shortest_qualid_of_module : ModPath.t -> qualid
+val shortest_qualid_of_universe : universe_id -> qualid
 
 (** Deprecated synonyms *)
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 7e5933cea..0cf96d487 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -155,9 +155,15 @@ GEXTEND Gram
       | "Type" -> Sorts.InType
       ] ]
   ;
+  universe_expr:
+    [ [ id = global; "+"; n = natural -> Some (id,n)
+      | id = global -> Some (id,0)
+      | "_" -> None
+    ] ]
+  ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids
-      | id = name -> [id]
+    [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> ids
+      | u = universe_expr -> [u]
       ] ]
   ;
   lconstr:
@@ -307,8 +313,9 @@ GEXTEND Gram
   universe_level:
     [ [ "Set" -> GSet
       | "Prop" -> GProp
-      | "Type" -> GType None
-      | id = name -> GType (Some id)
+      | "Type" -> GType UUnknown
+      | "_" -> GType UAnonymous
+      | id = global -> GType (UNamed id)
       ] ]
   ;
   fix_constr:
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 337510ef1..0d491d92b 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -155,7 +155,7 @@ let mk_list univ typ l =
   loop l
 
 let mk_plist = 
-  let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in
+  let type1lev = Universes.new_univ_level () in
     fun l -> mk_list type1lev mkProp l
 
 let mk_list = mk_list Univ.Level.set
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0d1e401d9..6527ba935 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -414,15 +414,17 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       let eqnl = detype_eqns constructs constagsl bl in
       GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
+let detype_universe sigma u =
+  let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in
+  Univ.Universe.map fn u
+
 let detype_sort sigma = function
   | Prop Null -> GProp
   | Prop Pos -> GSet
   | Type u ->
     GType
       (if !print_universes
-       then
-         let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in
-         [Loc.tag @@ Name.mk_name (Id.of_string_soft u)]
+       then detype_universe sigma u
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -434,8 +436,8 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in
-  GType (Some (Loc.tag @@ Name.mk_name (Id.of_string_soft l)))
+  let l = Termops.reference_of_level sigma l in
+  GType (UNamed l)
 
 let detype_instance sigma l = 
   let l = EInstance.kind sigma l in
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index bc563b46d..f0cb8fd1f 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,7 +30,8 @@ let smartmap_cast_type f c =
 let glob_sort_eq g1 g2 = match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
-| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2
+| GType l1, GType l2 ->
+   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
 | _ -> false
 
 let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 00c254dbe..b930c5db8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -177,61 +177,77 @@ let _ =
 	    optwrite = (:=) Universes.set_minimization })
 
 (** Miscellaneous interpretation functions *)
-let interp_known_universe_level evd id =
+
+let interp_known_universe_level evd r =
+  let loc, qid = Libnames.qualid_of_reference r in
   try
-    let level = Evd.universe_of_name evd id in
-    level
+    match r with
+    | Libnames.Ident (loc, id) -> Evd.universe_of_name evd id
+    | Libnames.Qualid _ -> raise Not_found
   with Not_found ->
-    let names, _ = Global.global_universe_names () in
-    snd (Id.Map.find id names)
-
-let interp_universe_level_name ~anon_rigidity evd (loc, s) =
-  match s with
-  | Anonymous ->
-     new_univ_level_variable ?loc anon_rigidity evd
-  | Name id ->
-     let s = Id.to_string id in
-     if CString.string_contains ~where:s ~what:"." then
-       match List.rev (CString.split '.' s) with
-       | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".")
-       | n :: dp ->
-	  let num = int_of_string n in
-	  let dp = DirPath.make (List.map Id.of_string dp) in
-	  let level = Univ.Level.make dp num in
-	  let evd =
-	    try Evd.add_global_univ evd level
-	    with UGraph.AlreadyDeclared -> evd
-	  in evd, level
-     else
-       try evd, interp_known_universe_level evd id
-       with Not_found ->
-         if not (is_strict_universe_declarations ()) then
-           new_univ_level_variable ?loc ~name:id univ_rigid evd
-         else user_err ?loc ~hdr:"interp_universe_level_name"
-             (Pp.(str "Undeclared universe: " ++ str s))
+    let univ, k = Nametab.locate_universe qid in
+    Univ.Level.make univ k
+
+let interp_universe_level_name ~anon_rigidity evd r =
+  try evd, interp_known_universe_level evd r
+  with Not_found ->
+    match r with (* Qualified generated name *)
+    | Libnames.Qualid (loc, qid) ->
+       let dp, i = Libnames.repr_qualid qid in
+       let num =
+         try int_of_string (Id.to_string i)
+         with Failure _ ->
+           user_err ?loc ~hdr:"interp_universe_level_name"
+                    (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r))
+       in
+       let level = Univ.Level.make dp num in
+       let evd =
+         try Evd.add_global_univ evd level
+         with UGraph.AlreadyDeclared -> evd
+       in evd, level
+    | Libnames.Ident (loc, id) -> (* Undeclared *)
+        if not (is_strict_universe_declarations ()) then
+          new_univ_level_variable ?loc ~name:id univ_rigid evd
+        else user_err ?loc ~hdr:"interp_universe_level_name"
+                      (Pp.(str "Undeclared universe: " ++ Id.print id))
 
 let interp_universe ?loc evd = function
   | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
 	    evd, Univ.Universe.make l
   | l ->
-    List.fold_left (fun (evd, u) l -> 
-        (* [univ_flexible_alg] can produce algebraic universes in terms *)
-        let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in
-	(evd', Univ.sup u (Univ.Universe.make l)))
+    List.fold_left (fun (evd, u) l ->
+      let evd', u' =
+        match l with
+        | Some (l,n) ->
+           (* [univ_flexible_alg] can produce algebraic universes in terms *)
+           let anon_rigidity = univ_flexible in
+           let evd', l = interp_universe_level_name ~anon_rigidity evd l in
+           let u' = Univ.Universe.make l in
+           (match n with
+            | 0 -> evd', u'
+            | 1 -> evd', Univ.Universe.super u'
+            | _ ->
+               user_err ?loc ~hdr:"interp_universe"
+                        (Pp.(str "Cannot interpret universe increment +" ++ int n)))
+        | None ->
+           let evd, l = new_univ_level_variable ?loc univ_flexible evd in
+           evd, Univ.Universe.make l
+      in (evd', Univ.sup u u'))
     (evd, Univ.Universe.type0m) l
 
 let interp_known_level_info ?loc evd = function
-  | None | Some (_, Anonymous) ->
+  | UUnknown | UAnonymous ->
     user_err ?loc ~hdr:"interp_known_level_info"
       (str "Anonymous universes not allowed here.")
-  | Some (loc, Name id) ->
-    try interp_known_universe_level evd id
+  | UNamed ref ->
+    try interp_known_universe_level evd ref
     with Not_found ->
-      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Id.print id)
+      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref)
 
 let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
-  | None -> new_univ_level_variable ?loc univ_rigid evd
-  | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s)
+  | UUnknown -> new_univ_level_variable ?loc univ_rigid evd
+  | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd
+  | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s
 
 type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index bce5710d6..2abbc389f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -150,10 +150,15 @@ let tag_var = tag Tag.variable
 
   let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c)
 
+  let pr_univ_expr = function
+    | Some (x,n) ->
+       pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+    | None -> str"_"
+
   let pr_univ l =
     match l with
-      | [_,x] -> Name.print x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")"
+      | [x] -> pr_univ_expr x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") pr_univ_expr l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -166,8 +171,9 @@ let tag_var = tag Tag.variable
   let pr_glob_level = function
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
-    | GType None -> tag_type (str "Type")
-    | GType (Some (_, u)) -> tag_type (Name.print u)
+    | GType UUnknown -> tag_type (str "Type")
+    | GType UAnonymous -> tag_type (str "_")
+    | GType (UNamed u) -> tag_type (pr_reference u)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -192,8 +198,9 @@ let tag_var = tag Tag.variable
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some (_,u) -> Name.print u
-        | None -> tag_type (str "Type"))
+        | UNamed u -> pr_reference u
+        | UAnonymous -> tag_type (str "Type")
+        | UUnknown -> tag_type (str "_"))
 
   let pr_universe_instance l =
     pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 4662c5543..cd22a7183 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -58,7 +58,7 @@ module Make(T : Task) () = struct
   type request = Request of T.request
 
   type more_data =
-    | MoreDataUnivLevel of Univ.Level.t list
+    | MoreDataUnivLevel of Universes.universe_id list
 
   let slave_respond (Request r) =
     let res = T.perform r in
@@ -169,8 +169,7 @@ module Make(T : Task) () = struct
         | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno
         | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in
     let more_univs n =
-      CList.init n (fun _ ->
-        Universes.new_univ_level (Global.current_dirpath ())) in
+      CList.init n (fun _ -> Universes.new_univ_id ()) in
 
     let rec kill_if () =
       if not (Worker.is_alive proc) then ()
@@ -309,7 +308,7 @@ module Make(T : Task) () = struct
       Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
     ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x));
     (* We ask master to allocate universe identifiers *)
-    Universes.set_remote_new_univ_level (bufferize (fun () ->
+    Universes.set_remote_new_univ_id (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
       match unmarshal_more_data (Option.get !slave_ic) with
       | MoreDataUnivLevel l -> l));
diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v
index a96a13700..c069b2d9d 100644
--- a/test-suite/bugs/closed/4390.v
+++ b/test-suite/bugs/closed/4390.v
@@ -8,16 +8,16 @@ Universe i.
 End foo.
 End M.
 
-Check Type@{i}.
+Check Type@{M.i}.
 (* Succeeds *)
 
 Fail Check Type@{j}.
 (* Error: Undeclared universe: j *)
 
-Definition foo@{j} : Type@{i} := Type@{j}.
+Definition foo@{j} : Type@{M.i} := Type@{j}.
 (* ok *)
 End A.
-
+Import A. Import M.
 Set Universe Polymorphism.
 Fail Universes j.
 Monomorphic Universe j.