diff options
Diffstat (limited to 'toplevel/stm.mli')
| -rw-r--r-- | toplevel/stm.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/stm.mli b/toplevel/stm.mli index 0a7473792..c47bacf65 100644 --- a/toplevel/stm.mli +++ b/toplevel/stm.mli @@ -44,10 +44,13 @@ val stop_worker : int -> unit val join : unit -> unit (* To save to disk an incomplete document *) type tasks -val dump : unit -> tasks +val dump : (Future.UUID.t * int) list -> tasks val check_task : string -> tasks -> int -> bool val info_tasks : tasks -> (string * float * int) list +val finish_tasks : string -> + Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> + tasks -> unit (* Id of the tip of the current branch *) val get_current_state : unit -> Stateid.t |