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.

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)