diff options
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 33 |
1 files changed, 13 insertions, 20 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 03074ced..f1d8a492 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -57,28 +57,20 @@ let load_rcfile() = else Flags.if_verbose msg_info (str"Skipping rcfile loading.") -(* Puts dir in the path of ML and in the LoadPath *) -let coq_add_path unix_path s = - Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true; - Mltop.add_ml_dir unix_path - (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = - if !Flags.load_init then - Mltop.add_rec_path ~unix_path ~coq_root ~implicit:true - else - Mltop.add_path ~unix_path ~coq_root ~implicit:false; + Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init); if with_ml then Mltop.add_rec_ml_dir unix_path let add_userlib_path ~unix_path = - Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; + Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; Mltop.add_rec_ml_dir unix_path (* Options -I, -I-as, and -R of the command line *) let includes = ref [] -let push_include s alias recursive implicit = - includes := (s,alias,recursive,implicit) :: !includes +let push_include s alias implicit = + includes := (s, alias, implicit) :: !includes let ml_includes = ref [] let push_ml_include s = ml_includes := s :: !ml_includes @@ -91,10 +83,11 @@ let init_load_path () = let coq_root = Names.DirPath.make [Nameops.coq_root] in (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) - if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; + if Coq_config.local then + Mltop.add_ml_dir (coqlib/"dev"); (* main loops *) if Coq_config.local || !Flags.boot then begin - let () = Mltop.add_ml_dir (coqlib/"stm") in + Mltop.add_ml_dir (coqlib/"stm"); Mltop.add_ml_dir (coqlib/"ide") end; Mltop.add_ml_dir (coqlib/"toploop"); @@ -109,13 +102,13 @@ let init_load_path () = List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs; (* then directories in COQPATH *) List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath; - (* then current directory *) - Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix ~implicit:false; - (* additional loadpath, given with options -I-as, -Q, and -R *) + (* then current directory (not recursively!) *) + Mltop.add_ml_dir "."; + Loadpath.add_load_path "." Nameops.default_root_prefix ~implicit:false; + (* additional loadpath, given with options -Q and -R *) List.iter - (fun (unix_path, coq_root, reci, implicit) -> - (if reci then Mltop.add_rec_path else Mltop.add_path) - ~unix_path ~coq_root ~implicit) + (fun (unix_path, coq_root, implicit) -> + Mltop.add_rec_path ~unix_path ~coq_root ~implicit) (List.rev !includes); (* additional ml directories, given with option -I *) List.iter Mltop.add_ml_dir (List.rev !ml_includes) |