diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-17 10:21:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-24 00:13:17 +0200 |
| commit | e2e88741120332f9e97459852d7361e2d8939881 (patch) | |
| tree | 9674a8785e31974fb73b96b840014d86d5e14b1b /library/library.mli | |
| parent | a2fa3dd1ec96cd70c817ff375d7b857924bb9825 (diff) | |
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.
Diffstat (limited to 'library/library.mli')
| -rw-r--r-- | library/library.mli | 5 |
1 files changed, 3 insertions, 2 deletions
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 } *) |