From d692c5dc034778a1d97ace593c9a3658a44e698b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 7 Mar 2014 16:38:59 +0100 Subject: Fix lookup of native files when option -R is missing. Testcase: mkdir a echo "Definition t := O." > a/a.v coqc -R a a a/a.v echo "Require Import a.a. Definition u := t." > b.v coqc -I . b.v rm -rf a b.* --- library/loadpath.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'library/loadpath.ml') diff --git a/library/loadpath.ml b/library/loadpath.ml index 60799a8a7..7c203bc88 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -22,6 +22,9 @@ type t = { let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" +let accessible_paths = + Summary.ref ([] : CUnix.physical_path list) ~name:"ACCPATHS" + let logical p = p.path_logical let physical p = p.path_physical @@ -30,6 +33,8 @@ let get_load_paths () = !load_paths let get_paths () = List.map physical !load_paths +let get_accessible_paths () = !accessible_paths + let anomaly_too_many_paths path = anomaly (str "Several logical paths are associated to" ++ spc () ++ str path) @@ -63,6 +68,9 @@ let add_load_path phys_path isroot coq_path = match List.filter filter !load_paths with | [] -> load_paths := binding :: !load_paths; + if isroot then + accessible_paths := List.fold_left (fun acc v -> (fst v) :: acc) + (phys_path :: !accessible_paths) (System.all_subdirs phys_path) | [p] -> let dir = p.path_logical in if not (DirPath.equal coq_path dir) -- cgit v1.2.3