Passing command-line option async_proofs_worker_priority functionally.

We lose track of it at some time in "known_state" and assume that the
reference cur_opt has not been modified in between the time it was set
(in "new_doc") and "known_state".

1 files changed, 6 insertions, 6 deletions

diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index ea438f3f76..e6cf6343c8 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -144,10 +144,10 @@ module MakeQueue(T : Task) () : sig
   (** [queue] is the abstract queue type. *)
   type queue
 
-  (** [create n] will initialize the queue with [n] workers. If [n] is
-      0, the queue won't spawn any process, working in a lazy local
-      manner. [not imposed by the this API] *)
-  val create : int -> queue
+  (** [create n pri] will initialize the queue with [n] workers having
+      priority [pri]. If [n] is 0, the queue won't spawn any process,
+      working in a lazy local manner. [not imposed by the this API] *)
+  val create : int -> CoqworkmgrApi.priority -> queue
 
   (** [destroy q] Deallocates [q], cancelling all pending tasks. *)
   val destroy : queue -> unit
@@ -203,9 +203,9 @@ module MakeQueue(T : Task) () : sig
   (** [clear q] Clears [q], only if the worker prool is empty *)
   val clear : queue -> unit
 
-  (** [with_n_workers n f] create a queue, run the function, destroy
+  (** [with_n_workers n pri f] creates a queue, runs the function, destroys
       the queue. The user should call join *)
-  val with_n_workers : int -> (queue -> 'a) -> 'a
+  val with_n_workers : int -> CoqworkmgrApi.priority -> (queue -> 'a) -> 'a
 
 end