diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-05 00:20:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-05 00:20:54 +0200 |
| commit | 34e6a7149a69791cc736bdd9b2b909be9f21ec8f (patch) | |
| tree | f33a4ed37d7fff96df7a720fe6146ecce56aba81 /toplevel/coqinit.ml | |
| parent | 72644c7f7b3f0fcc56779acfcfa4bfc9f041ebde (diff) | |
| parent | df54c829a4c06a93de47df4e8ccc441721360da8 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 3385d67e3..f0cac72d0 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"); @@ -138,6 +134,6 @@ let get_compat_version = function | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> - msg_warning (strbrk ("Compatibility with version "^s^" not supported.")); + msg_warning (str "Compatibility with version " ++ str s ++ str " not supported."); Flags.V8_2 - | s -> Errors.error ("Unknown compatibility version \""^s^"\".") + | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".") |