Merge PR #890: Global universe declarations

43 files changed, 727 insertions, 311 deletions

diff --git a/API/API.mli b/API/API.mli
index e320e496c..6227f17c6 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
@@ -4842,17 +4847,16 @@ sig
       set : unit -> unit ;
       reset : unit -> unit
     }
-  type proof_universes = UState.t * Universes.universe_binders option
   type proof_object = {
     id : Names.Id.t;
     entries : Safe_typing.private_constants Entries.definition_entry list;
     persistence : Decl_kinds.goal_kind;
-    universes: proof_universes;
+    universes: UState.t;
   }
 
   type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
-                  proof_universes
+                  UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
@@ -5006,7 +5010,7 @@ sig
       Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
       Proof.t -> Proof.t * bool
   val cook_proof :
-    unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind))
+    unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * UState.t * Decl_kinds.goal_kind))
 
   val get_current_context : unit -> Evd.evar_map * Environ.env
   val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types
diff --git a/CHANGES b/CHANGES
index 4c83b7c19..da346c04d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -22,10 +22,20 @@ Tactics
   contain proofs.
 
 Vernacular Commands
+
 - The deprecated Coercion Local, Open Local Scope, Notation Local syntax
   was removed. Use Local as a prefix instead.
 
+Universes
+
+- Qualified naming of global universes now works like other namespaced
+  objects (e.g. constants), with a separate namespace, inside and across
+  module and library boundaries. Global universe names introduced in an
+  inductive / constant / Let declaration get qualified with the name of
+  the declaration.
+
 Checker
+
 - The checker now accepts filenames in addition to logical paths.
 
 Changes from 8.7+beta2 to 8.7.0
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 75fac9454..a1a6a4391 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -285,8 +285,10 @@ universes and explicitly instantiate polymorphic definitions.
   \label{UniverseCmd}}
 
 In the monorphic case, this command declares a new global universe named
-{\ident}. It supports the polymorphic flag only in sections, meaning the
-universe quantification will be discharged on each section definition
+{\ident}, which can be referred to using its qualified name as
+well. Global universe names live in a separate namespace. The command
+supports the polymorphic flag only in sections, meaning the universe
+quantification will be discharged on each section definition
 independently. One cannot mix polymorphic and monomorphic declarations
 in the same section.
 
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index afdceae06..ea098902a 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -645,6 +645,24 @@ let eq_constr_universes_proj env sigma m n =
     let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
+let universes_of_constr sigma c =
+  let open Univ in
+  let rec aux s c =
+    match kind sigma c with
+    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
+      LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+    | Sort u ->
+       let sort = ESorts.kind sigma u in
+       if Sorts.is_small sort then s
+       else
+         let u = Sorts.univ_of_sort sort in
+         LSet.fold LSet.add (Universe.levels u) s
+    | Evar (k, args) ->
+       let concl = Evd.evar_concl (Evd.find sigma k) in
+       fold sigma aux (aux s (of_constr concl)) c
+    | _ -> fold sigma aux s c
+  in aux LSet.empty c
+
 open Context
 open Environ
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e9ef302cf..3e6a13f70 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -201,6 +201,10 @@ val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a ->
 val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
 val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
+(** Gather the universes transitively used in the term, including in the
+   type of evars appearing in it. *)
+val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
+
 (** {6 Substitutions} *)
 
 module Vars :
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..1aeb67afb 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -453,28 +453,95 @@ 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)
+(** 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_source =
+  | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *)
+  | QualifiedUniv of Id.t (* global universe introduced by some global value *)
+  | UnqualifiedUniv (* other global universe *)
+
+type universe_decl = universe_source * Nametab.universe_id
+
+let add_universe src (dp, i) =
+  let level = Univ.Level.make dp i in
+  let optpoly = match src with
+    | BoundUniv -> Some true
+    | UnqualifiedUniv -> Some false
+    | QualifiedUniv _ -> None
   in
