diff options
| author | Gaëtan Gilbert | 2021-03-26 15:34:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-04-14 12:54:38 +0200 |
| commit | 3efee577b4c92b38a987b40e555fae2c0a2023c4 (patch) | |
| tree | 182f9cd42fdb9969bab3149f3add552c7455de2e /engine/univGen.ml | |
| parent | 004bf5770bdcdd1b35dd27f683c733505823e741 (diff) | |
Remove remote counter system
Diffstat (limited to 'engine/univGen.ml')
| -rw-r--r-- | engine/univGen.ml | 7 |
1 files changed, 3 insertions, 4 deletions
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 |