diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-01-13 13:23:45 +0100 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-01-13 15:21:44 +0100 |
| commit | 2bfa94975ecc58d35637689ef2fd4473e8126c2e (patch) | |
| tree | d9b6544a5b068fbb60812e5d643e6bdc52620b6d /tools | |
| parent | e20e73300be869696264f8269c47c0ff92316c26 (diff) | |
Declared ML Module are not uncapitalized/capitalized/uncapitalized/...
The exact filename has to be written. This is coherent with the RefMan.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep.ml | 2 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 8 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mll | 2 |
3 files changed, 4 insertions, 8 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 578f47336..f083a59cf 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -121,7 +121,7 @@ let traite_Declare f = let s' = basename_noext s in (match search_ml_known s with | Some mldir when not (List.mem s' !decl_list) -> - let fullname = file_name (String.uncapitalize s') mldir in + let fullname = file_name s' mldir in let depl = mL_dep_list s (fullname ^ ".ml") in treat depl; decl_list := s :: !decl_list 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 () diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index f59d6a0f0..3bfea0c28 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -18,7 +18,7 @@ type coq_token = | Require of qualid list | RequireString of string - | Declare of string list (* Names are assumed to be uncapitalized *) + | Declare of string list | Load of string | AddLoadPath of string | AddRecLoadPath of string * qualid |