Removing mandatory suffixes for library files.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 16 insertions, 14 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 88306e214..03a18280a 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -264,7 +264,7 @@ let try_locate_qualified_library qid =
 (*s Loading from disk to cache (preparation phase) *)
 
 let raw_intern_library =
-  snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo")
+  snd (System.raw_extern_intern Coq_config.vo_magic_number)
 
 let with_magic_number_check f a =
   try f a
diff --git a/lib/system.ml b/lib/system.ml
index a72958b99..d2788de93 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -123,12 +123,11 @@ let marshal_in filename ch =
 
 exception Bad_magic_number of string
 
-let raw_extern_intern magic suffix =
-  let extern_state name =
-    let filename = CUnix.make_suffix name suffix in
+let raw_extern_intern magic =
+  let extern_state filename =
     let channel = open_trapping_failure filename in
     output_binary_int channel magic;
-    filename,channel
+    filename, channel
   and intern_state filename =
     let channel = open_in_bin filename in
     if not (Int.equal (input_binary_int channel) magic) then
@@ -137,8 +136,8 @@ let raw_extern_intern magic suffix =
   in
   (extern_state,intern_state)
 
-let extern_intern ?(warn=true) magic suffix =
-  let (raw_extern,raw_intern) = raw_extern_intern magic suffix in
+let extern_intern ?(warn=true) magic =
+  let (raw_extern,raw_intern) = raw_extern_intern magic in
   let extern_state name val_0 =
     try
       let (filename,channel) = raw_extern name in
@@ -152,7 +151,7 @@ let extern_intern ?(warn=true) magic suffix =
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name =
     try
-      let _,filename = find_file_in_path ~warn paths (CUnix.make_suffix name suffix) in
+      let _,filename = find_file_in_path ~warn paths name in
       let channel = raw_intern filename in
       let v = marshal_in filename channel in
       close_in channel;
diff --git a/lib/system.mli b/lib/system.mli
index 8cbbb9cab..c9c1df08a 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -36,10 +36,10 @@ val marshal_in : string -> in_channel -> 'a
 
 exception Bad_magic_number of string
 
-val raw_extern_intern : int -> string ->
+val raw_extern_intern : int ->
   (string -> string * out_channel) * (string -> in_channel)
 
-val extern_intern : ?warn:bool -> int -> string ->
+val extern_intern : ?warn:bool -> int ->
   (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a)
 
 val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
diff --git a/library/library.ml b/library/library.ml
index a5f93c02c..edb86bc4c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -318,7 +318,7 @@ let in_import : DirPath.t * bool -> obj =
 (*s Loading from disk to cache (preparation phase) *)
 
 let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern Coq_config.vo_magic_number ".vo"
+  System.raw_extern_intern Coq_config.vo_magic_number
 
 (************************************************************************)
 (*s Locate absolute or partially qualified library names in the path *)
@@ -401,10 +401,10 @@ let mk_library md table digest =
 let fetch_opaque_table (f,pos,digest) =
   try
     let ch = System.with_magic_number_check raw_intern_library f in
-    seek_in ch pos;
+    let () = seek_in ch pos in
     if not (String.equal (System.marshal_in f ch) digest) then failwith "File changed!";
     let table = (System.marshal_in f ch : LightenLibrary.table) in
-    close_in ch;
+    let () = close_in ch in
     table
   with e when Errors.noncritical e ->
     error
diff --git a/library/states.ml b/library/states.ml
index f30633171..906ebdacc 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -18,13 +18,16 @@ 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 ".coq" in
+    extern_intern Coq_config.state_magic_number in
   (fun s ->
+    let s = ensure_suffix s in
     if !Flags.load_proofs <> Flags.Force then
       Errors.error "Write State only works with option -force-load-proofs";
     raw_extern s (freeze())),
   (fun s ->
+    let s = ensure_suffix s in
     unfreeze
       (with_magic_number_check (raw_intern (Library.get_load_paths ())) s);
     Library.overwrite_library_filenames s)