-  cache_universe_context (p, ctx);
-  Global.set_global_universe_names glob'
+  Option.iter (fun poly ->
+      let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
+      Global.push_context_set poly ctx;
+      Universes.add_global_universe level poly;
+      if poly then Lib.add_section_context ctx)
+    optpoly
 
-let input_universes : universe_decl -> Libobject.obj =
+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 (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
+  else ()
+
+let qualify_univ src (sp,i as orig) =
+  match src with
+  | BoundUniv | UnqualifiedUniv -> orig
+  | QualifiedUniv l ->
+    let sp0, id = Libnames.repr_path sp in
+    let sp0 = DirPath.repr sp0 in
+    Libnames.make_path (DirPath.make (l::sp0)) id, i+1
+
+let cache_universe ((sp, _), (src, id)) =
+  let sp, i = qualify_univ src (sp,1) in
+  let () = check_exists sp in
+  let () = Nametab.push_universe (Nametab.Until i) sp id in
+    add_universe src id
+
+let load_universe i ((sp, _), (src, id)) =
+  let sp, i = qualify_univ src (sp,i) in
+  let () = Nametab.push_universe (Nametab.Until i) sp id in
+  add_universe src id
+
+let open_universe i ((sp, _), (src, id)) =
+  let sp, i = qualify_univ src (sp,i) in
+  let () = Nametab.push_universe (Nametab.Exactly i) sp id in
+  ()
+
+let discharge_universe = function
+  | _, (BoundUniv, _) -> None
+  | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
+
+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);
-      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
-      classify_function = (fun a -> Keep a) }
+      cache_function = cache_universe;
+      load_function = load_universe;
+      open_function = open_universe;
+      discharge_function = discharge_universe;
+      subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
+      classify_function = (fun a -> Substitute a) }
+
+let declare_univ_binders gr pl =
+  if Global.is_polymorphic gr then
+    Universes.register_universe_binders gr pl
+  else
+    let l = match gr with
+      | ConstRef c -> Label.to_id @@ Constant.label c
+      | IndRef (c, _) -> Label.to_id @@ MutInd.label c
+      | VarRef id -> id
+      | ConstructRef _ ->
+        anomaly ~label:"declare_univ_binders"
+          Pp.(str "declare_univ_binders on an constructor reference")
+    in
+    Id.Map.iter (fun id lvl ->
+        match Univ.Level.name lvl with
+        | None -> ()
+        | Some na ->
+          ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na))))
+      pl
 
 let do_universe poly l =
   let in_section = Lib.sections_are_opened () in
@@ -484,11 +551,14 @@ 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))
+  let src = if poly then BoundUniv else UnqualifiedUniv in
+  List.iter (fun (id,lev) ->
+      ignore(Lib.add_leaf id (input_universe (src, lev))))
+    l
 
 type constraint_decl = polymorphic * Univ.constraints
 
@@ -510,20 +580,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 +606,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..f368d164e 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -80,13 +80,11 @@ val recursive_message : bool (** true = fixpoint *) ->
 
 val exists_name : Id.t -> bool
 
-
-
 (** Global universe contexts, names and constraints *)
+val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit
 
 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/proofs/pfedit.ml b/proofs/pfedit.ml
index c526ae000..31a73db04 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -140,7 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
     Proof_global.discard_current ();
