diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 24 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 3 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
3 files changed, 11 insertions, 17 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 7b3fa1628..01dec915a 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -70,22 +70,14 @@ let getenv_else s dft = try Sys.getenv s with Not_found -> dft (* Initializes the LoadPath according to COQLIB and Coq_config *) let init_load_path () = - if Coq_config.local then begin - (* local use (no installation) *) - List.iter - (fun s -> coq_add_path (Filename.concat Coq_config.coqtop s)) - ["states"; "dev"]; - coq_add_rec_path (Filename.concat Coq_config.coqtop "theories"); - coq_add_path (Filename.concat Coq_config.coqtop "tactics"); - coq_add_rec_path (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 - coq_add_path (Filename.concat coqlib "states"); - coq_add_rec_path (Filename.concat coqlib "theories"); - coq_add_path (Filename.concat coqlib "tactics"); - coq_add_rec_path (Filename.concat coqlib "contrib") - end; + (* developper specific directories to open *) + let dev = if Coq_config.local then [ "dev" ] else [] in + let dirs = "states" :: dev @ [ "theories"; "tactics"; "contrib" ] in + let coqlib = + if Coq_config.local || !Options.boot then Coq_config.coqtop + (* variable COQLIB overrides the default library *) + else getenv_else "COQLIB" Coq_config.coqlib in + List.iter (fun s -> coq_add_rec_path (Filename.concat coqlib s)) dirs; let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in add_ml_include camlp4; Mltop.add_path "." [Nametab.default_root]; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0778b7735..9e9c3436a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -120,7 +120,8 @@ let parse_args () = | "-full" :: rem -> warning "option -full deprecated\n"; parse rem | "-batch" :: rem -> set_batch_mode (); parse rem - + | "-boot" :: rem -> boot := true; no_load_rc (); set_batch_mode (); + parse rem | "-outputstate" :: s :: rem -> set_outputstate s; parse rem | "-outputstate" :: [] -> usage () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8dc848d3c..f9d5decd9 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -47,6 +47,7 @@ let print_usage_channel co command = -init-file f set the rcfile to f -user u use the rcfile of user u -batch batch mode (exits just after arguments parsing) + -boot boot mode (implies -q and -batch) -emacs tells Coq it is executed under Emacs " |