diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-03-07 16:38:59 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-03-07 16:38:59 +0100 |
commit | d692c5dc034778a1d97ace593c9a3658a44e698b (patch) | |
tree | 7b66e9e5056660511a7a3d73efa4eea2fda24eba /library/loadpath.ml | |
parent | b80cf566a39efe65f5ef0b1cc4ff9bb295a67fc7 (diff) |
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.*
Diffstat (limited to 'library/loadpath.ml')
-rw-r--r-- | library/loadpath.ml | 8 |
1 files changed, 8 insertions, 0 deletions
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) |