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.ml        | 2 +-
 tools/coqdep_common.ml | 8 ++------
 tools/coqdep_lexer.mll | 2 +-
 3 files changed, 4 insertions(+), 8 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 578f473368..f083a59cfb 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 a952881c8c..1845351cde 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 f59d6a0f03..3bfea0c289 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
-- 
cgit v1.2.3