-    const, status, fst univs
+    const, status, univs
   with reraise ->
     let reraise = CErrors.push reraise in
     Proof_global.discard_current ();
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 2acb678d7..5a317a956 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -35,11 +35,11 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
 
 (** {6 ... } *)
 (** [get_goal_context n] returns the context of the [n]th subgoal of
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index c1e1c2eda..535ef2013 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,17 +68,16 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_universes = UState.t * Universes.universe_binders option
 
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  universes: proof_universes;
+  universes: UState.t;
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
@@ -333,7 +332,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
-  let binders = if poly then Some (UState.universe_binders universes) else None in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
@@ -409,7 +407,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   in
   let entries = Future.map2 entry_fn fpl initial_goals in
   { id = pid; entries = entries; persistence = strength;
-    universes = (universes, binders) },
+    universes },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
 let return_proof ?(allow_partial=false) () =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 059459042..27e99f218 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -37,18 +37,17 @@ val compact_the_proof : unit -> unit
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-type proof_universes = UState.t * Universes.universe_binders option
 
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  universes: proof_universes;
+  universes: UState.t;
 }
 
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
-		  proof_universes
+                UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
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.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index f69379a57..d6d410d1a 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -44,26 +44,45 @@ bar@{u} = nat
 bar is universe polymorphic
 foo@{u Top.17 v} = 
 Type@{Top.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1, Top.17+1, v+1)}
+     : Type@{max(u+1,Top.17+1,v+1)}
 (* u Top.17 v |=  *)
 
 foo is universe polymorphic
-Monomorphic mono = Type@{u}
-     : Type@{u+1}
-(* {u} |=  *)
+Monomorphic mono = Type@{mono.u}
+     : Type@{mono.u+1}
+(* {mono.u} |=  *)
 
 mono is not universe polymorphic
+mono
+     : Type@{mono.u+1}
+Type@{mono.u}
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+monomono
+     : Type@{MONOU+1}
+mono.monomono
+     : Type@{mono.MONOU+1}
+monomono
+     : Type@{MONOU+1}
+mono
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+bobmorane = 
+let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
+     : Type@{max(tt.u,ff.u)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
-     : Type@{max(E+1, M+1, N+1)}
+     : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
 
 foo is universe polymorphic
 foo@{Top.16 Top.17 Top.18} = 
 Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
-     : Type@{max(Top.16+1, Top.17+1, Top.18+1)}
+     : Type@{max(Top.16+1,Top.17+1,Top.18+1)}
 (* Top.16 Top.17 Top.18 |=  *)
 
 foo is universe polymorphic
@@ -88,9 +107,10 @@ The command has indeed failed with message:
 This object does not support universe names.
 The command has indeed failed with message:
 Cannot enforce v < u because u < gU < gV < v
-Monomorphic bind_univs.mono = Type@{u}
-     : Type@{u+1}
-(* {u} |=  *)
+Monomorphic bind_univs.mono = 
+Type@{bind_univs.mono.u}
+     : Type@{bind_univs.mono.u+1}
+(* {bind_univs.mono.u} |=  *)
 
 bind_univs.mono is not universe polymorphic
 bind_univs.poly@{u} = Type@{u}
@@ -99,12 +119,12 @@ bind_univs.poly@{u} = Type@{u}
 
 bind_univs.poly is universe polymorphic
 insec@{v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* v |=  *)
 
 insec is universe polymorphic
 insec@{u v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
@@ -125,28 +145,28 @@ inmod@{u} = Type@{u}
 inmod is universe polymorphic
 Applied.infunct@{u v} = 
 inmod@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i}
-(* i Top.33 Top.34 |=  *)
+axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i}
-(* i Top.33 Top.34 |=  *)
+axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.36} -> Type@{i}
+axfoo' : Type@{Top.44} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.36} -> Type@{i}
+axbar' : Type@{Top.44} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 116d5e5e9..266d94ad9 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,6 +1,6 @@
 Set Universe Polymorphism.
 Set Printing Universes.
-Unset Strict Universe Declaration.
+(* Unset Strict Universe Declaration. *)
 
 (* universe binders on inductive types and record projections *)
 Inductive Empty@{u} : Type@{u} := .
@@ -25,14 +25,59 @@ Print wrap.
 Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
 Print bar.
 
+Unset Strict Universe Declaration.
 (* The universes in the binder come first, then the extra universes in
    order of appearance. *)
 Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
 Print foo.
