Merge branch 'v8.5' into trunk

1 files changed, 11 insertions, 14 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 1ce3fe28d..3385d67e3 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -59,26 +59,23 @@ let load_rcfile() =
 
 (* Puts dir in the path of ML and in the LoadPath *)
 let coq_add_path unix_path s =
-  Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true;
+  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 =
-  if !Flags.load_init then
-    Mltop.add_rec_path ~unix_path ~coq_root ~implicit:true
-  else
-    Mltop.add_path ~unix_path ~coq_root ~implicit:false;
+  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_userlib_path ~unix_path =
-  Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false;
+  Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false;
   Mltop.add_rec_ml_dir unix_path
 
 (* Options -I, -I-as, and -R of the command line *)
 let includes = ref []
-let push_include s alias recursive implicit =
-  includes := (s,alias,recursive,implicit) :: !includes
+let push_include s alias implicit =
+  includes := (s, alias, implicit) :: !includes
 let ml_includes = ref []
 let push_ml_include s = ml_includes := s :: !ml_includes
 
@@ -109,13 +106,13 @@ let init_load_path () =
     List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs;
     (* then directories in COQPATH *)
     List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath;
-    (* then current directory *)
-    Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix ~implicit:false;
-    (* additional loadpath, given with options -I-as, -Q, and -R *)
+    (* then current directory (not recursively!) *)
+    Mltop.add_ml_dir ".";
+    Loadpath.add_load_path "." Nameops.default_root_prefix ~implicit:false;
+    (* additional loadpath, given with options -Q and -R *)
     List.iter
-      (fun (unix_path, coq_root, reci, implicit) ->
-        (if reci then Mltop.add_rec_path else Mltop.add_path)
-          ~unix_path ~coq_root ~implicit)
+      (fun (unix_path, coq_root, implicit) ->
+        Mltop.add_rec_path ~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)