diff options
| author | Gaëtan Gilbert | 2021-04-01 19:35:27 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-04-14 12:54:05 +0200 |
| commit | 004bf5770bdcdd1b35dd27f683c733505823e741 (patch) | |
| tree | ddab8d75e94782d2f21e7d2cc4fae83f6326f7dc /engine | |
| parent | ea62d1e19f2ba565ea3a18ba3709a06af5c845ac (diff) | |
Put async worker id in universe names
This removes the need for the remote counter.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/univGen.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 ()) |