From 3e275d4bd1c3eb002b68c36ab116e5ab687d52f3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 4 Dec 2018 10:33:47 +0100
Subject: Fix race condition triggered by fresh universe generation

Remote counters were trying to build universe levels (as opposed to
simple integers), but did not have access to the right dirpath at
construction time. We fix it by constructing the level only at use time,
and we introduce some abstractions for qualified and unqualified level
names.
---
 checker/values.ml      |  4 ++--
 engine/uState.ml       |  2 +-
 engine/univGen.ml      | 20 ++++++++------------
 engine/univGen.mli     |  8 +++-----
 engine/univNames.ml    |  9 +++++----
 interp/declare.ml      |  6 +++---
 kernel/indtypes.ml     |  2 +-
 kernel/inductive.ml    |  2 +-
 kernel/uGraph.ml       |  2 +-
 kernel/univ.ml         | 50 +++++++++++++++++++++++++++++++++++++++-----------
 kernel/univ.mli        | 31 ++++++++++++++++++++++++++++---
 library/nametab.ml     | 15 +++++----------
 library/nametab.mli    | 12 +++++-------
 pretyping/pretyping.ml |  6 +++---
 stm/asyncTaskQueue.ml  |  2 +-
 15 files changed, 106 insertions(+), 65 deletions(-)

diff --git a/checker/values.ml b/checker/values.ml
index dcb2bca81a..f73e19a972 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -93,9 +93,9 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|]
 
 
 (** kernel/univ *)
-
+let v_level_qualid = v_tuple "Level.Qualid.t" [|v_dp;Int|]
 let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) 
-  [|(*Level*)[|Int;v_dp|]; (*Var*)[|Int|]|]
+  [|(*Level*)[|v_level_qualid|]; (*Var*)[|Int|]|]
 let v_level = v_tuple "level" [|Int;v_raw_level|] 
 let v_expr = v_tuple "levelexpr" [|v_level;Int|]
 let v_univ = List v_expr
diff --git a/engine/uState.ml b/engine/uState.ml
index 6aecc368e6..56b7a16ace 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -533,7 +533,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 = UnivGen.new_univ_level () in
+  let u = UnivGen.fresh_level () in
   let ctx' = Univ.ContextSet.add_universe u ctx in
   let uctx', pred =
     match rigid with
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 130aa06f53..5aa4734b23 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -14,25 +14,21 @@ open Constr
 open Univ
 
 (* Generator of levels *)
-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 -> Global.current_dirpath (), n)
-
-let new_univ_level () =
-  let dp, id = new_univ_id () in
-  Univ.Level.make dp id
+    ~build:(fun n -> Level.Id.make n)
 
-let fresh_level () = new_univ_level ()
+let fresh_level () =
+  let id = new_univ_id () in
+  Univ.Level.make2 (Global.current_dirpath ()) id
 
 (* TODO: remove *)
-let new_univ dp = Univ.Universe.make (new_univ_level dp)
-let new_Type dp = mkType (new_univ dp)
-let new_Type_sort dp = Type (new_univ dp)
+let new_univ () = Univ.Universe.make (fresh_level ())
+let new_Type () = mkType (new_univ ())
+let new_Type_sort () = Type (new_univ ())
 
 let fresh_instance auctx =
-  let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in
+  let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
   let ctx = Array.fold_right LSet.add inst LSet.empty in
   let inst = Instance.of_array inst in
   inst, (ctx, AUContext.instantiate inst auctx)
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 8af5f8fdb0..66e80368a4 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -15,14 +15,12 @@ open Univ
 
 
 (** The global universe counter *)
-type universe_id = DirPath.t * int
-
-val set_remote_new_univ_id : universe_id RemoteCounter.installer
+val set_remote_new_univ_id : Level.Id.t RemoteCounter.installer
 
 (** Side-effecting functions creating new universe levels. *)
 
-val new_univ_id : unit -> universe_id
-val new_univ_level : unit -> Level.t
+val new_univ_id : unit -> Level.Id.t
+val fresh_level : unit -> Level.t
 
 val new_univ : unit -> Universe.t
 [@@ocaml.deprecated "Use [new_univ_level]"]
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 1019f8f0c2..6bf1187b65 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -15,12 +15,13 @@ open Univ
 
 let qualid_of_level l =
   match Level.name l with
