- configure: affiche si le natdynlink est positionne

- coq_makefile: utilise Coq_config pour avoir la liste des contribs
- mltop: normalisation des noms de modules ML (majuscule)
- Makefiles: introduction de fichiers %-mod.ml qui se chargent de faire
  les declarations de modules ML d'un plugin



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11987 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 3 deletions

diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index fc808f0b7..334b4d82a 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -235,9 +235,11 @@ type ml_module_object = { mnames : string list }
 let known_loaded_modules = ref Stringset.empty
 
 let add_known_module mname =
+  let mname = String.capitalize mname in
   known_loaded_modules := Stringset.add mname !known_loaded_modules
 
-let module_is_known mname = Stringset.mem mname !known_loaded_modules
+let module_is_known mname =
+  Stringset.mem (String.capitalize mname) !known_loaded_modules
 
 let load_object mname fname=
   dir_ml_load fname;
@@ -295,8 +297,8 @@ let cache_ml_module_object (_,{mnames=mnames}) =
 	     if_verbose msgnl (str" failed]");
 	     raise e
 	 else
-	   if_verbose
-	     msgnl (str"[Ignoring ML file " ++ str mname ++ str "]"))
+	     (if_verbose msgnl (str" failed]");
+	      error ("Dynamic link not supported (module "^name^")")))
     mnames
 
 let export_ml_module_object x = Some x