Nettoyage et documentation de Library

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

3 files changed, 153 insertions, 199 deletions

diff --git a/library/library.ml b/library/library.ml
index 388580eab..fee383233 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -25,9 +25,9 @@ open Declaremods
 
 type logical_path = dir_path
 
-let load_path = ref ([],[] : System.physical_path list * logical_path list)
+let load_paths = ref ([],[] : System.physical_path list * logical_path list)
 
-let get_load_path () = fst !load_path
+let get_load_paths () = fst !load_paths
 
 (* Hints to partially detects if two paths refer to the same repertory *)
 let rec remove_path_dot p = 
@@ -60,17 +60,17 @@ let canonical_path_name p =
 
 let find_logical_path phys_dir = 
   let phys_dir = canonical_path_name phys_dir in
-  match list_filter2 (fun p d -> p = phys_dir) !load_path with
+  match list_filter2 (fun p d -> p = phys_dir) !load_paths with
   | _,[dir] -> dir
   | _,[] -> Nameops.default_root_prefix
   | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
-let remove_path dir =
-  load_path := list_filter2 (fun p d -> p <> dir) !load_path
+let remove_load_path dir =
+  load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
 
-let add_load_path_entry (phys_path,coq_path) =
+let add_load_path (phys_path,coq_path) =
   let phys_path = canonical_path_name phys_path in
-  match list_filter2 (fun p d -> p = phys_path) !load_path with
+  match list_filter2 (fun p d -> p = phys_path) !load_paths with
   | _,[dir] ->
       if coq_path <> dir 
         (* If this is not the default -I . to coqtop *)
@@ -85,19 +85,19 @@ let add_load_path_entry (phys_path,coq_path) =
 	    ^(string_of_dirpath dir)
 	    ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
              flush_all ());
-	  remove_path phys_path;
-	  load_path := (phys_path::fst !load_path, coq_path::snd !load_path)
+	  remove_load_path phys_path;
+	  load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
 	end
   | _,[] ->
-      load_path := (phys_path :: fst !load_path, coq_path :: snd !load_path)
+      load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
   | _ -> anomaly ("Two logical paths are associated to "^phys_path)
 
 let physical_paths (dp,lp) = dp
 
-let load_path_of_logical_path dir =
-  fst (list_filter2 (fun p d -> d = dir) !load_path)
+let load_paths_of_dir_path dir =
+  fst (list_filter2 (fun p d -> d = dir) !load_paths)
 
