diff options
-rw-r--r-- | tools/coqdep.ml | 2 | ||||
-rw-r--r-- | tools/coqdep_common.ml | 8 | ||||
-rw-r--r-- | tools/coqdep_lexer.mll | 2 | ||||
-rw-r--r-- | toplevel/mltop.ml | 8 |
4 files changed, 5 insertions, 15 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 diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 09b604d1a..ca325bc62 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -188,13 +188,10 @@ let add_rec_path ~unix_path ~coq_root = (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = - let base = if Filename.check_suffix name ".cmo" then Filename.chop_suffix name ".cmo" else name - in - String.capitalize base let get_ml_object_suffix name = if Filename.check_suffix name ".cmo" then @@ -207,7 +204,6 @@ let get_ml_object_suffix name = None let file_of_name name = - let name = String.uncapitalize name in let suffix = get_ml_object_suffix name in let fail s = errorlabstrm "Mltop.load_object" @@ -248,18 +244,16 @@ let file_of_name name = let known_loaded_modules = ref String.Set.empty let add_known_module mname = - let mname = String.capitalize mname in known_loaded_modules := String.Set.add mname !known_loaded_modules let module_is_known mname = - String.Set.mem (String.capitalize mname) !known_loaded_modules + String.Set.mem mname !known_loaded_modules (** A plugin is just an ML module with an initialization function. *) let known_loaded_plugins = ref String.Map.empty let add_known_plugin init name = - let name = String.capitalize name in add_known_module name; known_loaded_plugins := String.Map.add name init !known_loaded_plugins |