STM: code restructured to reuse task queue for tactics

1 files changed, 4 insertions, 8 deletions

diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index bec46901f..72887b21a 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -24,18 +24,14 @@ let new_counter ~name a ~incr ~build =
     (* - slaves must use a remote counter getter, not this one! *)
     (* - in the main process there is a race condition between slave
          managers (that are threads) and the main thread, hence the mutex *)
-    (match !Flags.async_proofs_mode with
-    | Flags.APonParallel n when n > 0 ->
-        Errors.anomaly(Pp.str"Slave processes must install remote counters");
-    | _ -> ());
+    if Flags.async_proofs_is_worker () then
+      Errors.anomaly(Pp.str"Slave processes must install remote counters");
     Mutex.lock m; let x = f () in Mutex.unlock m;
     build x in
   let getter = ref(mk_thsafe_getter (fun () -> !data := incr !!data; !!data)) in
   let installer f =
-    (match !Flags.async_proofs_mode with
-    | Flags.APoff | Flags.APonLazy | Flags.APonParallel 0 -> 
-      Errors.anomaly(Pp.str"Only slave processes can install a remote counter")
-    | _ -> ());
+    if not (Flags.async_proofs_is_worker ()) then
+      Errors.anomaly(Pp.str"Only slave processes can install a remote counter");
     getter := f in
   (fun () -> !getter ()), installer