Merge branch 'v8.5' into trunk

7 files changed, 47 insertions, 50 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 1ce3fe28da..3385d67e31 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)
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 5f7133c37c..c019cc1ced 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 22ab469dcb..1544fd8696 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,21 +402,21 @@ 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" ->
       begin match rem with
-      | d :: "-as" :: [] -> error_missing_arg "-as"
-      | d :: "-as" :: p :: rem
-      | d :: p :: rem -> set_include d p true true; args := rem
+      | d :: "-as" :: [] -> error_missing_arg opt
+      | d :: "-as" :: p :: rem ->
+        warning "option -R * -as * deprecated, remove the -as";
+        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 e7500f6ae4..2362d250ed 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 ~root:true ~implicit coq_dirpath
-    end
-  else
-    msg_warning (str ("Cannot open " ^ dir))
-
 let convert_string d =
   try Names.Id.of_string d
   with UserError _ ->
@@ -189,9 +180,9 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
     let dirs = List.map_filter convert_dirs dirs in
     let () = add_ml_dir unix_path in
     let add (path, dir) =
-      Loadpath.add_load_path path ~root:false ~implicit dir in
+      Loadpath.add_load_path path ~implicit dir in
     let () = List.iter add dirs in
-    Loadpath.add_load_path unix_path ~root:true ~implicit coq_root
+    Loadpath.add_load_path unix_path ~implicit coq_root
   else
     msg_warning (str ("Cannot open " ^ unix_path))
 
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 2a91afd88e..4f3f4ddde4 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 *)
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 4ee3bc4745..f053839c70 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -23,9 +23,7 @@ let print_usage_channel co command =
   output_string co
 "  -I dir                 look for ML files in dir\
 \n  -include dir           (idem)\
-\n  -I dir -as coqdir      implicitly map physical dir to logical coqdir\
-\n  -R dir -as coqdir      recursively map physical dir to logical coqdir\
-\n  -R dir coqdir          (idem)\
+\n  -R dir coqdir          recursively map physical dir to logical coqdir\
 \n  -Q dir coqdir          map physical dir to logical coqdir\
 \n  -top coqdir            set the toplevel name to be coqdir instead of Top\
 \n  -notop                 set the toplevel name to be the empty logical path\
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 62e5f0a324..cfa9bddc6e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -387,12 +387,13 @@ let err_unmapped_library loc qid =
        pr_dirpath dir ++ str".")
 
 let err_notfound_library loc qid =
-  msg_error
-    (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid ++ str"."))
+  user_err_loc
+    (loc,"locate_library",
+     strbrk "Unable to locate library " ++ pr_qualid qid ++ str".")
 
 let print_located_library r =
   let (loc,qid) = qualid_of_reference r in
-  try msg_found_library (Library.locate_qualified_library false qid)
+  try msg_found_library (Library.locate_qualified_library ~warn:false qid)
   with
     | Library.LibUnmappedDir -> err_unmapped_library loc qid
     | Library.LibNotFound -> err_notfound_library loc qid
@@ -750,12 +751,24 @@ let vernac_end_segment (_,id as lid) =
 (* Libraries *)
 
 let vernac_require from import qidl =
-  let qidl = match from with
-  | None -> qidl
-  | Some ns -> List.map (Libnames.join_reference ns) qidl
-  in
   let qidl = List.map qualid_of_reference qidl in
-  let modrefl = List.map Library.try_locate_qualified_library qidl in
+  let root = match from with
+  | None -> None
+  | Some from ->
+    let (_, qid) = Libnames.qualid_of_reference from in
+    let (hd, tl) = Libnames.repr_qualid qid in
+    Some (Libnames.add_dirpath_suffix hd tl)
+  in
+  let locate (loc, qid) =
+    try
+      let warn = Flags.is_verbose () in
+      let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in
+      (dir, f)
+    with
+      | Library.LibUnmappedDir -> err_unmapped_library loc qid
+      | Library.LibNotFound -> err_notfound_library loc qid
+  in
+  let modrefl = List.map locate qidl in
   if Dumpglob.dump () then
     List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
   Library.require_library_from_dirpath modrefl import
@@ -879,11 +892,10 @@ let vernac_set_used_variables e =
 let expand filename =
   Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename
 
-let vernac_add_loadpath isrec pdir ldiropt =
+let vernac_add_loadpath implicit pdir ldiropt =
   let pdir = expand pdir in
   let alias = Option.default Nameops.default_root_prefix ldiropt in
-  (if isrec then Mltop.add_rec_path else Mltop.add_path)
-    ~unix_path:pdir ~coq_root:alias ~implicit:true
+  Mltop.add_rec_path ~unix_path:pdir ~coq_root:alias ~implicit
 
 let vernac_remove_loadpath path =
   Loadpath.remove_load_path (expand path)