From 229dd629d2425750ec4e4ea5598804745979b6d2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Jan 2015 20:10:31 +0100 Subject: Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep. --- tools/coqdep_common.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'tools/coqdep_common.ml') diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 10150497d..fa6a0daeb 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -103,20 +103,21 @@ let safe_hash_add cmp clq q (k,v) = For the ML files, the string is the basename without extension. *) -let warning_ml_clash x s s' suff = +let warning_ml_clash x s suff s' suff' = + if suff = suff' then eprintf "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff (match s with None -> "." | Some d -> d) ((match s' with None -> "." | Some d -> d) // x) suff let mkknown () = - let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in + let h = (Hashtbl.create 19 : (string, dir * string) Hashtbl.t) in let add x s suff = - try let s' = Hashtbl.find h x in warning_ml_clash x s' s suff - with Not_found -> Hashtbl.add h x s - and iter f = Hashtbl.iter f h + try let s',suff' = Hashtbl.find h x in warning_ml_clash x s' suff' s suff + with Not_found -> Hashtbl.add h x (s,suff) + and iter f = Hashtbl.iter (fun x (s,_) -> f x s) h and search x = - try Some (Hashtbl.find h x) + try Some (fst (Hashtbl.find h x)) with Not_found -> None in add, iter, search @@ -442,7 +443,7 @@ let add_caml_known phys_dir _ f = let basename,suff = get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in match suff with - | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".ml"|".ml4" -> add_ml_known f (Some phys_dir) suff | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff -- cgit v1.2.3