3 files changed, 40 insertions, 2 deletions
diff --git a/library/library.ml b/library/library.ml
index 893a44921..3bd19dc1a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -11,6 +11,39 @@ open Lib
 (* Modules on disk contain the following informations (after the magic 
    number, and before the digest). *)
 
+let loadpath_name = "LoadPath"
+
+module LoadPath =
+struct
+  let check s = if not (System.exists_dir s) then warning (s^" was not found")
+  let key = Goptions.PrimaryTable loadpath_name
+  let title = "Load Paths for Coq files"
+  let member_message s b =
+    if b then s^" is declared in the load path for Coq files"
+    else s^" is not declared in the load path for Coq files"
+  let synchronous = false
+end
+
+(* This generates commands Add Path, Remove Path, Print Path *)
+module LoadPathTable = Goptions.MakeStringTable(LoadPath)
+
+let get_load_path = LoadPathTable.elements
+let add_path dir = 
+  (Goptions.get_string_table (Goptions.PrimaryTable loadpath_name))#add dir
+let remove_path dir =
+  (Goptions.get_string_table (Goptions.PrimaryTable loadpath_name))#remove dir
+let rec_add_path dir = List.iter add_path (System.all_subdirs dir)
+
+(* Vieilles versions
+let load_path = ref ([] : string list)
+let add_path dir = load_path := dir :: !load_path
+let remove_path dir =
+  if List.mem dir !load_path then
+    load_path := List.filter (fun s -> s <> dir) !load_path
+let get_load_path () = !load_path
+let rec_add_path dir = List.iter add_path (System.all_subdirs dir)
+*)
+
 type module_disk = { 
   md_name : string;
   md_compiled_env : compiled_env;
@@ -92,7 +125,7 @@ let load_objects decls =
   segment_iter load_object decls
 
 let rec load_module_from doexp s f =
-  let (fname,ch) = raw_intern_module f in
+  let (fname,ch) = raw_intern_module (get_load_path ()) f in
   let md = System.marshal_in ch in
   let digest = System.marshal_in ch in
   close_in ch;
diff --git a/library/library.mli b/library/library.mli
index f3899250e..0eb47bd3a 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -32,3 +32,8 @@ val require_module : bool option -> string -> string option -> bool -> unit
 
 val save_module_to : string -> string -> unit
 
+(*s Global load path *)
+val get_load_path : unit -> string list
+val add_path : string -> unit
+val rec_add_path : string -> unit
+val remove_path : string -> unit
diff --git a/library/states.ml b/library/states.ml
index 0e60caecb..b5c45383d 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -20,7 +20,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 s))
+  (fun s -> set_state (raw_intern (Library.get_load_path ()) s))
 
 (* Rollback. *)