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 | |
| parent | 004bf5770bdcdd1b35dd27f683c733505823e741 (diff) | |
Remove remote counter system
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/univGen.ml | 7 | ||||
| -rw-r--r-- | engine/univGen.mli | 6 |
2 files changed, 3 insertions, 10 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 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 |