From 10f0deda5c452b586d50419f269c3952a466db16 Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 17 Mar 2009 20:05:36 +0000 Subject: - 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 --- toplevel/mltop.ml4 | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'toplevel/mltop.ml4') 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 -- cgit v1.2.3