-  | Some (d, n as na)  ->
+  | Some qid  ->
     begin
-    try Nametab.shortest_qualid_of_universe na
+    try Nametab.shortest_qualid_of_universe qid
     with Not_found ->
-      let name = Id.of_string_soft (string_of_int n) in
-      Libnames.make_qualid d name
+      let (dp,n) = Level.Qualid.repr qid in
+      let name = Id.of_string_soft (Level.Id.to_string n) in
+      Libnames.make_qualid dp name
     end
   | None ->
     Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
diff --git a/interp/declare.ml b/interp/declare.ml
index 1e972d3e35..0c9d26dd01 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -469,7 +469,7 @@ type universe_source =
   | QualifiedUniv of Id.t (* global universe introduced by some global value *)
   | UnqualifiedUniv (* other global universe *)
 
-type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list
+type universe_name_decl = universe_source * (Id.t * Univ.Level.Qualid.t) list
 
 let check_exists sp =
   if Nametab.exists_universe sp then
@@ -543,9 +543,9 @@ let do_universe poly l =
   let l =
     List.map (fun {CAst.v=id} ->
       let lev = UnivGen.new_univ_id () in
-      (id, lev)) l
+      (id, Univ.Level.Qualid.make (Global.current_dirpath ()) lev)) l
   in
-  let ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx)
+  let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
       Univ.LSet.empty l, Univ.Constraint.empty
   in
   let () = declare_universe_context poly ctx in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a4a02791b4..8efda16d64 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -218,7 +218,7 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
 let check_subtyping cumi paramsctxt env_ar inds = 
     let numparams = Context.Rel.nhyps paramsctxt in
     let uctx = CumulativityInfo.univ_context cumi in
-    let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in
+    let new_levels = Array.init (UContext.size uctx) (fun i -> Level.make2 DirPath.empty (Level.Id.make i)) in
     let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
         LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
     in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9bbcf07f7e..30d96a22e0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -594,7 +594,7 @@ let rec ienv_decompose_prod (env,_ as ienv) n c =
      | _ -> assert false
 
 let lambda_implicit_lift n a =
-  let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in
+  let level = Level.make2 (DirPath.make [Id.of_string "implicit"]) (Level.Id.make 0) in
   let implicit_sort = mkType (Universe.make level) in
   let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
   iterate lambda_implicit n (lift n a)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index afdc8f1511..064fffe98e 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -921,7 +921,7 @@ let sort_universes g =
   let types = Array.init (max_lvl + 1) (function
     | 0 -> Level.prop
     | 1 -> Level.set
-    | n -> Level.make mp (n-2))
+    | n -> Level.make2 mp (Level.Id.make (n-2)))
   in
   let g = Array.fold_left (fun g u ->
     let g, u = safe_repr g u in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 2b3b4f9486..57a5dce8a4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -36,10 +36,35 @@ open Util
 module RawLevel =
 struct
   open Names
+
+  module Id = struct
+    type t = int
+
+    let make i = i
+    let to_string i = string_of_int i
+
+  end
+
+  module Qualid = struct
+    type t = DirPath.t * Id.t
+
+    let make dp i = (dp,i)
+    let repr x = x
+
+    let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+
+    let hash (d,i) = Hashset.Combine.combine 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
+
   type t =
     | Prop
     | Set
-    | Level of int * DirPath.t
+    | Level of Qualid.t
     | Var of int
 
   (* Hash-consing *)
@@ -49,7 +74,7 @@ struct
       match x, y with
       | Prop, Prop -> true
       | Set, Set -> true
-      | Level (n,d), Level (n',d') ->
+      | Level (d,n), Level (d',n') ->
         Int.equal n n' && DirPath.equal d d'
       | Var n, Var n' -> Int.equal n n'
       | _ -> false
@@ -62,7 +87,7 @@ struct
     | Set, Set -> 0
     | Set, _ -> -1
     | _, Set -> 1
-    | Level (i1, dp1), Level (i2, dp2) ->
+    | Level (dp1, i1), Level (dp2, i2) ->
       if i1 < i2 then -1
       else if i1 > i2 then 1
       else DirPath.compare dp1 dp2
@@ -83,9 +108,9 @@ struct
   let hcons = function
     | Prop as x -> x
     | Set as x -> x
-    | Level (n,d) as x -> 
+    | Level (d,n) as x ->
       let d' = Names.DirPath.hcons d in
-        if d' == d then x else Level (n,d')
+        if d' == d then x else Level (d',n)
     | Var _n as x -> x
 
   open Hashset.Combine
