aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/coqworkmgrApi.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/coqworkmgrApi.mli')
-rw-r--r--stm/coqworkmgrApi.mli8
1 files changed, 6 insertions, 2 deletions
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index 70d4173ae..953903810 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -8,9 +8,13 @@
(* High level api for clients of the service (like coqtop) *)
+type priority = Low | High
+val string_of_priority : priority -> string
+val priority_of_string : string -> priority
+
(* Connects to a work manager if any. If no worker manager, then
-async-proofs-j and -async-proofs-tac-j are used *)
-val init : Flags.priority -> unit
+val init : priority -> unit
(* blocking *)
val get : int -> int
@@ -21,7 +25,7 @@ val giveback : int -> unit
(* Low level *)
type request =
- | Hello of Flags.priority
+ | Hello of priority
| Get of int
| TryGet of int
| GiveBack of int