Merge PR #9155: Fix race condition triggered by fresh universe generation

1 files changed, 10 insertions, 11 deletions

diff --git a/engine/univGen.ml b/engine/univGen.ml
index 130aa06f53..40c4c909fe 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -13,26 +13,25 @@ open Names
 open Constr
 open Univ
 
+type univ_unique_id = int
 (* 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)
+    ~build:(fun n -> n)
 
-let new_univ_level () =
-  let dp, id = new_univ_id () in
-  Univ.Level.make dp id
+let new_univ_global () =
+  Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
 
-let fresh_level () = new_univ_level ()
+let fresh_level () =
+  Univ.Level.make (new_univ_global ())
 
 (* 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)