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.

5 files changed, 17 insertions, 32 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 5222d8774..db77877ef 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)
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 5f7133c37..c019cc1ce 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -15,8 +15,8 @@ val set_rcfile : string -> unit
 val no_load_rc : unit -> unit
 val load_rcfile : unit -> unit
 
-val push_include : string -> Names.DirPath.t -> bool -> bool -> unit
-(** [push_include phys_path log_path recursive implicit] *)
+val push_include : string -> Names.DirPath.t -> bool -> unit
+(** [push_include phys_path log_path implicit] *)
 
 val push_ml_include : string -> unit
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5795de885..e9e86953b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -135,9 +135,9 @@ let set_outputstate s =
   outputstate:=s
 let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate
 
-let set_include d p recursive implicit =
+let set_include d p implicit =
   let p = dirpath_of_string p in
-  push_include d p recursive implicit
+  push_include d p implicit
 
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
@@ -402,14 +402,12 @@ let parse_args arglist =
     (* Complex options with many args *)
     |"-I"|"-include" ->
       begin match rem with
-      | d :: "-as" :: p :: rem -> set_include d p false true; args := rem
-      | d :: "-as" :: [] -> error_missing_arg "-as"
       | d :: rem -> push_ml_include d; args := rem
       | [] -> error_missing_arg opt
       end
     |"-Q" ->
       begin match rem with
-      | d :: p :: rem -> set_include d p true false; args := rem
+      | d :: p :: rem -> set_include d p false; args := rem
       | _ -> error_missing_arg opt
       end
     |"-R" ->
@@ -417,8 +415,8 @@ let parse_args arglist =
       | d :: "-as" :: [] -> error_missing_arg opt
       | d :: "-as" :: p :: rem ->
         warning "option -R * -as * deprecated, remove the -as";
-        set_include d p true true; args := rem
-      | d :: p :: rem -> set_include d p true true; args := rem
+        set_include d p true; args := rem
+      | d :: p :: rem -> set_include d p true; args := rem
       | _ -> error_missing_arg opt
       end
 
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index ab3636956..0b6fc48c4 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -161,15 +161,6 @@ let add_rec_ml_dir unix_path =
 
 (* Adding files to Coq and ML loadpath *)
 
-let add_path ~unix_path:dir ~coq_root:coq_dirpath ~implicit =
-  if exists_dir dir then
-    begin
-      add_ml_dir dir;
-      Loadpath.add_load_path dir ~implicit coq_dirpath
-    end
-  else
-    msg_warning (str ("Cannot open " ^ dir))
-
 let convert_string d =
   try Names.Id.of_string d
   with UserError _ ->
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 2a91afd88..4f3f4ddde 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -47,7 +47,6 @@ val add_ml_dir : string -> unit
 val add_rec_ml_dir : string -> unit
 
 (** Adds a path to the Coq and ML paths *)
-val add_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
 val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
 
 (** List of modules linked to the toplevel *)