aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/remoteCounter.ml
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-27 11:03:43 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-03 12:08:03 +0200
commitf14b6f1a17652566f0cbc00ce81421ba0684dad5 (patch)
tree8a331593d0d1b518e8764c92ac54e3b11c222358 /lib/remoteCounter.ml
parent500d38d0887febb614ddcadebaef81e0c7942584 (diff)
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
Diffstat (limited to 'lib/remoteCounter.ml')
-rw-r--r--lib/remoteCounter.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 6cc48c874..e7646fb79 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -25,7 +25,7 @@ let new_counter ~name a ~incr ~build =
(* - in the main process there is a race condition between slave
managers (that are threads) and the main thread, hence the mutex *)
if Flags.async_proofs_is_worker () then
- Errors.anomaly(Pp.str"Slave processes must install remote counters");
+ CErrors.anomaly(Pp.str"Slave processes must install remote counters");
Mutex.lock m; let x = f () in Mutex.unlock m;
build x in
let mk_thsafe_remote_getter f () =
@@ -33,7 +33,7 @@ let new_counter ~name a ~incr ~build =
let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in
let installer f =
if not (Flags.async_proofs_is_worker ()) then
- Errors.anomaly(Pp.str"Only slave processes can install a remote counter");
+ CErrors.anomaly(Pp.str"Only slave processes can install a remote counter");
getter := mk_thsafe_remote_getter f in
(fun () -> !getter ()), installer