Prevent States.intern_state and System.extern_intern from looking up files in the loadpath.

This patch causes a bit of code duplication (because of the .coq suffix
added to state files) but it makes it clear which part of the code is
looking up files in the loadpath and for what purpose. Also it makes the
interface of System.extern_intern and System.raw_extern_intern much saner.

1 files changed, 4 insertions, 2 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);