Remove Mltop.add_path as it is no longer possible to import files from subdirectories.

Using Mltop.add_path instead of Mltop.add_rec_path causes the following
kind of behavior:

$ coqtop -nois
Coq < Require Import Coq.Init.Datatypes.
Error: Cannot find a physical path bound to logical path Coq.Init.

The only case where its use is still warranted is the implicit "." path. It
shall not be recursive because Coq might be called from about anywhere.

This patch also removes -I-as since its behavior is no longer the one from
8.4 so it is not worth keeping it around.

1 files changed, 10 insertions, 13 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 5222d87749..db77877efd 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -59,15 +59,12 @@ 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
 
@@ -77,8 +74,8 @@ let add_userlib_path ~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)