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