Declared ML Module are not uncapitalized/capitalized/uncapitalized/...

The exact filename has to be written. This is coherent with the RefMan.

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