diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-17 12:45:14 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-17 12:45:14 +0200 |
| commit | e7bc24af330f003f7a672b2a27c37ba001e70b2b (patch) | |
| tree | 91b8b2e526052aec8fe6a0aab085c3aa0218fe49 /toplevel/coqinit.ml | |
| parent | 820a453c158006244f02e079d1a820f6670a1293 (diff) | |
No longer add dev/ to the LoadPath, only to the ML path.
This patch should get rid of the following warning:
Invalid character '-' in identifier "v8-syntax".
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index db77877ef..f1d8a4923 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -57,11 +57,6 @@ 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_rec_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 = Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init); @@ -88,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"); |