- 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

5 files changed, 20 insertions, 12 deletions

diff --git a/Makefile.build b/Makefile.build
index 96b72d5c17..3fce3ec903 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -909,6 +909,10 @@ endif
 	$(SHOW)'OCAMLYACC $<'
 	$(HIDE)$(OCAMLYACC) $<
 
+%-mod.ml: %.mllib
+	sed -e "s/\([^ ]\+\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
+	echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@
+
 %.ml4-preprocessed: %.ml4 | %.ml4.d
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \
@@ -970,6 +974,8 @@ checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC)
 	$(SHOW)'COQDEP  $<'
 	$(HIDE)$(COQDEPBOOT) -slash -boot -c "$<" > "$@" \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
+	echo "$*".cma: "$*"-mod.cmo >> "$@"
+	echo "$*".cmxa "$*".cmxs: "$*"-mod.cmx >> "$@"
 
 ## Veerry nasty hack to keep ocamldep happy
 %.ml: | %.ml4
diff --git a/Makefile.stage2 b/Makefile.stage2
index 8bee9ed3bc..56ca007931 100644
--- a/Makefile.stage2
+++ b/Makefile.stage2
@@ -10,7 +10,9 @@ include Makefile.stage1
 include Makefile.doc
 
 -include $(MLLIBFILES:.mllib=.mllib.d)
-.SECONDARY: $(MLLIBFILES:.mli=.mllib.d)
+.SECONDARY: $(MLLIBFILES:.mllib=.mllib.d)
+-include $(MLLIBFILES:%.mllib=%-mod.ml.d)
+.SECONDARY: $(MLLIBFILES:%.mllib=%-mod.ml.d)
 -include $(ML4FILES:.ml4=.ml4.ml.d)
 .SECONDARY: $(ML4FILES:.ml4=.ml4.ml.d)
 -include $(VFILES:.v=.v.d)
diff --git a/configure b/configure
index 827019eedc..de3c6fbbdc 100755
--- a/configure
+++ b/configure
@@ -842,6 +842,9 @@ echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
 echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
 echo "  Objective-Caml library in         : $CAMLLIB"
 echo "  Camlp4 library in                 : $CAMLP4LIB"
+if test "$best_compiler" = opt ; then
+echo "  Native dynamic link support       : $HASNATDYNLINK"
+fi
 if test "$COQIDE" != "no"; then
 echo "  Lablgtk2 library in               : $LABLGTKLIB"
 fi
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 7ee38e256c..24473c8261 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -318,14 +318,9 @@ let include_dirs (inc_i,inc_r) =
   -I $(COQLIB)/library -I $(COQLIB)/parsing \\
   -I $(COQLIB)/pretyping -I $(COQLIB)/interp \\
   -I $(COQLIB)/proofs -I $(COQLIB)/tactics \\
-  -I $(COQLIB)/toplevel -I $(COQLIB)/contrib/cc -I $(COQLIB)/contrib/dp \\
-  -I $(COQLIB)/contrib/extraction -I $(COQLIB)/contrib/field \\
-  -I $(COQLIB)/contrib/firstorder -I $(COQLIB)/contrib/fourier \\
-  -I $(COQLIB)/contrib/funind -I $(COQLIB)/contrib/interface \\
-  -I $(COQLIB)/contrib/micromega -I $(COQLIB)/contrib/omega \\
-  -I $(COQLIB)/contrib/ring -I $(COQLIB)/contrib/romega \\
-  -I $(COQLIB)/contrib/rtauto -I $(COQLIB)/contrib/setoid_ring \\
-  -I $(COQLIB)/contrib/subtac -I $(COQLIB)/contrib/xml\n";
+  -I $(COQLIB)/toplevel";
+    List.iter (fun c -> print " \\
+  -I $(COQLIB)/contrib/"; print c) Coq_config.contrib_dirs; print "\n";
     print "COQLIBS:="; print_list "\\\n  " str_i'; print " "; print_list "\\\n  " str_r; print "\n";
     print "COQDOCLIBS:=";   print_list "\\\n  " str_r; print "\n\n"
 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index fc808f0b7c..334b4d82a5 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