diff options
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 9bc8965d..3093fa6c 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: coqdep.ml 13983 2011-04-08 17:57:56Z herbelin $ *) open Printf open Coqdep_lexer @@ -41,8 +41,8 @@ let add_coqlib_known phys_dir log_dir f = match get_extension f [".vo"] with | (basename,".vo") -> let name = log_dir@[basename] in - Hashtbl.add coqlibKnown [basename] (); - Hashtbl.add coqlibKnown name () + let paths = suffixes name in + List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () let sort () = @@ -199,7 +199,8 @@ let coqdep () = let coqlib = Envars.coqlib () in add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; - add_dir add_coqlib_known (coqlib//"user-contrib") [] + let user = coqlib//"user-contrib" in + if Sys.file_exists user then add_rec_dir add_coqlib_known user [] end; List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; |