diff options
| -rw-r--r-- | tools/coq_makefile.ml | 6 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 8 |
2 files changed, 10 insertions, 4 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index d22072cd35..fcfd00cb40 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -97,9 +97,9 @@ let standard sds = sds; print "\n"; print "install:\n"; - print "\t@if test -z $(TARGETDIR); then echo \"You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')\"; exit 1; fi\n"; - if !some_vfile then print "\tcp -f *.vo $(TARGETDIR)\n"; - if !some_mlfile then print "\tcp -f *.cmo $(TARGETDIR)\n"; + print "\tmkdir -p `$(COQC) -where`/user-contrib\n"; + if !some_vfile then print "\tcp -f *.vo `$(COQC) -where`/user-contrib\n"; + if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\n"; List.iter (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n") sds; 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 |