Reorder search path order, so the standard library is search last.

This allows the construction of an extended library that shadows the standard
library.

Signed-off-by: Tom Prince <tom.prince@ualberta.net>

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

3 files changed, 14 insertions, 15 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index e8cc52ecf9..c2c21fbe29 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -103,17 +103,14 @@ let init_load_path () =
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let plugins = coqlib/"plugins" in
-  (* first user-contrib *)
-  if Sys.file_exists user_contrib then
-    add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
+  (* NOTE: These directories are searched from last to first *)
+  (* first standard library *)
+  add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.make_dirpath[coq_root]);
   (* then plugins *)
   add_rec_path ~unix_path:plugins ~coq_root:(Names.make_dirpath [coq_root]);
-  (* then standard library *)
-(*  List.iter
-    (fun (s,alias) ->
-      add_rec_path (coqlib/s) ([alias; coq_root]))
-    theories_dirs_map;*)
-  add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.make_dirpath[coq_root]);
+  (* then user-contrib *)
+  if Sys.file_exists user_contrib then
+    add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
   (* then current directory *)
   add_path ~unix_path:"." ~coq_root:Check.default_root_prefix;
   (* additional loadpath, given with -I -include -R options *)
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index e9226d3836..ccce7cd311 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -190,6 +190,7 @@ let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
   parse (List.tl (Array.to_list Sys.argv));
   if not Coq_config.has_natdynlink then option_natdynlk := false;
+  (* NOTE: These directories are searched from last to first *)
   if !Flags.boot then begin
     add_rec_dir add_known "theories" ["Coq"];
     add_rec_dir add_known "plugins" ["Coq"]
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 7ffb5a5f3a..d7031297d6 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -92,17 +92,18 @@ let init_load_path () =
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let dirs = ["states";"plugins"] in
-    (* first user-contrib *)
-    if Sys.file_exists user_contrib then
-      Mltop.add_rec_path ~unix_path:user_contrib ~coq_root:Nameops.default_root_prefix;
-    (* then states, theories and dev *)
-    List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
-    (* developer specific directory to open *)
+    (* NOTE: These directories are searched from last to first *)
+    (* first, developer specific directory to open *)
     if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
     (* then standard library *)
     List.iter
       (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root]))
       theories_dirs_map;
+    (* then states and plugins *)
+    List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
+    (* then user-contrib *)
+    if Sys.file_exists user_contrib then
+      Mltop.add_rec_path ~unix_path:user_contrib ~coq_root:Nameops.default_root_prefix;
     (* then current directory *)
     Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix;
     (* additional loadpath, given with -I -include -R options *)