+Set Strict Universe Declaration.
 
 (* Binders even work with monomorphic definitions! *)
 Monomorphic Definition mono@{u} := Type@{u}.
 Print mono.
+Check mono.
+Check Type@{mono.u}.
+
+Module mono.
+  Fail Monomorphic Universe u.
+  Monomorphic Universe MONOU.
+
+  Monomorphic Definition monomono := Type@{MONOU}.
+  Check monomono.
+End mono.
+Check mono.monomono. (* qualified MONOU *)
+Import mono.
+Check monomono. (* unqualified MONOU *)
+Check mono. (* still qualified mono.u *)
+
+Monomorphic Constraint Set < Top.mono.u.
+
+Module mono2.
+  Monomorphic Universe u.
+End mono2.
+
+Fail Monomorphic Definition mono2@{u} := Type@{u}.
+
+Module SecLet.
+  Unset Universe Polymorphism.
+  Section foo.
+    (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
+    Unset Strict Universe Declaration.
+    Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
+    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *)
+    Definition bobmorane := tt -> ff.
+  End foo.
+  Print bobmorane. (*
+                     bobmorane@{Top.15 Top.16 ff.u ff.v} =
+                     let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff
+                     : Type@{max(Top.15,ff.u)}
+                     (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15
+                     ff.v < ff.u
+                    *)
+
+                    bobmorane is universe polymorphic
+                    *)
+End SecLet.
 
 (* fun x x => foo is nonsense with local binders *)
 Fail Definition fo@{u u} := Type@{u}.
@@ -61,7 +106,7 @@ Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
 Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
 
 (* Universe binders survive through compilation, sections and modules. *)
-Require bind_univs.
+Require TestSuite.bind_univs.
 Print bind_univs.mono.
 Print bind_univs.poly.
 
diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v
index f17c00e9d..e834fde11 100644
--- a/test-suite/prerequisite/bind_univs.v
+++ b/test-suite/prerequisite/bind_univs.v
@@ -3,3 +3,5 @@
 Monomorphic Definition mono@{u} := Type@{u}.
 
 Polymorphic Definition poly@{u} := Type@{u}.