@@ -94,18 +119,20 @@ struct
     | Prop -> combinesmall 1 0
     | Set -> combinesmall 1 1
     | Var n -> combinesmall 2 n
-    | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d))
+    | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d))
 
 end
 
 module Level = struct
 
-  open Names
+  module Id = RawLevel.Id
+
+  module Qualid = RawLevel.Qualid
 
   type raw_level = RawLevel.t =
   | Prop
   | Set
-  | Level of int * DirPath.t
+  | Level of Qualid.t
   | Var of int
 
   (** Embed levels with their hash value *)
@@ -166,7 +193,7 @@ module Level = struct
     match data x with
     | Prop -> "Prop"
     | Set -> "Set"
-    | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n
+    | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n
     | Var n -> "Var(" ^ string_of_int n ^ ")"
 
   let pr u = str (to_string u)
@@ -185,11 +212,12 @@ module Level = struct
     match data u with
     | Var n -> Some n | _ -> None
 
-  let make m n = make (Level (n, Names.DirPath.hcons m))
+  let make2 m n = make (Level (Names.DirPath.hcons m, n))
+  let make qid = make (Level qid)
 
   let name u =
     match data u with
-    | Level (n, d) -> Some (d, n)
+    | Level (d, n) -> Some (d, n)
     | _ -> None
 end
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index de7b334ae4..69aecac4f3 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -11,9 +11,32 @@
 (** Universes. *)
 module Level :
 sig
+
+  module Id : sig
+    type t
+
+    val make : int -> t
+    val to_string : t -> string
+
+  end
+  (** Non-qualified global universe level *)
+
+  module Qualid : sig
+    type t
+
+    val make : Names.DirPath.t -> Id.t -> t
+    val repr : t -> Names.DirPath.t * Id.t
+    val equal : t -> t -> bool
+    val hash : t -> int
+    val compare : t -> t -> int
+
+  end
+  (** Qualified global universe level *)
+
   type t
   (** Type of universe levels. A universe level is essentially a unique name
-      that will be associated to constraints later on. *)
+      that will be associated to constraints later on. A level can be local to a
+      definition or global. *)
 
   val set : t
   val prop : t
@@ -34,7 +57,9 @@ sig
 
   val hash : t -> int
 
-  val make : Names.DirPath.t -> int -> t
+  val make : Qualid.t -> t
+
+  val make2 : Names.DirPath.t -> Id.t -> t
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
@@ -48,7 +73,7 @@ sig
 
   val var_index : t -> int option
 
-  val name : t -> (Names.DirPath.t * int) option
+  val name : t -> Qualid.t option
 end
 
 (** Sets of universe levels *)
