diff options
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 38 |
1 files changed, 20 insertions, 18 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 91cec4bb..acbf909c 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -36,7 +36,7 @@ let load_rcfile() = else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else try - let warn x = msg_warning (str x) in + let warn x = Feedback.msg_warning (str x) in let inferedrc = List.find CUnix.file_readable_p [ Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version; Envars.xdg_config_home warn / rcdefaultname; @@ -51,21 +51,20 @@ let load_rcfile() = " found. Skipping rcfile loading.")) *) with reraise -> - let reraise = Errors.push reraise in - let () = msg_info (str"Load of rcfile failed.") in + let reraise = CErrors.push reraise in + let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise else - Flags.if_verbose msg_info (str"Skipping rcfile loading.") + Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.") (* 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); - if with_ml then - Mltop.add_rec_ml_dir unix_path + let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in + Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:(!Flags.load_init) let add_userlib_path ~unix_path = - Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; - Mltop.add_rec_ml_dir unix_path + Mltop.add_rec_path Mltop.AddRecML ~unix_path + ~coq_root:Nameops.default_root_prefix ~implicit:false (* Options -I, -I-as, and -R of the command line *) let includes = ref [] @@ -78,7 +77,7 @@ let push_ml_include s = ml_includes := s :: !ml_includes let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in - let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in + let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in let coqpath = Envars.coqpath in let coq_root = Names.DirPath.make [Nameops.coq_root] in (* NOTE: These directories are searched from last to first *) @@ -90,7 +89,8 @@ let init_load_path () = Mltop.add_ml_dir (coqlib/"stm"); Mltop.add_ml_dir (coqlib/"ide") end; - Mltop.add_ml_dir (coqlib/"toploop"); + if System.exists_dir (coqlib/"toploop") then + Mltop.add_ml_dir (coqlib/"toploop"); (* then standard library *) add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; (* then plugins *) @@ -108,7 +108,7 @@ let init_load_path () = (* additional loadpath, given with options -Q and -R *) List.iter (fun (unix_path, coq_root, implicit) -> - Mltop.add_rec_path ~unix_path ~coq_root ~implicit) + Mltop.add_rec_path Mltop.AddNoML ~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) @@ -125,16 +125,18 @@ let init_ocaml_path () = Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; - [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; + [ "engine" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ]; - [ "grammar" ]; [ "ide" ] ] + [ "grammar" ]; [ "ide" ]; [ "ltac" ]; ] let get_compat_version = function - | "8.5" -> Flags.Current + | "8.6" -> Flags.Current + | "8.5" -> Flags.V8_5 | "8.4" -> Flags.V8_4 | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> - msg_warning (str "Compatibility with version " ++ str s ++ str " not supported."); - Flags.V8_2 - | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".") + CErrors.errorlabstrm "get_compat_version" + (str "Compatibility with version " ++ str s ++ str " not supported.") + | s -> CErrors.errorlabstrm "get_compat_version" + (str "Unknown compatibility version \"" ++ str s ++ str "\".") |