From 004bf5770bdcdd1b35dd27f683c733505823e741 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 1 Apr 2021 19:35:27 +0200
Subject: Put async worker id in universe names

This removes the need for the remote counter.
---
 engine/univGen.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/univGen.ml b/engine/univGen.ml
index 278ca6bf34..b98c15f245 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -20,7 +20,8 @@ let new_univ_id, set_remote_new_univ_id =
     ~build:(fun n -> n)
 
 let new_univ_global () =
-  Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
+  let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in
+  Univ.Level.UGlobal.make (Global.current_dirpath ()) s (new_univ_id ())
 
 let fresh_level () =
   Univ.Level.make (new_univ_global ())
-- 
cgit v1.2.3