From 7c41bc9bdc883aacbc015954a89ff13fe9c9c1c0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 1 Apr 2015 10:51:32 +0200
Subject: From X Require Y looks for X with absolute path, disregarding -R.

---
 library/library.ml | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

(limited to 'library/library.ml')

diff --git a/library/library.ml b/library/library.ml
index 2ebf4e5c3..9d0ccb972 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -268,8 +268,9 @@ type library_location = LibLoaded | LibInPath
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
-  let loadpath = Loadpath.expand_root_path pref in
+  let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in
   let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
+  let loadpath = List.map fst loadpath in
   let find ext =
     try
       let name = Id.to_string base ^ ext in
@@ -286,10 +287,20 @@ let locate_absolute_library dir =
   | [vo;vi] -> dir, vo
   | _ -> assert false
 
-let locate_qualified_library warn qid =
+let locate_qualified_library ?root ?(warn = true) qid =
   (* Search library in loadpath *)
   let dir, base = repr_qualid qid in
-  let loadpath = Loadpath.expand_path dir in
+  let loadpath = match root with
+  | None -> Loadpath.expand_path dir
+  | Some root ->
+    let filter path =
+      if is_dirpath_prefix_of root path then
+        let path = drop_dirpath_prefix root path in
+        is_dirpath_suffix_of dir path
+      else false
+    in
+    Loadpath.filter_path filter
+  in
   let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
   let find ext =
     try
@@ -333,14 +344,6 @@ let try_locate_absolute_library dir =
     | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir)
     | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir)
 
-let try_locate_qualified_library (loc,qid) =
-  try
-    let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
-    dir,f
-  with
-    | LibUnmappedDir -> error_unmapped_dir qid
-    | LibNotFound -> error_lib_not_found qid
-
 (************************************************************************)
 (** {6 Tables of opaque proof terms} *)
 
-- 
cgit v1.2.3