summaryrefslogtreecommitdiff
path: root/toplevel/coqinit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqinit.ml')
-rw-r--r--toplevel/coqinit.ml27
1 files changed, 10 insertions, 17 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 884589e7..d32a773d 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqinit.ml 10901 2008-05-07 18:53:48Z letouzey $ *)
+(* $Id: coqinit.ml 11749 2009-01-05 14:01:04Z notin $ *)
open Pp
open System
@@ -93,16 +93,11 @@ let theories_dirs_map = [
"theories/Init", "Init"
]
-(* Initializes the LoadPath according to COQLIB and Coq_config *)
+(* Initializes the LoadPath *)
let init_load_path () =
- let coqlib =
- (* variable COQLIB overrides the default library *)
- getenv_else "COQLIB"
- (if Coq_config.local || !Flags.boot then Coq_config.coqtop
- else Coq_config.coqlib) in
+ let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
let dirs = "states" :: ["contrib"] in
- let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
(* first user-contrib *)
if Sys.file_exists user_contrib then
Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
@@ -114,8 +109,6 @@ let init_load_path () =
List.iter
(fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root]))
theories_dirs_map;
- (* then camlp4lib *)
- add_ml_include camlp4;
(* then current directory *)
Mltop.add_path "." Nameops.default_root_prefix;
(* additional loadpath, given with -I -include -R options *)
@@ -129,13 +122,13 @@ let init_library_roots () =
(* Initialises the Ocaml toplevel before launching it, so that it can
find the "include" file in the *source* directory *)
-(* We only assume that the variable COQTOP is set *)
let init_ocaml_path () =
- let coqtop = getenv_else "COQTOP" Coq_config.coqtop in
+ let coqsrc = Coq_config.coqsrc in
let add_subdir dl =
- Mltop.add_ml_dir (List.fold_left (/) coqtop dl)
+ Mltop.add_ml_dir (List.fold_left (/) coqsrc dl)
in
- List.iter add_subdir
- [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
- [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
- [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]
+ Mltop.add_ml_dir (Envars.coqlib ());
+ List.iter add_subdir
+ [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
+ [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
+ [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]