diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 6 | ||||
| -rw-r--r-- | library/states.ml | 6 |
2 files changed, 5 insertions, 7 deletions
diff --git a/library/library.ml b/library/library.ml index f5c7f6335..0fb938e9b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -742,7 +742,8 @@ let save_library_to ?todo dir f otab = if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then error_recursively_dependent_library dir; (* Open the vo file and write the magic number *) - let (f',ch) = raw_extern_library f in + let f' = f in + let ch = raw_extern_library f' in try (* Writing vo payload *) System.marshal_out_segment f' ch (sd : seg_sum); @@ -765,7 +766,8 @@ let save_library_to ?todo dir f otab = iraise reraise let save_library_raw f sum lib univs proofs = - let (f',ch) = raw_extern_library (f^"o") in + 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); diff --git a/library/states.ml b/library/states.ml index 96a487b16..4e55f0cdc 100644 --- a/library/states.ml +++ b/library/states.ml @@ -22,16 +22,12 @@ let unfreeze (fl,fs) = Summary.unfreeze_summaries fs let (extern_state,intern_state) = - let ensure_suffix f = CUnix.make_suffix f ".coq" in let (raw_extern, raw_intern) = extern_intern Coq_config.state_magic_number in (fun s -> - let s = ensure_suffix s in raw_extern s (freeze ~marshallable:`Yes)), (fun s -> - let s = ensure_suffix s in - let paths = Loadpath.get_paths () in - unfreeze (with_magic_number_check (raw_intern paths) s); + unfreeze (with_magic_number_check raw_intern s); Library.overwrite_library_filenames s) (* Rollback. *) |