-let get_full_load_path () = List.combine (fst !load_path) (snd !load_path)
+let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
 
 (************************************************************************)
 (*s Modules on disk contain the following informations (after the magic 
@@ -124,7 +124,7 @@ type library_t = {
   library_imports : compilation_unit_name list;
   library_digest : Digest.t }
 
-module CompilingLibraryOrdered = 
+module LibraryOrdered = 
   struct
     type t = dir_path
     let compare d1 d2 =
@@ -132,12 +132,12 @@ module CompilingLibraryOrdered =
         (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
   end
 
-module CompilingLibraryMap = Map.Make(CompilingLibraryOrdered)
+module LibraryMap = Map.Make(LibraryOrdered)
 
-(* This is a map from names to libraries *)
-let libraries_table = ref CompilingLibraryMap.empty
+(* This is a map from names to loaded libraries *)
+let libraries_table = ref LibraryMap.empty
 
-(* These are the _ordered_ lists of loaded, imported and exported libraries *)
+(* These are the _ordered_ sets of loaded, imported and exported libraries *)
 let libraries_loaded_list = ref []
 let libraries_imports_list = ref []
 let libraries_exports_list = ref []
@@ -155,7 +155,7 @@ let unfreeze (mt,mo,mi,me) =
   libraries_exports_list := me
 
 let init () =
-  libraries_table := CompilingLibraryMap.empty;
+  libraries_table := LibraryMap.empty;
   libraries_loaded_list := [];
   libraries_imports_list := [];
   libraries_exports_list := []
@@ -168,18 +168,32 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section = false }
 
-let find_library s =
-  CompilingLibraryMap.find s !libraries_table
+(* cache for libraries loaded in memory but not necessarily in environment *)
+let compunit_cache = ref LibraryMap.empty
 
-let try_find_library s =
-  try find_library s
+let _ = 
+  Summary.declare_summary "MODULES-CACHE"
+    { Summary.freeze_function = (fun () -> !compunit_cache);
+      Summary.unfreeze_function = (fun cu -> compunit_cache := cu);
+      Summary.init_function = 
+	(fun () -> compunit_cache := LibraryMap.empty);
+      Summary.survive_module = true;
+      Summary.survive_section = true }
+
+(* various requests to the tables *)
+
+let find_library dir =
+  LibraryMap.find dir !libraries_table
+
+let try_find_library dir =
+  try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (string_of_dirpath s))
+    error ("Unknown library " ^ (string_of_dirpath dir))
 
-let library_full_filename m = (find_library m).library_filename
+let library_full_filename dir = (find_library dir).library_filename
 
 let library_is_loaded dir =
-  try let _ = CompilingLibraryMap.find dir !libraries_table in true
+  try let _ = LibraryMap.find dir !libraries_table in true
   with Not_found -> false
 
 let library_is_opened dir = 
@@ -203,7 +217,7 @@ let register_loaded_library m =
     | m'::_ as l when m'.library_name = m.library_name -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;
-  libraries_table := CompilingLibraryMap.add m.library_name m !libraries_table
+  libraries_table := LibraryMap.add m.library_name m !libraries_table
 
   (* ... while if a library is imported/exported several time, then
      only the last occurrence is really needed - though the imported
@@ -225,10 +239,8 @@ let register_open_library export m =
 (************************************************************************)
 (*s Opening libraries *)
 
-(*s [open_library s] opens a library. The library [s] and all
-  libraries needed by [s] are assumed to be already loaded. When
-  opening [s] we recursively open all the libraries needed by [s]
-  and tagged [exported]. *)
+(* [open_library export explicit m] opens library [m] if not already
+   opened _or_ if explicitly asked to be (re)opened *)
 
 let eq_lib_name m1 m2 = m1.library_name = m2.library_name
 
@@ -246,6 +258,9 @@ let open_library export explicit_libs m =
     if export then 
       libraries_exports_list := remember_last_of_each !libraries_exports_list m
 
+(* open_libraries recursively open a list of libraries but opens only once 
+   a library that is re-exported many times *)
+
 let open_libraries export modl = 
   let to_open_list = 
     List.fold_left
@@ -288,6 +303,8 @@ let (in_import, out_import) =
 
 
 (************************************************************************)
+(*s Low-level interning/externing of libraries to files *)
+
 (*s Loading from disk to cache (preparation phase) *)
 
 let vo_magic_number7 = 07992 (* V8.0 final old syntax *)
@@ -314,23 +331,16 @@ let raw_intern_library a =
 let raw_extern_library =
   if !Options.v7 then raw_extern_library7 else raw_extern_library8
 
-(* cache for loaded libraries *)
-let compunit_cache = ref CompilingLibraryMap.empty
-
-let _ = 
-  Summary.declare_summary "MODULES-CACHE"
-    { Summary.freeze_function = (fun () -> !compunit_cache);
-      Summary.unfreeze_function = (fun cu -> compunit_cache := cu);
-      Summary.init_function = 
-	(fun () -> compunit_cache := CompilingLibraryMap.empty);
-      Summary.survive_module = true;
-      Summary.survive_section = true }
+let with_magic_number_check f a =
+  try f a
+  with System.Bad_magic_number fname ->
+    errorlabstrm "with_magic_number_check"
+    (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
+    spc () ++ str"It is corrupted" ++ spc () ++
+    str"or was compiled with another version of Coq.")
 
-(*s [load_library s] loads the library [s] from the disk, and [find_library s]
-   returns the library of name [s], loading it if necessary. 
-   The boolean [doexp] specifies if we open the libraries which are declared
-   exported in the dependencies (it is [true] at the highest level;
-   then same value as for caller is reused in recursive loadings). *)
+(************************************************************************)
+(*s Locate absolute or partially qualified library names in the path *)
 
 exception LibUnmappedDir
 exception LibNotFound
@@ -339,7 +349,7 @@ type library_location = LibLoaded | LibInPath
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
-  let loadpath = load_path_of_logical_path pref in
+  let loadpath = load_paths_of_dir_path pref in
   if loadpath = [] then raise LibUnmappedDir;
   try
     let name = (string_of_id base)^".vo" in
@@ -352,13 +362,29 @@ let locate_absolute_library dir =
   with Not_found ->
     raise LibNotFound
 
-let with_magic_number_check f a =
-  try f a
-  with System.Bad_magic_number fname ->
-    errorlabstrm "with_magic_number_check"
-    (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
-    spc () ++ str"It is corrupted" ++ spc () ++
-    str"or was compiled with another version of Coq.")
+let locate_qualified_library qid =
+  try
+    (* Search library in loadpath *)
+    let dir, base = repr_qualid qid in 
+    let loadpath =
+      if repr_dirpath dir = [] then get_load_paths ()
+      else 
+        (* we assume dir is an absolute dirpath *)
+	load_paths_of_dir_path dir
+    in
+    if loadpath = [] then raise LibUnmappedDir;
+    let name =  (string_of_id base)^".vo" in
+    let path, file = System.where_in_path loadpath name in
+    let dir = extend_dirpath (find_logical_path path) base in
+    (* Look if loaded *)
+    try 
+      (LibLoaded, dir, library_full_filename dir)      
+    with Not_found ->
+      (LibInPath, dir, file)
+  with Not_found -> raise LibNotFound
+
+(************************************************************************)
+(* Internalise libraries *)
 
 let lighten_library m = 
   if !Options.dont_load_proofs then lighten_library m else m
@@ -382,11 +408,11 @@ let intern_from_file f =
 let rec intern_library (dir, f) =
   try
     (* Look if in the current logical environment *)
-    CompilingLibraryMap.find dir !libraries_table
+    LibraryMap.find dir !libraries_table
   with Not_found ->
   try
     (* Look if already loaded in cache and consequently its dependencies *)
-    CompilingLibraryMap.find dir !compunit_cache
+    LibraryMap.find dir !compunit_cache
   with Not_found ->
     (* [dir] is an absolute name which matches [f] which must be in loadpath *)
     let m = intern_from_file f in
@@ -398,12 +424,12 @@ let rec intern_library (dir, f) =
     intern_and_cache_library dir m
 
 and intern_and_cache_library dir m =
-  compunit_cache := CompilingLibraryMap.add dir m !compunit_cache;
+  compunit_cache := LibraryMap.add dir m !compunit_cache;
   try
     List.iter (intern_mandatory_library dir) m.library_deps;
     m
   with e ->
-    compunit_cache := CompilingLibraryMap.remove dir !compunit_cache; 
+    compunit_cache := LibraryMap.remove dir !compunit_cache; 
     raise e
 
 and intern_mandatory_library caller (dir,d) =
@@ -443,7 +469,7 @@ let rec_intern_by_filename_only id f =
   check_library_short_name f m.library_name id;
   (* We check no other file containing same library is loaded *)
   try
-    let m' = CompilingLibraryMap.find m.library_name !libraries_table in
+    let m' = LibraryMap.find m.library_name !libraries_table in
     Options.if_verbose warning 
       ((string_of_dirpath m.library_name)^" is already loaded from file "^
        m'.library_filename);
@@ -452,27 +478,6 @@ let rec_intern_by_filename_only id f =
     let m = intern_and_cache_library m.library_name m in
     m.library_name
 
-let locate_qualified_library qid =
-  try
-    (* Search library in loadpath *)
-    let dir, base = repr_qualid qid in 
-    let loadpath =
-      if repr_dirpath dir = [] then get_load_path ()
-      else 
-        (* we assume dir is an absolute dirpath *)
-	load_path_of_logical_path dir
-    in
-    if loadpath = [] then raise LibUnmappedDir;
-    let name =  (string_of_id base)^".vo" in
-    let path, file = System.where_in_path loadpath name in
-    let dir = extend_dirpath (find_logical_path path) base in
-    (* Look if loaded *)
-    try 
-      (LibLoaded, dir, library_full_filename dir)      
-    with Not_found ->
-      (LibInPath, dir, file)
-  with Not_found -> raise LibNotFound
-
 let rec_intern_qualified_library (loc,qid) =
   try
     let (_,dir,f) = locate_qualified_library qid in
@@ -491,7 +496,7 @@ let rec_intern_qualified_library (loc,qid) =
 
 let rec_intern_library_from_file idopt f =
   (* A name is specified, we have to check it contains library id *)
-  let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
+  let _, f = System.find_file_in_path (get_load_paths ()) (f^".vo") in
   rec_intern_by_filename_only idopt f
 
 (**********************************************************************)
@@ -519,11 +524,11 @@ let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir))
 let rec load_library dir =
   try
     (* Look if loaded in current env (and consequently its dependencies) *)
-    CompilingLibraryMap.find dir !libraries_table
+    LibraryMap.find dir !libraries_table
   with Not_found ->
     (* [dir] is an absolute name matching [f] which must be in loadpath *)
     let m =
-      try CompilingLibraryMap.find dir !compunit_cache
+      try LibraryMap.find dir !compunit_cache
       with Not_found ->
         anomaly ((string_of_dirpath dir)^" should be in cache")
     in
@@ -556,57 +561,39 @@ let (in_require, out_require) =
        export_function = export_require;
        classify_function = (fun (_,o) -> Anticipate o) }
 