diff --git a/library/nametab.ml b/library/nametab.ml
index e29c7b2960..ab69da3467 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -347,12 +347,10 @@ module DirTab = Make(DirPath')(GlobDirRef)
 type dirtab = DirTab.t
 let the_dirtab = Summary.ref ~name:"dirtab" (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'
+  type t = Univ.Level.Qualid.t
+  let equal = Univ.Level.Qualid.equal
 end
 module UnivTab = Make(FullPath)(UnivIdEqual)
 type univtab = UnivTab.t
@@ -375,12 +373,9 @@ let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevt
 
 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
+  type t = Univ.Level.Qualid.t
+  let hash = Univ.Level.Qualid.hash
+  let compare = Univ.Level.Qualid.compare
 end
 
 module UnivIdMap = HMap.Make(UnivIdOrdered)
diff --git a/library/nametab.mli b/library/nametab.mli
index 24af07619d..496c76d9b0 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -120,11 +120,9 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
 
-type universe_id = DirPath.t * int
+module UnivIdMap : CMap.ExtS with type key = Univ.Level.Qualid.t
 
-module UnivIdMap : CMap.ExtS with type key = universe_id
-
-val push_universe : visibility -> full_path -> universe_id -> unit
+val push_universe : visibility -> full_path -> Univ.Level.Qualid.t -> unit
 
 (** {6 The following functions perform globalization of qualified names } *)
 
@@ -139,7 +137,7 @@ val locate_modtype : qualid -> ModPath.t
 val locate_dir : qualid -> GlobDirRef.t
 val locate_module : qualid -> ModPath.t
 val locate_section : qualid -> DirPath.t
-val locate_universe : qualid -> universe_id
+val locate_universe : qualid -> Univ.Level.Qualid.t
 
 (** These functions globalize user-level references into global
    references, like [locate] and co, but raise a nice error message
@@ -196,7 +194,7 @@ 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
+val path_of_universe : Univ.Level.Qualid.t -> full_path
 
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
@@ -218,7 +216,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.Qualid.t -> qualid
 
 (** Deprecated synonyms *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f5e48bcd39..d01c44811f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -120,8 +120,8 @@ let interp_known_universe_level evd qid =
     if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
     else raise Not_found
   with Not_found ->
-    let univ, k = Nametab.locate_universe qid in
-    Univ.Level.make univ k
+    let qid = Nametab.locate_universe qid in
+    Univ.Level.make qid
 
 let interp_universe_level_name ~anon_rigidity evd qid =
   try evd, interp_known_universe_level evd qid
@@ -140,7 +140,7 @@ let interp_universe_level_name ~anon_rigidity evd qid =
           user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
             (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
       in
-      let level = Univ.Level.make dp num in
+      let level = Univ.Level.make2 dp (Univ.Level.Id.make num) in
       let evd =
         try Evd.add_global_univ evd level
         with UGraph.AlreadyDeclared -> evd
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 94e04d1842..b834fb71e4 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,7 +60,7 @@ module Make(T : Task) () = struct
   type request = Request of T.request
 
   type more_data =
-    | MoreDataUnivLevel of UnivGen.universe_id list
+    | MoreDataUnivLevel of Univ.Level.Id.t list
 
   let slave_respond (Request r) =
     let res = T.perform r in
-- 
cgit v1.2.3


From cff3c5a7148afc722852bd01658fe49ffec1d967 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Dec 2018 15:52:37 +0100
Subject: Revise API for global universes.

Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.

Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).

Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)

This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~

Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.

UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.

NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
---
 checker/values.ml      |  4 ++--
 engine/termops.mli     |  2 +-
 engine/uState.ml       |  6 ++++--
 engine/uState.mli      |  2 +-
 engine/univGen.ml      |  9 ++++++---
 engine/univGen.mli     |  6 ++++--
 engine/univNames.ml    | 17 +++++++----------
 engine/univNames.mli   |  2 +-
 interp/declare.ml      |  8 ++------
 kernel/indtypes.ml     |  4 +++-
 kernel/inductive.ml    |  6 +++---
 kernel/uGraph.ml       |  2 +-
 kernel/univ.ml         | 27 +++++++--------------------
 kernel/univ.mli        | 22 ++++------------------
 library/nametab.ml     | 10 +++++-----
 library/nametab.mli    | 10 +++++-----
 pretyping/detyping.ml  | 19 +++++++++++++++++--
 pretyping/pretyping.ml |  2 +-
 stm/asyncTaskQueue.ml  |  2 +-
 19 files changed, 75 insertions(+), 85 deletions(-)

diff --git a/checker/values.ml b/checker/values.ml
index f73e19a972..863f965896 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -93,9 +93,9 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|]
 
 
 (** kernel/univ *)
-let v_level_qualid = v_tuple "Level.Qualid.t" [|v_dp;Int|]
+let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|]
 let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) 
-  [|(*Level*)[|v_level_qualid|]; (*Var*)[|Int|]|]
+  [|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|]
 let v_level = v_tuple "level" [|Int;v_raw_level|] 
 let v_expr = v_tuple "levelexpr" [|v_level;Int|]
 let v_univ = List v_expr
diff --git a/engine/termops.mli b/engine/termops.mli
index eef8452e64..7920af8e0e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -290,7 +290,7 @@ 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.qualid
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
 
 (** Combinators on judgments *)
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 56b7a16ace..185283225c 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -324,12 +324,14 @@ let constrain_variables diff ctx =
 let qualid_of_level uctx =
   let map, map_rev = uctx.uctx_names in 
     fun l ->
-      try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)
+      try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname))
       with Not_found | Option.IsNone ->
         UnivNames.qualid_of_level l
 
 let pr_uctx_level uctx l =
