diff options
| -rw-r--r-- | checker/checker.ml | 15 | ||||
| -rw-r--r-- | tools/coqdep.ml | 1 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 13 |
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 *) |