aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdep.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index ccce7cd311..a683aaae9f 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -199,7 +199,9 @@ let coqdep () =
add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
let user = coqlib//"user-contrib" in
- if Sys.file_exists user then add_rec_dir add_coqlib_known user []
+ if Sys.file_exists user then add_rec_dir add_coqlib_known user [];
+ let coqpath = Envars.coqpath () in
+ List.iter (fun s -> add_rec_dir add_coqlib_known s []) coqpath;
end;
List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;