From 2bfa94975ecc58d35637689ef2fd4473e8126c2e Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Mon, 13 Jan 2014 13:23:45 +0100 Subject: Declared ML Module are not uncapitalized/capitalized/uncapitalized/... The exact filename has to be written. This is coherent with the RefMan. --- tools/coqdep_common.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'tools/coqdep_common.ml') diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index a952881c8..1845351cd 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -100,8 +100,6 @@ let safe_hash_add clq q (k,v) = (** Files found in the loadpaths. For the ML files, the string is the basename without extension. - To allow ML source filename to be potentially capitalized, - we perform a double search. *) let mkknown () = @@ -109,10 +107,8 @@ let mkknown () = let add x s = if Hashtbl.mem h x then () else Hashtbl.add h x s and iter f = Hashtbl.iter f h and search x = - try Some (Hashtbl.find h (String.uncapitalize x)) - with Not_found -> - try Some (Hashtbl.find h (String.capitalize x)) - with Not_found -> None + try Some (Hashtbl.find h x) + with Not_found -> None in add, iter, search let add_ml_known, iter_ml_known, search_ml_known = mkknown () -- cgit v1.2.3