From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 toplevel/coqinit.ml | 38 ++++++++++++++++++++------------------
 1 file changed, 20 insertions(+), 18 deletions(-)

(limited to 'toplevel/coqinit.ml')

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 "\".")
-- 
cgit v1.2.3