Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir

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

2 files changed, 0 insertions, 18 deletions

diff --git a/library/library.ml b/library/library.ml
index a493be013..6ff8a84db 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -17,25 +17,9 @@ let get_load_path () = !load_path
 
 let add_load_path_entry lpe = load_path := lpe :: !load_path
 
-let add_path dir coq_dirpath = 
-  if coq_dirpath = [] then anomaly "add_path: empty path in library";
-  Nametab.push_library_root (List.hd coq_dirpath);
-  if exists_dir dir then
-    add_load_path_entry { directory = dir; coq_dirpath = coq_dirpath }
-  else
-    wARNING [< 'sTR ("Cannot open " ^ dir) >]
-
-
 let remove_path dir =
   load_path := List.filter (fun lpe -> lpe.directory <> dir) !load_path
 
-let rec_add_path dir coq_dirpath =
-  if coq_dirpath = [] then anomaly "add_path: empty path in library";
-  Nametab.push_library_root (List.hd coq_dirpath);
-  let dirs = all_subdirs dir (Some coq_dirpath) in
-  if dirs = [] then wARNING [< 'sTR ("Cannot open " ^ dir) >];
-  load_path := dirs @ !load_path
-
 (*s Modules on disk contain the following informations (after the magic 
     number, and before the digest). *)
 
diff --git a/library/library.mli b/library/library.mli
index f937e30ab..18ebb9708 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -58,6 +58,4 @@ val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit
 (*s Global load path *)
 val get_load_path : unit -> System.load_path
 val add_load_path_entry : System.load_path_entry -> unit
-val add_path : unix_path:string -> coq_root:dir_path -> unit
-val rec_add_path : unix_path:string -> coq_root:dir_path -> unit
 val remove_path : string -> unit