-  Libnames.pr_qualid (qualid_of_level uctx l)
+  match qualid_of_level uctx l with
+  | Some qid -> Libnames.pr_qualid qid
+  | None -> Univ.Level.pr l
 
 type ('a, 'b) gen_universe_decl = {
   univdecl_instance : 'a; (* Declared universes *)
diff --git a/engine/uState.mli b/engine/uState.mli
index ad0cd5c1bb..5170184ef4 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -188,6 +188,6 @@ val update_sigma_env : t -> Environ.env -> t
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
 
 val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 5aa4734b23..40c4c909fe 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -13,14 +13,17 @@ open Names
 open Constr
 open Univ
 
+type univ_unique_id = int
 (* Generator of levels *)
 let new_univ_id, set_remote_new_univ_id =
   RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
-    ~build:(fun n -> Level.Id.make n)
+    ~build:(fun n -> n)
+
+let new_univ_global () =
+  Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
 
 let fresh_level () =
-  let id = new_univ_id () in
-  Univ.Level.make2 (Global.current_dirpath ()) id
+  Univ.Level.make (new_univ_global ())
 
 (* TODO: remove *)
 let new_univ () = Univ.Universe.make (fresh_level ())
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 66e80368a4..b4598e10d0 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -15,11 +15,13 @@ open Univ
 
 
 (** The global universe counter *)
-val set_remote_new_univ_id : Level.Id.t RemoteCounter.installer
+type univ_unique_id
+val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer
+val new_univ_id : unit -> univ_unique_id (** for the stm *)
 
 (** Side-effecting functions creating new universe levels. *)
 
-val new_univ_id : unit -> Level.Id.t
+val new_univ_global : unit -> Level.UGlobal.t
 val fresh_level : unit -> Level.t
 
 val new_univ : unit -> Universe.t
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6bf1187b65..19705f9d36 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -16,17 +16,14 @@ open Univ
 let qualid_of_level l =
   match Level.name l with
   | Some qid  ->
-    begin
-    try Nametab.shortest_qualid_of_universe qid
-    with Not_found ->
-      let (dp,n) = Level.Qualid.repr qid in
-      let name = Id.of_string_soft (Level.Id.to_string n) in
-      Libnames.make_qualid dp name
-    end
-  | None ->
-    Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
+    (try Some (Nametab.shortest_qualid_of_universe qid)
+     with Not_found -> None)
+  | None -> None
 
-let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
+let pr_with_global_universes l =
+  match qualid_of_level l with
+  | Some qid  -> Libnames.pr_qualid qid
+  | None -> Level.pr l
 
 (** Global universe information outside the kernel, to handle
     polymorphic universe names in sections that have to be discharged. *)
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 6e68153ac2..e9c517babf 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -11,7 +11,7 @@
 open Univ
 
 val pr_with_global_universes : Level.t -> Pp.t
-val qualid_of_level : Level.t -> Libnames.qualid
+val qualid_of_level : Level.t -> Libnames.qualid option
 
 (** Local universe name <-> level mapping *)
 
diff --git a/interp/declare.ml b/interp/declare.ml
index 0c9d26dd01..a809a856b9 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -469,7 +469,7 @@ type universe_source =
   | QualifiedUniv of Id.t (* global universe introduced by some global value *)
   | UnqualifiedUniv (* other global universe *)
 
-type universe_name_decl = universe_source * (Id.t * Univ.Level.Qualid.t) list
+type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list
 
 let check_exists sp =
   if Nametab.exists_universe sp then
@@ -540,11 +540,7 @@ let do_universe poly l =
       user_err ~hdr:"Constraint"
                    (str"Cannot declare polymorphic universes outside sections")
   in
-  let l =
-    List.map (fun {CAst.v=id} ->
-      let lev = UnivGen.new_univ_id () in
-      (id, Univ.Level.Qualid.make (Global.current_dirpath ()) lev)) l
-  in
+  let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in
   let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
       Univ.LSet.empty l, Univ.Constraint.empty
   in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8efda16d64..68d44f8782 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -218,7 +218,9 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
 let check_subtyping cumi paramsctxt env_ar inds = 
     let numparams = Context.Rel.nhyps paramsctxt in
     let uctx = CumulativityInfo.univ_context cumi in
-    let new_levels = Array.init (UContext.size uctx) (fun i -> Level.make2 DirPath.empty (Level.Id.make i)) in
+    let new_levels = Array.init (UContext.size uctx)
+        (fun i -> Level.make (Level.UGlobal.make DirPath.empty i))
+    in
     let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
         LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
     in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 30d96a22e0..05c5c0e821 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -593,10 +593,10 @@ let rec ienv_decompose_prod (env,_ as ienv) n c =
      ienv_decompose_prod ienv' (n-1) b
      | _ -> assert false
 
+let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0))
+let dummy_implicit_sort = mkType (Universe.make dummy_univ)
 let lambda_implicit_lift n a =
