diff options
| author | coqbot-app[bot] | 2021-04-14 16:19:19 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-14 16:19:19 +0000 |
| commit | 00391bd681098132cc89c356d1d27334d257fc8b (patch) | |
| tree | 9bb7bc653fd98b120ab5f80e2475141f85ad841f /engine | |
| parent | 90a6c01dec9d58fa409e7097ac5ba03f08a9ae7b (diff) | |
| parent | 8df5a37d934b4f862a6183ee451c6bb34ae72d94 (diff) | |
Merge PR #14050: Remove remote counter system
Reviewed-by: gares
Ack-by: ppedrot
Ack-by: ejgallego
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/univGen.ml | 10 | ||||
| -rw-r--r-- | engine/univGen.mli | 6 |
2 files changed, 5 insertions, 11 deletions
diff --git a/engine/univGen.ml b/engine/univGen.ml index 278ca6bf34..b917d91512 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -13,14 +13,14 @@ 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 () = - 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 ()) 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 |