diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index e7f56ef87a..61b2da2f9e 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -72,14 +72,20 @@ let getenv_else s dft = try Sys.getenv s with Not_found -> dft let init_load_path () = (* developper specific directories to open *) let dev = if Coq_config.local then [ "dev" ] else [] in - let dirs = "states" :: dev @ [ "theories"; "tactics"; "contrib" ] in let coqlib = if Coq_config.local || !Options.boot then Coq_config.coqtop (* variable COQLIB overrides the default library *) else getenv_else "COQLIB" Coq_config.coqlib in + (* first user-contrib *) + let user_contrib = Filename.concat coqlib "user-contrib" in + if Sys.file_exists user_contrib then + Mltop.add_path user_contrib Nametab.default_root_prefix; + (* then standard library *) + let dirs = "states" :: dev @ [ "theories"; "tactics"; "contrib" ] in List.iter (fun s -> coq_add_rec_path (Filename.concat coqlib s)) dirs; let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in add_ml_include camlp4; + (* then current directory *) Mltop.add_path "." Nametab.default_root_prefix; (* additional loadpath, given with -I -include -R options *) List.iter |