4 files changed, 17 insertions, 22 deletions
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)