diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-27 15:54:22 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-27 15:54:22 +0000 |
commit | ba232d00408519083cf45992c06e71eae1c99310 (patch) | |
tree | 6695f62561c045e1afaf5027bf8cb49e6b70f3c0 /toplevel/coqinit.ml | |
parent | d57bd605795c9b3a1e569a2de3ed19852421183f (diff) |
Bug installation non locale
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1228 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/coqinit.ml')
-rw-r--r-- | toplevel/coqinit.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 5f7b4fbea..f70d67741 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -78,11 +78,14 @@ let init_load_path () = ["states"; "dev"]; add_coq_rec_include (Filename.concat Coq_config.coqtop "theories"); add_coq_include (Filename.concat Coq_config.coqtop "tactics"); - add_coq_rec_include (Filename.concat Coq_config.coqtop "contrib"); + add_coq_rec_include (Filename.concat Coq_config.coqtop "contrib") end else begin (* default load path; variable COQLIB overrides the default library *) let coqlib = getenv_else "COQLIB" Coq_config.coqlib in - add_coq_rec_include coqlib + add_coq_include (Filename.concat coqlib "states"); + add_coq_rec_include (Filename.concat coqlib "theories"); + add_coq_include (Filename.concat coqlib "tactics"); + add_coq_rec_include (Filename.concat coqlib "contrib") end; let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in add_ml_include camlp4; |