aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/library.mli')
-rw-r--r--library/library.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.mli b/library/library.mli
index 77d78207d..75b256258 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -44,7 +44,7 @@ val start_library : string -> DirPath.t * string
(** {6 End the compilation of a library and save it to a ".vo" file } *)
val save_library_to :
- ?todo:((Future.UUID.t,'document) Stateid.request list * 'counters) ->
+ ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
DirPath.t -> string -> Opaqueproof.opaquetab -> unit
val load_library_todo :