+(* Require libraries, import them if [export <> None], mark them for export
+   if [export = Some true] *)
+
+(* read = require without opening *)
+
 let xml_require = ref (fun d -> ())
 let set_xml_require f = xml_require := f
 
-let require_library spec qidl export =
-(*
-  if sections_are_opened () && Options.verbose () then
-    warning ("Objets of "^(string_of_library modref)^
-             " not surviving sections (e.g. Grammar \nand Hints)\n"^
-             "will be removed at the end of the section");
-*)
+let require_library qidl export =
   let modrefl = List.map rec_intern_qualified_library qidl in
     if Lib.is_modtype () || Lib.is_module () then begin
       add_anonymous_leaf (in_require (modrefl,None));
-      List.iter
-	(fun dir ->
-	   add_anonymous_leaf (in_import (dir, export)))
-	modrefl
+      option_iter (fun exp ->
+	List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
+	export
     end
     else
-      add_anonymous_leaf (in_require (modrefl,Some export));
+      add_anonymous_leaf (in_require (modrefl,export));
   if !Options.xml_export then List.iter !xml_require modrefl;
   add_frozen_state ()
 
-let require_library_from_file spec idopt file export =
+let require_library_from_file idopt file export =
   let modref = rec_intern_library_from_file idopt file in
     if Lib.is_modtype () || Lib.is_module () then begin
       add_anonymous_leaf (in_require ([modref],None));
-      add_anonymous_leaf (in_import (modref, export))
+      option_iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
+	export
     end
     else
-      add_anonymous_leaf (in_require ([modref],Some export));
+      add_anonymous_leaf (in_require ([modref],export));
     if !Options.xml_export then !xml_require modref;
     add_frozen_state ()
 
-
-(* read = require without opening *)
-
-let read_library qid =
-  let modref = rec_intern_qualified_library qid in
-  add_anonymous_leaf (in_require ([modref],None));
-  if !Options.xml_export then !xml_require modref;
-  add_frozen_state ()
-
-let read_library_from_file f =
-  let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
-  let modref = rec_intern_by_filename_only None f in
-  add_anonymous_leaf (in_require ([modref],None));
-  if !Options.xml_export then !xml_require modref;
-  add_frozen_state ()
-
-
 (* called at end of section *)
 
 let reload_library modrefl =
@@ -617,7 +604,7 @@ let reload_library modrefl =
 
 (* the function called by Vernacentries.vernac_import *)
 
-let import_library export (loc,qid) =
+let import_module export (loc,qid) =
   try
     match Nametab.locate_module qid with
 	MPfile dir -> 
@@ -634,27 +621,30 @@ let import_library export (loc,qid) =
 	 str ((string_of_qualid qid)^" is not a module"))
   
 (************************************************************************)
