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

1 files changed, 6 insertions, 9 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index e8cc52ecf..c2c21fbe2 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 *)