diff options
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 27 |
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" ] ] |