-(*s [save_library s] saves the library [m] to the disk. *)
+(*s Initializing the compilation of a library. *)
 
 let start_library f = 
   let _,longf = 
-    System.find_file_in_path (get_load_path ()) (f^".v") in
+    System.find_file_in_path (get_load_paths ()) (f^".v") in
   let ldir0 = find_logical_path (Filename.dirname longf) in
   let id = id_of_string (Filename.basename f) in
   let ldir = extend_dirpath ldir0 id in
   Declaremods.start_library ldir;
   ldir,longf
 
+(************************************************************************)
+(*s [save_library dir] ends library [dir] and save it to the disk. *)
+
 let current_deps () =
   List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list
 
 let current_reexports () =
   List.map (fun m -> m.library_name) !libraries_exports_list
 
-let save_library_to s f =
-  let cenv, seg = Declaremods.end_library s in
+let save_library_to dir f =
+  let cenv, seg = Declaremods.end_library dir in
   let md = { 
-    md_name = s;
+    md_name = dir;
     md_compiled = cenv;
     md_objects = seg;
     md_deps = current_deps ();
@@ -668,33 +658,7 @@ let save_library_to s f =
     close_out ch
   with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e)
 
-(*s Pretty-printing of libraries state. *)
- 
-(* this function is not used... *)
-let fmt_libraries_state () =
-  let opened = opened_libraries ()
-  and loaded = loaded_libraries () in
-  (str "Imported (open) Modules: " ++
-     prlist_with_sep pr_spc pr_dirpath opened ++ fnl () ++
-     str "Loaded Modules: " ++
-     prlist_with_sep pr_spc pr_dirpath loaded ++ fnl ())
-
-
-(*s For tactics/commands requiring vernacular libraries *)
-
-let check_required_library d =
-  let d' = List.map id_of_string d in
-  let dir = make_dirpath (List.rev d') in
-  if not (library_is_loaded dir) then
-(* Loading silently ...
-    let m, prefix = list_sep_last d' in
-    read_library 
-     (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
-*)
-(* or failing ...*)
-    error ("Library "^(list_last d)^" has to be required first")
-
-
+(************************************************************************)
 (*s Display the memory use of a library. *)
 
 open Printf
diff --git a/library/library.mli b/library/library.mli
index 02f01967c..4ecc76809 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -15,65 +15,58 @@ open Libnames
 open Libobject
 (*i*)
 
-(*s This module is the heart of the library. It provides low level
-  functions to load, open and save libraries. Libraries are saved
-  onto the disk with checksums (obtained with the [Digest] module),
-  which are checked at loading time to prevent inconsistencies
-  between files written at various dates. It also provides a high
-  level function [require] which corresponds to the vernacular
-  command [Require]. *)
+(*s This module provides functions to load, open and save
+  libraries. Libraries correspond to the subclass of modules that
+  coincide with a file on disk (the ".vo" files). Libraries on the
+  disk comes with checksums (obtained with the [Digest] module), which
+  are checked at loading time to prevent inconsistencies between files
+  written at various dates.
+*)
+
+(*s Require = load in the environment + open (if the optional boolean
+    is not [None]); mark also for export if the boolean is [Some true] *)
+val require_library : qualid located list -> bool option -> unit
+val require_library_from_file :
+  identifier option -> System.physical_path -> bool option -> unit
 
-val read_library : qualid located -> unit
+(*s Open a module (or a library); if the boolean is true then it's also
+   an export otherwise just a simple import *)
+val import_module : bool -> qualid located -> unit
 
-val read_library_from_file : System.physical_path -> unit
+(*s Start the compilation of a library *)
+val start_library : string -> dir_path * string
 
-(* [import_library true qid] = [export qid] *)
- 
-val import_library : bool -> qualid located -> unit
+(*s End the compilation of a library and save it to a ".vo" file *)
+val save_library_to : dir_path -> string -> unit
 
+(*s Interrogate the status of libraries *)
+
+  (* - Tell if a library is loaded or opened *)
 val library_is_loaded : dir_path -> bool
 val library_is_opened : dir_path -> bool
 
+  (* - Tell which libraries are loaded or imported *)
 val loaded_libraries : unit -> dir_path list
 val opened_libraries : unit -> dir_path list
 
-val fmt_libraries_state : unit -> Pp.std_ppcmds
-
-(*s Require. The command [require_library spec m file export] loads and opens
-  a library [m]. [file] specifies the filename, if not [None]. [spec]
-  specifies to look for a specification ([true]) or for an implementation
-  ([false]), if not [None]. And [export] specifies if the library must be 
-  exported. *)
-
-val require_library :
-  bool option -> qualid located list -> bool -> unit
-
-val require_library_from_file :
-  bool option -> identifier option -> System.physical_path -> bool -> unit
-
-val set_xml_require : (dir_path -> unit) -> unit
-
-(*s [save_library_to s f] saves the current environment as a library [s]
-  in the file [f]. *)
-
-val start_library : string -> dir_path * string
-val save_library_to : dir_path -> string -> unit
-
-(* [library_full_filename] returns the full filename of a loaded library. *)
-
+  (* - Return the full filename of a loaded library. *)
 val library_full_filename : dir_path -> string
 
+(*s Hook for the xml exportation of libraries *)
+val set_xml_require : (dir_path -> unit) -> unit
 
-(*s Global load path *)
-type logical_path = dir_path
+(*s Global load paths: a load path is a physical path in the file
+    system; to each load path is associated a Coq [dir_path] (the "logical"
+    path of the physical path) *)
 
-val get_load_path : unit -> System.physical_path list
-val get_full_load_path : unit -> (System.physical_path * logical_path) list
-val add_load_path_entry : System.physical_path * logical_path -> unit
-val remove_path : System.physical_path -> unit
-val find_logical_path : System.physical_path -> logical_path
-val load_path_of_logical_path : dir_path -> System.physical_path list
+val get_load_paths : unit -> System.physical_path list
+val get_full_load_paths : unit -> (System.physical_path * dir_path) list
+val add_load_path : System.physical_path * dir_path -> unit
+val remove_load_path : System.physical_path -> unit
+val find_logical_path : System.physical_path -> dir_path
+val load_paths_of_dir_path : dir_path -> System.physical_path list
 
+(*s Locate a library in the load paths *)
 exception LibUnmappedDir
 exception LibNotFound
 type library_location = LibLoaded | LibInPath
@@ -81,13 +74,10 @@ type library_location = LibLoaded | LibInPath
 val locate_qualified_library :
   qualid -> library_location * dir_path * System.physical_path
 
-
-val check_required_library : string list -> unit
-
-(*s Displays the memory use of a library. *)
+(*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds
 
-(* For discharge *)
+(*s For discharge *)
 type library_reference
 
 val out_require : Libobject.obj -> library_reference
diff --git a/library/states.ml b/library/states.ml
index 0fa62265a..2a34c8753 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -24,7 +24,7 @@ let state_magic_number = 19764
 let (extern_state,intern_state) =
   let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
   (fun s -> raw_extern s (get_state())),
-  (fun s -> set_state (raw_intern (Library.get_load_path ()) s))
+  (fun s -> set_state (raw_intern (Library.get_load_paths ()) s))
 
 (* Rollback. *)