+
+Monomorphic Universe reqU.
diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v
new file mode 100644
index 000000000..c4a1d7c28
--- /dev/null
+++ b/test-suite/success/unidecls.v
@@ -0,0 +1,121 @@
+Set Printing Universes.
+
+Module unidecls.
+  Universes a b.
+End unidecls.
+
+Universe a.
+
+Constraint a < unidecls.a.
+
+Print Universes.
+
+(** These are different universes *)
+Check Type@{a}.
+Check Type@{unidecls.a}.
+
+Check Type@{unidecls.b}.
+
+Fail Check Type@{unidecls.c}.
+
+Fail Check Type@{i}.
+Universe foo.
+Module Foo.
+  (** Already declared globaly: but universe names are scoped at the module level  *)
+  Universe foo.
+  Universe bar.
+
+  Check Type@{Foo.foo}.
+  Definition bar := 0.
+End Foo.
+
+(** Already declared in the module *)
+Universe bar.
+
+(** Accessible outside the module: universe declarations are global *)
+Check Type@{bar}.
+Check Type@{Foo.bar}.
+
+Check Type@{Foo.foo}.
+(** The same *)
+Check Type@{foo}.
+Check Type@{Top.foo}.
+
+Universe secfoo.
+Section Foo'.
+  Fail Universe secfoo.
+  Universe secfoo2.
+  Check Type@{Foo'.secfoo2}.
+  Constraint secfoo2 < a.
+End Foo'.
+
+Check Type@{secfoo2}.
+Fail Check Type@{Foo'.secfoo2}.
+Fail Check eq_refl : Type@{secfoo2} = Type@{a}.
+
+(** Below, u and v are global, fixed universes *)
+Module Type Arg.
+  Universe u.
+  Parameter T: Type@{u}.
+End Arg.
+
+Module Fn(A : Arg).
+  Universes v.
+
+  Check Type@{A.u}.
+  Constraint A.u < v.
+
+  Definition foo : Type@{v} := nat.
+  Definition bar : Type@{A.u} := nat.
+
+  Fail Definition foo(A : Type@{v}) : Type@{A.u} := A.
+End Fn.
+
+Module ArgImpl : Arg.
+  Definition T := nat.
+End ArgImpl.
+
+Module ArgImpl2 : Arg.
+  Definition T := bool.
+End ArgImpl2.
+
+(** Two applications of the functor result in the exact same universes *)
+Module FnApp := Fn(ArgImpl).
+
+Check Type@{FnApp.v}.
+Check FnApp.foo.
+Check FnApp.bar.
+
+Check (eq_refl : Type@{ArgImpl.u} = Type@{ArgImpl2.u}).
+
+Module FnApp2 := Fn(ArgImpl).
+Check Type@{FnApp2.v}.
+Check FnApp2.foo.
+Check FnApp2.bar.
+
+Import ArgImpl2.
+(** Now u refers to ArgImpl.u and ArgImpl2.u *)
+Check FnApp2.bar.
+
+(** It can be shadowed *)
+Universe u.
+
+(** This refers to the qualified name *)
+Check FnApp2.bar.
+
+Constraint u = ArgImpl.u.
+Print Universes.
+
+Set Universe Polymorphism.
+
+Section PS.
+  Universe poly.
+
+  Definition id (A : Type@{poly}) (a : A) : A := a.
+End PS.
+(** The universe is polymorphic and discharged, does not persist *)
+Fail Check Type@{poly}.
+
+Print Universes.
+Check id nat.
+Check id@{Set}.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b80741269..cb1d2f7c7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -126,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
-    Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm);
+    Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders evm);
     instance_hook k info global imps ?hook (ConstRef kn);
     id
 
