diff options
| author | Vincent Laporte | 2019-05-21 12:39:17 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-05-21 12:39:17 +0000 |
| commit | 0aa9a5407874332dfa31f1a0f73d2dc91e95fb39 (patch) | |
| tree | 2b1a3cb6418624b9f096479ee58cceb28607f921 /library | |
| parent | 02d6f5660d54fcf4dfc9cff36cbda41dca3f601f (diff) | |
| parent | eed3831a2cc32042fdee95767da00d7e52840371 (diff) | |
Merge PR #10160: Miscellaneous fixes related to the command line
Ack-by: gares
Ack-by: herbelin
Reviewed-by: vbgl
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 19 | ||||
| -rw-r--r-- | library/library.mli | 2 |
2 files changed, 9 insertions, 12 deletions
diff --git a/library/library.ml b/library/library.ml index 04e38296d9..500e77f89b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -612,8 +612,6 @@ let import_module export modl = (*s Initializing the compilation of a library. *) let load_library_todo f = - let longf = Loadpath.locate_file (f^".v") in - let f = longf^"io" in let ch = raw_intern_library f in let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in @@ -626,7 +624,7 @@ let load_library_todo f = if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); if s3 = None then user_err ~hdr:"restart" (str"not a .vio file"); if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); - longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 + s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) @@ -727,14 +725,13 @@ let save_library_to ?todo ~output_native_objects dir f otab = iraise reraise let save_library_raw f sum lib univs proofs = - let f' = f^"o" in - let ch = raw_extern_library f' in - System.marshal_out_segment f' ch (sum : seg_sum); - System.marshal_out_segment f' ch (lib : seg_lib); - System.marshal_out_segment f' ch (Some univs : seg_univ option); - System.marshal_out_segment f' ch (None : seg_discharge option); - System.marshal_out_segment f' ch (None : 'tasks option); - System.marshal_out_segment f' ch (proofs : seg_proofs); + let ch = raw_extern_library f in + System.marshal_out_segment f ch (sum : seg_sum); + System.marshal_out_segment f ch (lib : seg_lib); + System.marshal_out_segment f ch (Some univs : seg_univ option); + System.marshal_out_segment f ch (None : seg_discharge option); + System.marshal_out_segment f ch (None : 'tasks option); + System.marshal_out_segment f ch (proofs : seg_proofs); close_out ch module StringOrd = struct type t = string let compare = String.compare end diff --git a/library/library.mli b/library/library.mli index a976be0184..390299bf56 100644 --- a/library/library.mli +++ b/library/library.mli @@ -46,7 +46,7 @@ val save_library_to : DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : - string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs + 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 } *) |