-  let level = Level.make2 (DirPath.make [Id.of_string "implicit"]) (Level.Id.make 0) in
-  let implicit_sort = mkType (Universe.make level) in
-  let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
+  let lambda_implicit a = mkLambda (Anonymous, dummy_implicit_sort, a) in
   iterate lambda_implicit n (lift n a)
 
 (* This removes global parameters of the inductive types in lc (for
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 064fffe98e..5fc8d0297f 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -921,7 +921,7 @@ let sort_universes g =
   let types = Array.init (max_lvl + 1) (function
     | 0 -> Level.prop
     | 1 -> Level.set
-    | n -> Level.make2 mp (Level.Id.make (n-2)))
+    | n -> Level.make (Level.UGlobal.make  mp (n-2)))
   in
   let g = Array.fold_left (fun g u ->
     let g, u = safe_repr g u in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 57a5dce8a4..7b5ed05bda 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -37,19 +37,10 @@ module RawLevel =
 struct
   open Names
 
-  module Id = struct
-    type t = int
+  module UGlobal = struct
+    type t = DirPath.t * int
 
-    let make i = i
-    let to_string i = string_of_int i
-
-  end
-
-  module Qualid = struct
-    type t = DirPath.t * Id.t
-
-    let make dp i = (dp,i)
-    let repr x = x
+    let make dp i = (DirPath.hcons dp,i)
 
     let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
 
@@ -64,7 +55,7 @@ struct
   type t =
     | Prop
     | Set
-    | Level of Qualid.t
+    | Level of UGlobal.t
     | Var of int
 
   (* Hash-consing *)
@@ -74,8 +65,7 @@ struct
       match x, y with
       | Prop, Prop -> true
       | Set, Set -> true
-      | Level (d,n), Level (d',n') ->
-        Int.equal n n' && DirPath.equal d d'
+      | Level l, Level l' -> UGlobal.equal l l'
       | Var n, Var n' -> Int.equal n n'
       | _ -> false
 
@@ -125,14 +115,12 @@ end
 
 module Level = struct
 
-  module Id = RawLevel.Id
-
-  module Qualid = RawLevel.Qualid
+  module UGlobal = RawLevel.UGlobal
 
   type raw_level = RawLevel.t =
   | Prop
   | Set
-  | Level of Qualid.t
+  | Level of UGlobal.t
   | Var of int
 
   (** Embed levels with their hash value *)
@@ -212,7 +200,6 @@ module Level = struct
     match data u with
     | Var n -> Some n | _ -> None
 
-  let make2 m n = make (Level (Names.DirPath.hcons m, n))
   let make qid = make (Level qid)
 
   let name u =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 69aecac4f3..512f38cedd 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -12,20 +12,10 @@
 module Level :
 sig
 
-  module Id : sig
+  module UGlobal : sig
     type t
 
-    val make : int -> t
-    val to_string : t -> string
-
-  end
-  (** Non-qualified global universe level *)
-
-  module Qualid : sig
-    type t
-
-    val make : Names.DirPath.t -> Id.t -> t
-    val repr : t -> Names.DirPath.t * Id.t
+    val make : Names.DirPath.t -> int -> t
     val equal : t -> t -> bool
     val hash : t -> int
     val compare : t -> t -> int
@@ -57,11 +47,7 @@ sig
 
   val hash : t -> int
 
-  val make : Qualid.t -> t
-
-  val make2 : Names.DirPath.t -> Id.t -> t
-  (** Create a new universe level from a unique identifier and an associated
-      module path. *)
+  val make : UGlobal.t -> t
 
   val pr : t -> Pp.t
   (** Pretty-printing *)
@@ -73,7 +59,7 @@ sig
 
   val var_index : t -> int option
 
-  val name : t -> Qualid.t option
+  val name : t -> UGlobal.t option
 end
 
 (** Sets of universe levels *)
diff --git a/library/nametab.ml b/library/nametab.ml
index ab69da3467..f0f643d9b5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -349,8 +349,8 @@ let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)
 
 module UnivIdEqual =
 struct
-  type t = Univ.Level.Qualid.t
-  let equal = Univ.Level.Qualid.equal
+  type t = Univ.Level.UGlobal.t
+  let equal = Univ.Level.UGlobal.equal
 end
 module UnivTab = Make(FullPath)(UnivIdEqual)
 type univtab = UnivTab.t
@@ -373,9 +373,9 @@ let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevt
 
 module UnivIdOrdered =
 struct
-  type t = Univ.Level.Qualid.t
-  let hash = Univ.Level.Qualid.hash
-  let compare = Univ.Level.Qualid.compare
+  type t = Univ.Level.UGlobal.t
+  let hash = Univ.Level.UGlobal.hash
+  let compare = Univ.Level.UGlobal.compare
 end
 
 module UnivIdMap = HMap.Make(UnivIdOrdered)
diff --git a/library/nametab.mli b/library/nametab.mli
index 496c76d9b0..b7926cf515 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -120,9 +120,9 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
 
-module UnivIdMap : CMap.ExtS with type key = Univ.Level.Qualid.t
+module UnivIdMap : CMap.ExtS with type key = Univ.Level.UGlobal.t
 
-val push_universe : visibility -> full_path -> Univ.Level.Qualid.t -> unit
+val push_universe : visibility -> full_path -> Univ.Level.UGlobal.t -> unit
 
 (** {6 The following functions perform globalization of qualified names } *)
 
@@ -137,7 +137,7 @@ val locate_modtype : qualid -> ModPath.t
 val locate_dir : qualid -> GlobDirRef.t
 val locate_module : qualid -> ModPath.t
 val locate_section : qualid -> DirPath.t
-val locate_universe : qualid -> Univ.Level.Qualid.t
+val locate_universe : qualid -> Univ.Level.UGlobal.t
 
 (** These functions globalize user-level references into global
    references, like [locate] and co, but raise a nice error message
@@ -194,7 +194,7 @@ 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 : Univ.Level.Qualid.t -> full_path
+val path_of_universe : Univ.Level.UGlobal.t -> full_path
 
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
@@ -216,7 +216,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.Qualid.t -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
 
 (** Deprecated synonyms *)
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 33ced6d6e0..ce7c7c8702 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -589,8 +589,23 @@ let detype_cofix detype avoid env sigma n (names,tys,bodies) =
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
+(* TODO use some algebraic type with a case for unnamed univs so we
+   can cleanly detype them. NB: this corresponds to a hack in
+   Pretyping.interp_universe_level_name to convert Foo.xx strings into
+   universes. *)
+let hack_qualid_of_univ_level sigma l =
+  match Termops.reference_of_level sigma l with
+  | Some qid -> qid
+  | None ->
+    let path = String.split_on_char '.' (Univ.Level.to_string l) in
+    let path = List.rev_map Id.of_string_soft path in
+    Libnames.qualid_of_dirpath (DirPath.make path)
+
 let detype_universe sigma u =
-  let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in
+  let fn (l, n) =
+    let qid = hack_qualid_of_univ_level sigma l in
+    Some (qid, n)
+  in
   Univ.Universe.map fn u
 
 let detype_sort sigma = function
@@ -611,7 +626,7 @@ 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 = Termops.reference_of_level sigma l in
+  let l = hack_qualid_of_univ_level sigma l in
   GType (UNamed l)
 
 let detype_instance sigma l = 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d01c44811f..2be0f73ea4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -140,7 +140,7 @@ let interp_universe_level_name ~anon_rigidity evd qid =
           user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
             (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
       in
-      let level = Univ.Level.make2 dp (Univ.Level.Id.make num) in
+      let level = Univ.Level.(make (UGlobal.make dp num)) in
       let evd =
         try Evd.add_global_univ evd level
         with UGraph.AlreadyDeclared -> evd
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index b834fb71e4..51166cf238 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,7 +60,7 @@ module Make(T : Task) () = struct
   type request = Request of T.request
 
   type more_data =
-    | MoreDataUnivLevel of Univ.Level.Id.t list
+    | MoreDataUnivLevel of UnivGen.univ_unique_id list
 
   let slave_respond (Request r) =
     let res = T.perform r in
-- 
cgit v1.2.3