From e2e88741120332f9e97459852d7361e2d8939881 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Mar 2015 10:21:41 +0100 Subject: Splitting the library representation on disk in two. The first part only contains the summary of the library, while the second one contains the effective content of it. --- library/library.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'library/library.mli') diff --git a/library/library.mli b/library/library.mli index 350670680..967a54e4c 100644 --- a/library/library.mli +++ b/library/library.mli @@ -28,6 +28,7 @@ val require_library_from_file : (** {6 ... } *) (** Segments of a library *) +type seg_sum type seg_lib type seg_univ = (* cst, all_cst, finished? *) Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool @@ -47,8 +48,8 @@ val save_library_to : DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : - string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs -val save_library_raw : string -> seg_lib -> seg_univ -> seg_proofs -> unit + string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs +val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit (** {6 Interrogate the status of libraries } *) -- cgit v1.2.3