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


From 3efee577b4c92b38a987b40e555fae2c0a2023c4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 26 Mar 2021 15:34:59 +0100
Subject: Remove remote counter system

---
 engine/univGen.ml  | 7 +++----
 engine/univGen.mli | 6 ------
 2 files changed, 3 insertions(+), 10 deletions(-)

(limited to 'engine')

diff --git a/engine/univGen.ml b/engine/univGen.ml
index b98c15f245..b917d91512 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -13,11 +13,10 @@ 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 -> n)
+let new_univ_id =
+  let cnt = ref 0 in
+  fun () -> incr cnt; !cnt
 
 let new_univ_global () =
   let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 05737411f5..743d819747 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -13,12 +13,6 @@ open Constr
 open Environ
 open Univ
 
-
-(** The global universe counter *)
-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_global : unit -> Level.UGlobal.t
-- 
cgit v1.2.3