1 files changed, 21 insertions, 22 deletions

diff --git a/library/loadpath.ml b/library/loadpath.ml
index 78f8dd25..d03c6c55 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -8,7 +8,7 @@
 
 open Pp
 open Util
-open Errors
+open CErrors
 open Names
 open Libnames
 
@@ -50,6 +50,13 @@ let remove_load_path dir =
   let filter p = not (String.equal p.path_physical dir) in
   load_paths := List.filter filter !load_paths
 
+let warn_overriding_logical_loadpath =
+  CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath"
+         (fun (phys_path, old_path, coq_path) ->
+          str phys_path ++ strbrk " was previously bound to " ++
+            pr_dirpath old_path ++ strbrk "; it is remapped to " ++
+            pr_dirpath coq_path)
+
 let add_load_path phys_path coq_path ~implicit =
   let phys_path = CUnix.canonical_path_name phys_path in
   let filter p = String.equal p.path_physical phys_path in
@@ -65,17 +72,12 @@ let add_load_path phys_path coq_path ~implicit =
     let replace =
       if DirPath.equal coq_path old_path then
         implicit <> old_implicit
-      else if DirPath.equal coq_path (Nameops.default_root_prefix)
-              && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then
-        false (* This is the default "-I ." path, don't override the old path *)
       else
         let () =
           (* Do not warn when overriding the default "-I ." path *)
           if not (DirPath.equal old_path Nameops.default_root_prefix) then
-            msg_warning
-              (str phys_path ++ strbrk " was previously bound to " ++
-                 pr_dirpath old_path ++ strbrk "; it is remapped to " ++
-                 pr_dirpath coq_path) in
+          warn_overriding_logical_loadpath (phys_path, old_path, coq_path)
+        in
         true in
     if replace then
       begin
@@ -84,10 +86,6 @@ let add_load_path phys_path coq_path ~implicit =
       end
   | _ -> anomaly_too_many_paths phys_path
 
-let extend_path_with_dirpath p dir =
-  List.fold_left Filename.concat p
-    (List.rev_map Id.to_string (DirPath.repr dir))
-
 let filter_path f =
   let rec aux = function
   | [] -> []
@@ -97,18 +95,19 @@ let filter_path f =
   in
   aux !load_paths
 
-let expand_path dir =
+let expand_path ?root dir =
   let rec aux = function
   | [] -> []
-  | { path_physical = ph; path_logical = lg; path_implicit = implicit }  :: l ->
-    match implicit with
-    | true ->
-      (** The path is implicit, so that we only want match the logical suffix *)
-      if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l
-    | false ->
-      (** Otherwise we must match exactly *)
-      if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
-  in
+  | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l ->
+    let success =
+      match root with
+      | None ->
+        if implicit then is_dirpath_suffix_of dir lg
+        else DirPath.equal dir lg
+      | Some root ->
+        is_dirpath_prefix_of root lg &&
+          is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in
+    if success then (ph, lg) :: aux l else aux l in
   aux !load_paths
 
 let locate_file fname =