diff options
| author | notin | 2008-03-25 16:04:55 +0000 |
|---|---|---|
| committer | notin | 2008-03-25 16:04:55 +0000 |
| commit | 36780f223b50549f522ac2832eab127a9cc40615 (patch) | |
| tree | 435251a6edca3f617ad6733ecf58bf81dadd9dc7 /tools | |
| parent | 1e1d06303d476b1e7f171dc09ed1e18508e20436 (diff) | |
Correction d'un bug dans la gestion des 'Declare ML Module'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10717 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep.ml | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index ef4a933844..097e19fe28 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -238,9 +238,9 @@ let traite_fichier_Coq verbose f = addQueue deja_vu_ml str; try let mldir = Hashtbl.find mlKnown str in - printf " %s.cmo" (file_name ([str],mldir)) - with Not_found -> () - end) + printf " %s.cmo" (file_name ([String.uncapitalize str],mldir)) + with Not_found -> () + end) sl | Load str -> let str = Filename.basename str in @@ -306,7 +306,7 @@ let traite_Declare f = | s :: ll -> if (Hashtbl.mem mlKnown s) & not (List.mem s !decl_list) then begin let mldir = Hashtbl.find mlKnown s in - let fullname = file_name ([s],mldir) in + let fullname = file_name ([(String.uncapitalize s)],mldir) in let depl = mL_dep_list s (fullname ^ ".ml") in treat depl; decl_list := s :: !decl_list @@ -407,6 +407,11 @@ let usage () = flush stderr; exit 1 +let make_ml_module_name filename = + (* Computes a ML Module name from its physical name *) + let basename = Filename.chop_extension filename in + String.capitalize basename + let add_coqlib_known phys_dir log_dir f = if Filename.check_suffix f ".vo" then let basename = Filename.chop_suffix f ".vo" in @@ -415,15 +420,9 @@ let add_coqlib_known phys_dir log_dir f = Hashtbl.add coqlibKnown name () let add_known phys_dir log_dir f = - if Filename.check_suffix f ".ml" then - let basename = Filename.chop_suffix f ".ml" in - Hashtbl.add mlKnown basename (Some phys_dir) - else if Filename.check_suffix f ".ml4" then - let basename = Filename.chop_suffix f ".ml4" in - Hashtbl.add mlKnown basename (Some phys_dir) - else if Filename.check_suffix f ".mli" then - let basename = Filename.chop_suffix f ".mli" in - Hashtbl.add mliKnown basename (Some phys_dir) + if (Filename.check_suffix f ".ml" || Filename.check_suffix f ".mli" || Filename.check_suffix f ".ml4") then + let basename = make_ml_module_name f in + Hashtbl.add mlKnown basename (Some phys_dir) else if Filename.check_suffix f ".v" then let basename = Filename.chop_suffix f ".v" in let name = log_dir@[basename] in |