@@ -208,7 +208,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
           (ParameterEntry
             (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
         in
-          Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars);
+          Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders !evars);
           instance_hook k pri global imps ?hook (ConstRef cst); id
       end
     else (
diff --git a/vernac/command.ml b/vernac/command.ml
index 01c7f149b..66d4fe984 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -95,7 +95,7 @@ let interp_definition pl bl poly red_option c ctypopt =
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
   let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
   let nb_args = Context.Rel.nhyps ctx in
-  let imps,pl,ce =
+  let imps,ce =
     match ctypopt with
       None ->
         let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -105,11 +105,10 @@ let interp_definition pl bl poly red_option c ctypopt =
 	let c = EConstr.Unsafe.to_constr c in
         let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
         let body = nf (it_mkLambda_or_LetIn c ctx) in
-        let vars = Univops.universes_of_constr body in
-        let evd = Evd.restrict_universe_context !evdref vars in
-        let uctx = Evd.check_univ_decl ~poly evd decl in
-        let binders = Evd.universe_binders evd in
-        imps1@(Impargs.lift_implicits nb_args imps2), binders,
+        let vars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+        let () = evdref := Evd.restrict_universe_context !evdref vars in
+        let uctx = Evd.check_univ_decl ~poly !evdref decl in
+        imps1@(Impargs.lift_implicits nb_args imps2),
           definition_entry ~univs:uctx body
     | Some ctyp ->
         let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
@@ -131,23 +130,22 @@ let interp_definition pl bl poly red_option c ctypopt =
         in
 	if not (try List.for_all chk imps2 with Not_found -> false)
 	then warn_implicits_in_term ();
-        let vars = Univ.LSet.union (Univops.universes_of_constr body) 
-          (Univops.universes_of_constr typ) in
-        let ctx = Evd.restrict_universe_context !evdref vars in
-        let uctx = Evd.check_univ_decl ~poly ctx decl in
-        let binders = Evd.universe_binders evd in
-        imps1@(Impargs.lift_implicits nb_args impsty), binders,
-          definition_entry ~types:typ
-	    ~univs:uctx body
+        let bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+        let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in
+        let vars = Univ.LSet.union bodyvars tyvars in
+        let () = evdref := Evd.restrict_universe_context !evdref vars in
+        let uctx = Evd.check_univ_decl ~poly !evdref decl in
+        imps1@(Impargs.lift_implicits nb_args impsty),
+          definition_entry ~types:typ ~univs:uctx body
   in
-  red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
+  (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps)
 
-let check_definition (ce, evd, _, _, imps) =
+let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd Evd.empty;
   ce
 
 let do_definition ident k univdecl bl red_option c ctypopt hook =
-  let (ce, evd, univdecl, pl', imps as def) =
+  let (ce, evd, univdecl, imps as def) =
     interp_definition univdecl bl (pi2 k) red_option c ctypopt
   in
     if Flags.is_program_mode () then
@@ -168,7 +166,7 @@ let do_definition ident k univdecl bl red_option c ctypopt hook =
       ignore(Obligations.add_definition
           ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(DeclareDef.declare_definition ident k ce pl' imps
+      ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -224,7 +222,7 @@ match local with
   let kn = declare_constant ident ~local decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = Universes.register_universe_binders gr pl in
+  let () = Declare.declare_univ_binders gr pl in
   let () = assumption_message ident in
   let () = if do_instance then Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
@@ -712,7 +710,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
 	      let ind = (mind,i) in
 	      let gr = IndRef ind in
 	      maybe_declare_manual_implicits false gr indimpls;
-	      Universes.register_universe_binders gr pl;
+              Declare.declare_univ_binders gr pl;
 	      List.iteri
 		(fun j impls ->
 		 maybe_declare_manual_implicits false
@@ -1268,7 +1266,7 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive local p fixkind fixl ntns =
+let do_program_recursive local poly fixkind fixl ntns =
   let isfix = fixkind != Obligations.IsCoFixpoint in
   let (env, rec_sign, pl, evd), fix, info = 
     interp_recursive isfix fixl ntns 
@@ -1310,8 +1308,8 @@ let do_program_recursive local p fixkind fixl ntns =
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-  | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
-  | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
+  | Obligations.IsFixpoint _ -> (local, poly, Fixpoint)
+  | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint)
   in
   Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
 
diff --git a/vernac/command.mli b/vernac/command.mli
index 070f3e112..a1f916c78 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -28,7 +28,7 @@ val do_constraint : polymorphic ->
 val interp_definition :
   Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
-                        Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits
+                        Univdecls.universe_decl * Impargs.manual_implicits
 
 val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
   local_binder_expr list -> red_expr option -> constr_expr ->
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 980db4109..dfac78c04 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -36,7 +36,7 @@ let declare_global_definition ident ce local k pl imps =
   let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = Universes.register_universe_binders gr pl in
+  let () = Declare.declare_univ_binders gr pl in
   let () = definition_message ident in
   gr
 
@@ -49,6 +49,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     let () = definition_message ident in
     let gr = VarRef ident in
     let () = maybe_declare_manual_implicits false gr imps in
+    let () = Declare.declare_univ_binders gr pl in
     let () = if Proof_global.there_are_pending_proofs () then
 	       warn_definition_not_visible ident
     in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 42631a15b..200c2260e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -177,7 +177,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
+let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
@@ -204,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
           (locality, ConstRef kn)
     in
     definition_message id;
-    Universes.register_universe_binders r (Option.default Universes.empty_binders pl);
+    Declare.declare_univ_binders r (UState.universe_binders uctx);
     call_hook (fun exn -> exn) hook l r
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
@@ -286,17 +286,17 @@ let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
 let save_named ?export_seff proof =
-  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
-  save ?export_seff id const cstrs pl do_guard persistence hook
+  let id,const,uctx,do_guard,persistence,hook = proof in
+  save ?export_seff id const uctx do_guard persistence hook
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     user_err Pp.(str "This command can only be used for unnamed theorem.")
 
 let save_anonymous ?export_seff proof save_ident =
-  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
+  let id,const,uctx,do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save ?export_seff save_ident const cstrs pl do_guard persistence hook
+  save ?export_seff save_ident const uctx do_guard persistence hook
 
 (* Admitted *)
 
@@ -312,7 +312,7 @@ let admit (id,k,e) pl hook () =
   | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
   in
   let () = assumption_message id in
-  Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl);
+  Declare.declare_univ_binders (ConstRef kn) pl;
   call_hook (fun exn -> exn) hook Global (ConstRef kn)
 
 (* Starting a goal *)
@@ -330,8 +330,8 @@ let get_proof proof do_guard hook opacity =
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in
   make_terminator begin function
-  | Admitted (id,k,pe,(ctx,pl)) ->
-      admit (id,k,pe) pl (hook (Some ctx)) ();
+  | Admitted (id,k,pe,ctx) ->
+      admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) ();
       Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff = match opaque with
@@ -339,7 +339,7 @@ let universe_proof_terminator compute_guard hook =
         | Vernacexpr.Opaque      -> true, false
       in
       let proof = get_proof proof compute_guard
-	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
+        (hook (Some (proof.Proof_global.universes))) is_opaque in
       begin match idopt with
       | None -> save_named ~export_seff proof
       | Some (_,id) -> save_anonymous ~export_seff proof id
@@ -417,7 +417,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
   | (id,(t,(_,imps)))::other_thms ->
       let hook ctx strength ref =
         let ctx = match ctx with
-        | None -> Evd.empty_evar_universe_context
+        | None -> UState.empty
         | Some ctx -> ctx
         in
         let other_thms_data =
@@ -426,9 +426,9 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
             let body,opaq = retrieve_first_recthm ctx ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
-            let ctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
             let body = Option.map norm body in
-            List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
+            let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
+            List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
@@ -496,7 +496,7 @@ let save_proof ?proof = function
             if const_entry_type = None then
               user_err Pp.(str "Admitted requires an explicit statement");
             let typ = Option.get const_entry_type in
-            let ctx = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in
+            let ctx = UState.const_univ_entry ~poly:(pi2 k) universes in
             let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
             Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
         | None ->
@@ -518,12 +518,9 @@ let save_proof ?proof = function
                   Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
               | _ -> None in
 	    let decl = Proof_global.get_universe_decl () in
-            let evd = Evd.from_ctx universes in
             let poly = pi2 k in
-            let ctx = Evd.check_univ_decl ~poly evd decl in
-            let binders = if poly then Some (UState.universe_binders universes) else None in
-            Admitted(id,k,(sec_vars, (typ, ctx), None),
-		     (universes, binders))
+            let ctx = UState.check_univ_decl ~poly universes decl in
+            Admitted(id,k,(sec_vars, (typ, ctx), None), universes)
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1046d68f8..24d664951 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -833,7 +833,7 @@ let obligation_terminator name num guard hook auto pf =
     let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
     let ty = entry.Entries.const_entry_type in
     let (body, cstr), () = Future.force entry.Entries.const_entry_body in
-    let sigma = Evd.from_ctx (fst uctx) in
+    let sigma = Evd.from_ctx uctx in
     let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
     Inductiveops.control_only_guard (Global.env ()) body;
     (** Declare the obligation ourselves and drop the hook *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1d255b08e..1cdc538b5 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -613,7 +613,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
     States.with_state_protection (fun () ->
       typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in
   let sign = structure_signature (fields@params) in
-  match kind with
+  let gr = match kind with
   | Class def ->
      let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
      let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild
@@ -638,3 +638,6 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
 	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
+  in
+  Declare.declare_univ_binders gr pl;
+  gr