Take advantage of natdynlink when available: almost all contribs become loadable plugins

- Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode).
- Features that were available without any Require are now loaded systematically
  when launching coqtop (see Coqtop.load_initial_plugins):
     extraction, jprover, cc, ground, dp, recdef, xml
- The other plugins are loaded when a corresponding Require is done:
     quote, ring, field, setoid_ring, omega, romega, micromega, fourier
- I experienced a crash (segfault) while turning subtac into a plugin, so this
  one stays statically linked into coqtop for now
- When the ocaml version doesn't support natdynlink, or if "-natdynlink no"
  is explicitely given to configure, coqtop is statically linked with all of
  the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear.
- How should coqdep handle a "Declare ML Module "foo"" if foo is an archive
  and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the
  same location as the .v during the build, but can be moved later in any place of
  the ml loadpath.

This is clearly an experimentation. Feedback most welcome...

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

26 files changed, 225 insertions, 131 deletions

diff --git a/Makefile b/Makefile
index c8b885902c..0eaf689dd8 100644
--- a/Makefile
+++ b/Makefile
@@ -118,7 +118,7 @@ else
 stage1 $(STAGE1_TARGETS): always
 	$(call stage-template,1)
 
-CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.dep.ps %.dot
+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
 ifdef CM_STAGE1
 $(CAML_OBJECT_PATTERNS): always
 	$(call stage-template,1)
@@ -189,7 +189,7 @@ archclean: clean-ide cleantheories
 	rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN)
 	rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT)
 	rm -f bin/coq-parser.opt$(EXE) bin/coq-interface.opt$(EXE)
-	find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' -or -name '*.so' | xargs rm -f
+	find . -name '*.cmx' -or -name '*.cmxs' -or -name '*.cmxa' -or -name '*.[soa]' -or -name '*.so' | xargs rm -f
 	rm -f $(TOOLS) $(CSDPCERT)
 
 clean-ide:
diff --git a/Makefile.build b/Makefile.build
index bba84709bd..61d4944835 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -67,6 +67,7 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
               -I proofs -I tactics -I pretyping \
               -I interp -I toplevel -I parsing -I ide/utils -I ide \
               -I contrib/omega -I contrib/romega -I contrib/micromega \
+              -I contrib/quote \
 	      -I contrib/ring -I contrib/dp -I contrib/setoid_ring \
               -I contrib/xml -I contrib/extraction \
               -I contrib/interface -I contrib/fourier \
@@ -168,12 +169,14 @@ coqbinaries:: ${COQBINARIES} ${CSDPCERT}
 
 coq: coqlib tools coqbinaries
 
-coqlib:: theories contrib
+coqlib:: initplugins theories contrib
 
-coqlight: theories-light tools coqbinaries
+coqlight: initplugins theories-light tools coqbinaries
 
 states:: states/initial.coq
 
+initplugins: $(INITPLUGINSOPT) $(INITPLUGINS)
+
 $(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'	
 	$(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@
@@ -193,12 +196,12 @@ CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
 
 $(CHICKENOPT): checker/check.cmxa checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ unix.cmxa gramlib.cmxa checker/check.cmxa checker/main.ml
+	$(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ unix.cmxa gramlib.cmxa $^
 	$(STRIP) $@
 
 $(CHICKENBYTE): checker/check.cma checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml
+	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma $^
 
 $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
 	cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
@@ -207,13 +210,11 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
 
 $(COQMKTOPBYTE): $(COQMKTOPCMO)
 	$(SHOW)'OCAMLC -o $@'	
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma \
-          $(COQMKTOPCMO) $(OSDEPLIBS)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $^ $(OSDEPLIBS)
 
 $(COQMKTOPOPT): $(COQMKTOPCMX)
 	$(SHOW)'OCAMLOPT -o $@'	
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa \
-          $(COQMKTOPCMX) $(OSDEPLIBS)
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa $^ $(OSDEPLIBS)
 	$(STRIP) $@
 
 $(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP)
@@ -258,108 +259,109 @@ hightactics: $(HIGHTACTICS)
 # target for libraries
 
 lib/lib.cma: $(LIBREP)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBREP)
-
 lib/lib.cmxa: $(LIBREP:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(LIBREP:.cmo=.cmx)
 
 kernel/kernel.cma: $(KERNEL)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(KERNEL)
-
 kernel/kernel.cmxa: $(KERNEL:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(KERNEL:.cmo=.cmx)
-
-checker/check.cma: $(MCHECKER)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -a -o $@ $(MCHECKER)
-
-checker/check.cmxa: $(MCHECKER:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx)
 
 library/library.cma: $(LIBRARY)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBRARY)
-
 library/library.cmxa: $(LIBRARY:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(LIBRARY:.cmo=.cmx)
 
 pretyping/pretyping.cma: $(PRETYPING)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PRETYPING)
-
 pretyping/pretyping.cmxa: $(PRETYPING:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PRETYPING:.cmo=.cmx)
 
 interp/interp.cma: $(INTERP)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(INTERP)
-
 interp/interp.cmxa: $(INTERP:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(INTERP:.cmo=.cmx)
 
 parsing/parsing.cma: $(PARSING)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PARSING)
-
 parsing/parsing.cmxa: $(PARSING:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PARSING:.cmo=.cmx)
 
 proofs/proofs.cma: $(PROOFS)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PROOFS)
-
 proofs/proofs.cmxa: $(PROOFS:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PROOFS:.cmo=.cmx)
 
 tactics/tactics.cma: $(TACTICS)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(TACTICS)
-
 tactics/tactics.cmxa: $(TACTICS:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(TACTICS:.cmo=.cmx)
 
 toplevel/toplevel.cma: $(TOPLEVEL)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(TOPLEVEL)
-
 toplevel/toplevel.cmxa: $(TOPLEVEL:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(TOPLEVEL:.cmo=.cmx)
 
 parsing/highparsing.cma: $(HIGHPARSING)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHPARSING)
-
 parsing/highparsing.cmxa: $(HIGHPARSING:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHPARSING:.cmo=.cmx)
 
 tactics/hightactics.cma: $(HIGHTACTICS)
+tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx)
+
+contrib/contrib.cma: $(CONTRIBSTATIC)
+contrib/contrib.cmxa: $(CONTRIBSTATIC:.cmo=.cmx)
+
+$(OMEGACMA): $(OMEGACMO)
+$(OMEGACMA:.cma=.cmxa): $(OMEGACMO:.cmo=.cmx)
+
+$(ROMEGACMA): $(ROMEGACMO)
+$(ROMEGACMA:.cma=.cmxa): $(ROMEGACMO:.cmo=.cmx)
+
+$(MICROMEGACMA): $(MICROMEGACMO)
+$(MICROMEGACMA:.cma=.cmxa): $(MICROMEGACMO:.cmo=.cmx)
+
+$(QUOTACMA): $(QUOTECMO)
+$(QUOTECMA:.cma=.cmxa): $(QUOTECMO:.cmo=.cmx)
+
+$(RINGCMA): $(RINGCMO)
+$(RINGCMA:.cma=.cmxa): $(RINGCMO:.cmo=.cmx)
+
+$(NEWRINGCMA): $(NEWRINGCMO)
+$(NEWRINGCMA:.cma=.cmxa): $(NEWRINGCMO:.cmo=.cmx)
+
+$(FIELDCMA): $(FIELDCMO)
+$(FIELDCMA:.cma=.cmxa): $(FIELDCMO:.cmo=.cmx)
+
+$(XMLCMA): $(XMLCMO)
+$(XMLCMA:.cma=.cmxa): $(XMLCMO:.cmo=.cmx)
+
+$(FOURIERCMA): $(FOURIERCMO)
+$(FOURIERCMA:.cma=.cmxa): $(FOURIERCMO:.cmo=.cmx)
+
+$(EXTRACTIONCMA): $(EXTRACTIONCMO)
+$(EXTRACTIONCMA:.cma=.cmxa): $(EXTRACTIONCMO:.cmo=.cmx)
+
+$(RTAUTOCMA): $(RTAUTOCMO)
+$(RTAUTOCMA:.cma=.cmxa): $(RTAUTOCMO:.cmo=.cmx)
+
+$(JPROVERCMA): $(JPROVERCMO)
+$(JPROVERCMA:.cma=.cmxa): $(JPROVERCMO:.cmo=.cmx)
+
+$(FOCMA): $(FOCMO)
+$(FOCMA:.cma=.cmxa): $(FOCMO:.cmo=.cmx)
+
+$(CCCMA): $(CCCMO)
+$(CCCMA:.cma=.cmxa): $(CCCMO:.cmo=.cmx)
+
+$(DPCMA): $(DPCMO)
+$(DPCMA:.cma=.cmxa): $(DPCMO:.cmo=.cmx)
+
+$(FUNINDCMA): $(FUNINDCMO)
+$(FUNINDCMA:.cma=.cmxa): $(FUNINDCMO:.cmo=.cmx)
+
+$(SUBTACCMA): $(SUBTACCMO)
+$(SUBTACCMA:.cma=.cmxa): $(SUBTACCMO:.cmo=.cmx)
+
+%.cma:
 	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHTACTICS)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^
 
-tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx)
+%.cmxa:
 	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHTACTICS:.cmo=.cmx)
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^
 
-contrib/contrib.cma: $(CONTRIB)
+# For the checker, different flags may be used
+
+checker/check.cma: $(MCHECKER)
 	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(CONTRIB)
+	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -a -o $@ $^
 
-contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx)
+checker/check.cmxa: $(MCHECKER:.cmo=.cmx)
 	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(CONTRIB:.cmo=.cmx)
+	$(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -a -o $@ $^
 
 ###########################################################################
 # Csdp to micromega special targets
@@ -368,12 +370,12 @@ contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx)
 ifeq ($(BEST),opt)
 contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMX)
 	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $(CSDPCERTCMX)
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $^
 	$(STRIP) $@
 else
 contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $^
 endif
 
 ###########################################################################
@@ -421,11 +423,11 @@ ide/%.cmx: ide/%.ml | ide/%.ml.d
 
 ide/ide.cma: $(COQIDECMO)
 	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(COQIDECMO)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^
 
 ide/ide.cmxa: $(COQIDECMO:.cmo=.cmx)
 	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(COQIDECMO:.cmo=.cmx)
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^
 
 # install targets
 
@@ -551,7 +553,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
 # contribs (interface not included)
 ###########################################################################
 
-contrib: $(CONTRIBVO) $(CONTRIBCMO)
+contrib: $(CONTRIBVO)
 omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
 micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
 ring: $(RINGVO) $(RINGCMO)
@@ -575,7 +577,7 @@ states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/M
 	$(SHOW)'BUILD     $@'
 	$(HIDE)$(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
 
-theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY)
+theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY)
 	$(SHOW)'COQC -nois $<'
 	$(HIDE)rm -f theories/Init/$*.glob
 	$(HIDE)$(BOOTCOQTOP) -nois -compile theories/Init/$*
@@ -593,27 +595,27 @@ tools:: $(TOOLS) $(DEBUGPRINTERS)
 
 $(COQDEP): $(COQDEPCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $^ $(OSDEPLIBS)
 
 $(GALLINA): $(GALLINACMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $^
 
-$(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo
+$(COQMAKEFILE): config/coq_config.cmo tools/coq_makefile.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma $^
 
 $(COQTEX): tools/coq-tex.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma $^
 
 $(COQWC): tools/coqwc.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $^
 
 $(COQDOC): $(COQDOCCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $^
 
 ###########################################################################
 # Installation
@@ -730,7 +732,7 @@ dev/printers.cma: $(PRINTERSCMO)
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) gramlib.cma $(PRINTERSCMO) -o test-printer
 	@rm -f test-printer
 	$(SHOW)'OCAMLC -a $@'   
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(PRINTERSCMO) -linkall -a -o $@
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
 
 parsing/grammar.cma: $(GRAMMARCMO)
 	$(SHOW)'Testing $@'
diff --git a/Makefile.common b/Makefile.common
index 4ca7e2e45b..63740d086a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -234,33 +234,42 @@ HIGHTACTICS:=\
   tactics/extratactics.cmo tactics/eauto.cmo tactics/class_tactics.cmo \
   tactics/tauto.cmo tactics/eqdecide.cmo
 
+OMEGACMA:=contrib/omega/omega_plugin.cma
 OMEGACMO:=\
   contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
   contrib/omega/g_omega.cmo 
 
+ROMEGACMA:=contrib/romega/romega_plugin.cma
 ROMEGACMO:=\
   contrib/romega/const_omega.cmo \
   contrib/romega/refl_omega.cmo contrib/romega/g_romega.cmo
 
+MICROMEGACMA:=contrib/micromega/micromega_plugin.cma
 MICROMEGACMO:=\
   contrib/micromega/mutils.cmo  \
   contrib/micromega/micromega.cmo contrib/micromega/mfourier.cmo \
   contrib/micromega/certificate.cmo \
   contrib/micromega/coq_micromega.cmo contrib/micromega/g_micromega.cmo
 
+QUOTECMA:=contrib/quote/quote_plugin.cma
+QUOTECMO:=\
+  contrib/quote/quote.cmo contrib/quote/g_quote.cmo
+
+RINGCMA:=contrib/ring/ring_plugin.cma
 RINGCMO:=\
-  contrib/ring/quote.cmo contrib/ring/g_quote.cmo \
   contrib/ring/ring.cmo contrib/ring/g_ring.cmo 
 
-NEWRINGCMO:=\
-  contrib/setoid_ring/newring.cmo
+NEWRINGCMA:=contrib/setoid_ring/newring_plugin.cma
+NEWRINGCMO:=contrib/setoid_ring/newring.cmo
 
+DPCMA:=contrib/dp/dp_plugin.cma
 DPCMO:=contrib/dp/dp_why.cmo contrib/dp/dp_zenon.cmo \
       contrib/dp/dp.cmo contrib/dp/dp_gappa.cmo contrib/dp/g_dp.cmo
 
-FIELDCMO:=\
-  contrib/field/field.cmo 
+FIELDCMO:=contrib/field/field.cmo
+FIELDCMA:=contrib/field/field_plugin.cma
 
+XMLCMA:=contrib/xml/xml_plugin.cma
 XMLCMO:=\
   contrib/xml/unshare.cmo contrib/xml/xml.cmo contrib/xml/acic.cmo \
   contrib/xml/doubleTypeInference.cmo \
@@ -270,10 +279,12 @@ XMLCMO:=\
   contrib/xml/xmlentries.cmo 	contrib/xml/cic2Xml.cmo \
   contrib/xml/dumptree.cmo
 
+FOURIERCMA:=contrib/fourier/fourier_plugin.cma
 FOURIERCMO:=\
   contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo \
   contrib/fourier/g_fourier.cmo
 
+EXTRACTIONCMA:=contrib/extraction/extraction_plugin.cma
 EXTRACTIONCMO:=\
   contrib/extraction/table.cmo\
   contrib/extraction/mlutil.cmo\
@@ -286,12 +297,14 @@ EXTRACTIONCMO:=\
   contrib/extraction/extract_env.cmo \
   contrib/extraction/g_extraction.cmo
 
+JPROVERCMA:=contrib/jprover/jprover_plugin.cma
 JPROVERCMO:=\
   contrib/jprover/opname.cmo \
   contrib/jprover/jterm.cmo contrib/jprover/jlogic.cmo \
   contrib/jprover/jtunify.cmo contrib/jprover/jall.cmo \
   contrib/jprover/jprover.cmo
 
+FUNINDCMA:=contrib/funind/recdef_plugin.cma
 FUNINDCMO:=\
   contrib/funind/indfun_common.cmo contrib/funind/rawtermops.cmo \
   contrib/funind/recdef.cmo \
@@ -301,15 +314,18 @@ FUNINDCMO:=\
   contrib/funind/invfun.cmo contrib/funind/indfun.cmo \
   contrib/funind/merge.cmo contrib/funind/g_indfun.cmo
 
+FOCMA:=contrib/firstorder/ground_plugin.cma
 FOCMO:=\
   contrib/firstorder/formula.cmo contrib/firstorder/unify.cmo \
   contrib/firstorder/sequent.cmo contrib/firstorder/rules.cmo \
   contrib/firstorder/instances.cmo contrib/firstorder/ground.cmo \
   contrib/firstorder/g_ground.cmo
 
+CCCMA:=contrib/cc/cc_plugin.cma
 CCCMO:=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \
   contrib/cc/g_congruence.cmo 
 
+SUBTACCMA:=contrib/subtac/subtac_plugin.cma
 SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \
   contrib/subtac/g_eterm.cmo \
   contrib/subtac/subtac_errors.cmo contrib/subtac/subtac_coercion.cmo \
@@ -319,14 +335,28 @@ SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \
   contrib/subtac/subtac.cmo contrib/subtac/g_subtac.cmo \
   contrib/subtac/equations.cmo
 
+RTAUTOCMA:=contrib/rtauto/rtauto_plugin.cma
 RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
 	contrib/rtauto/g_rtauto.cmo
 
-CONTRIB:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
-        $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \
-	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
-	$(CCCMO)  $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \
-	$(FUNINDCMO)
+CONTRIBSTATIC:=\
+	$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
+        $(QUOTECMO) $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \
+        $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
+        $(CCCMO)  $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \
+        $(FUNINDCMO)
+
+ifeq ($(HASNATDYNLINK),true)
+ CONTRIBSTATIC:=$(SUBTACCMO)
+ INITPLUGINS:=$(EXTRACTIONCMA) $(JPROVERCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
+	$(XMLCMA) $(FUNINDCMA) #$(SUBTACCMA)
+ INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
+ ifeq ($(BEST),opt)
+  INITPLUGINSBEST:=$(INITPLUGINSOPT)
+ else
+  INITPLUGINSBEST:=$(INITPLUGINS)
+ endif
+endif
 
 CMA:=$(CLIBS) $(CAMLP4OBJS)
 CMXA:=$(CMA:.cma=.cmxa)
@@ -346,7 +376,7 @@ LINKCMX:=$(LINKCMOCMXA:.cmo=.cmx)
 # objects known by the toplevel of Coq
 OBJSCMO:=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \
         $(PROOFS) $(PARSING) $(TACTICS) $(TOPLEVEL) $(HIGHPARSING) \
-        $(HIGHTACTICS) $(CONTRIB)
+        $(HIGHTACTICS) $(CONTRIBSTATIC)
 
 COQIDECMO:=ide/utils/okey.cmo ide/utils/config_file.cmo \
 	  ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \
@@ -753,7 +783,7 @@ THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO)
 ## Contribs
 
 OMEGAVO:=$(addprefix contrib/omega/, \
- PreOmega.vo	OmegaLemmas.vo 	Omega.vo )
+ PreOmega.vo	OmegaLemmas.vo 	OmegaPlugin.vo Omega.vo )
 
 ROMEGAVO:=$(addprefix contrib/romega/, \
  ReflOmegaCore.vo 	ROmega.vo )
@@ -767,12 +797,15 @@ MICROMEGAVO:=$(addprefix contrib/micromega/, \
   QMicromega.vo         RMicromega.vo \
   Tauto.vo )
 
+QUOTEVO:=$(addprefix contrib/quote/, \
+ Quote.vo )
+
 RINGVO:=$(addprefix contrib/ring/, \
  LegacyArithRing.vo	Ring_normalize.vo \
  LegacyRing_theory.vo	LegacyRing.vo \
  LegacyNArithRing.vo    \
  LegacyZArithRing.vo	Ring_abstract.vo \
- Quote.vo		Setoid_ring_normalize.vo \
+ Setoid_ring_normalize.vo \
  Setoid_ring.vo		Setoid_ring_theory.vo )
 
 FIELDVO:=$(addprefix contrib/field/, \
@@ -811,7 +844,7 @@ RTAUTOVO:=$(addprefix contrib/rtauto/, \
 
 CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
 	    $(XMLVO) $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) \
-	    $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO)
+	    $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO)
 
 ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
 VFILES:= $(ALLVO:.vo=.v)
diff --git a/configure b/configure
index a64f561481..b9e6f9ea8f 100755
--- a/configure
+++ b/configure
@@ -59,6 +59,8 @@ usage () {
     printf "\tSpecifies the architecture\n"
     echo "-opt"
     printf "\tSpecifies whether or not to generate optimized executables\n"
+    echo "-natdynlink (yes|no)"
+    printf "\tSpecifies whether or not to use dynamic loading of native code\n"
     echo "-fsets (all|basic)"
     echo "-reals (all|basic)"
     printf "\tSpecifies whether or not to compile full FSets/Reals library\n"
@@ -104,6 +106,7 @@ coq_profile_flag=
 coq_annotate_flag=
 best_compiler=opt
 cflags="-fno-defer-pop -Wall -Wno-unused"
+natdynlink=yes
 
 gcc_exec=gcc
 ar_exec=ar
@@ -186,6 +189,11 @@ while : ; do
     -opt|--opt) bytecamlc=ocamlc.opt
                 camlp4oexec=camlp4o  # can't add .opt since dyn load'll be required
                 nativecamlc=ocamlopt.opt;;
+    -natdynlink|--natdynlink) case "$2" in
+	                  yes) natdynlink=yes;;
+                          *) natdynlink=no
+                        esac
+                        shift;;
     -fsets|--fsets) case "$2" in
 			yes|all) fsets=all;;
 			*) fsets=basic
@@ -212,7 +220,7 @@ while : ; do
 		      esac
 		      shift;;
     -with-geoproof|--with-geoproof) 
-	  case $2 in
+	  case "$2" in
 	      yes) with_geoproof=true;;
 	      no) with_geoproof=false;;
 	  esac
@@ -442,7 +450,7 @@ if [ "$coq_debug_flag" = "-g" ]; then
 fi
 
 # Native dynlink
-if test -f `"$CAMLC" -where`/dynlink.cmxa; then
+if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then
     HASNATDYNLINK=true
 else
     HASNATDYNLINK=false
diff --git a/contrib/field/LegacyField.v b/contrib/field/LegacyField.v
index ee1ddd477b..efa53b4e9d 100644
--- a/contrib/field/LegacyField.v
+++ b/contrib/field/LegacyField.v
@@ -11,5 +11,6 @@
 Require Export LegacyField_Compl.
 Require Export LegacyField_Theory.
 Require Export LegacyField_Tactic.
+Declare ML Module "field_plugin".
 
 (* Command declarations are moved to the ML side *)
diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v
index ac1592beea..07b2973a4a 100644
--- a/contrib/fourier/Fourier.v
+++ b/contrib/fourier/Fourier.v
@@ -10,15 +10,11 @@
 
 (* "Fourier's method to solve linear inequations/equations systems.".*)
 
-Declare ML Module "quote".
-Declare ML Module "ring".
-Declare ML Module "fourier".
-Declare ML Module "fourierR".
-Declare ML Module "field".
-
-Require Export Fourier_util.
+Require Export LegacyRing.
 Require Export LegacyField.
 Require Export DiscrR.
+Require Export Fourier_util.
+Declare ML Module "fourier_plugin".
 
 Ltac fourier := abstract (fourierz; field; discrR).
 
diff --git a/contrib/micromega/Psatz.v b/contrib/micromega/Psatz.v
index b2dd99100c..a3be562077 100644
--- a/contrib/micromega/Psatz.v
+++ b/contrib/micromega/Psatz.v
@@ -22,6 +22,7 @@ Require Import Raxioms.
 Require Export RingMicromega.
 Require Import VarMap.
 Require Tauto.
+Declare ML Module "micromega_plugin".
 
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v
index c054f218aa..f02209459f 100644
--- a/contrib/micromega/QMicromega.v
+++ b/contrib/micromega/QMicromega.v
@@ -17,6 +17,7 @@ Require Import RingMicromega.
 Require Import Refl.
 Require Import QArith.
 Require Import Qfield.
+Declare ML Module "micromega_plugin".
 
 Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq  Qle Qlt.
 Proof.
diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v
index 7c6969c2f2..70786a0571 100644
--- a/contrib/micromega/RMicromega.v
+++ b/contrib/micromega/RMicromega.v
@@ -17,6 +17,7 @@ Require Import RingMicromega.
 Require Import Refl.
 Require Import Raxioms RIneq Rpow_def DiscrR.
 Require Setoid.
+Declare ML Module "micromega_plugin".
 
 Definition Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R).
 Proof.
diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v
index 0855925a3d..1da3228a98 100644
--- a/contrib/micromega/ZMicromega.v
+++ b/contrib/micromega/ZMicromega.v
@@ -19,6 +19,7 @@ Require Import Refl.
 Require Import ZArith.
 Require Import List.
 Require Import Bool.
+Declare ML Module "micromega_plugin".
 
 Ltac flatten_bool :=
   repeat match goal with
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 3b427162e8..30b9457183 100644
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -19,6 +19,7 @@
 Require Export ZArith_base.
 Require Export OmegaLemmas.
 Require Export PreOmega.
+Declare ML Module "omega_plugin".
 
 Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
   Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
diff --git a/contrib/omega/OmegaPlugin.v b/contrib/omega/OmegaPlugin.v
new file mode 100644
index 0000000000..21535f0d3b
--- /dev/null
+++ b/contrib/omega/OmegaPlugin.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+Declare ML Module "omega_plugin".
diff --git a/contrib/ring/Quote.v b/contrib/quote/Quote.v
index 9a11a70b9c..f21a678e1a 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/quote/Quote.v
@@ -8,6 +8,8 @@
 
 (* $Id$ *)
 
+Declare ML Module "quote_plugin".
+
 (***********************************************************************
   The "abstract" type index is defined to represent variables.
 
diff --git a/contrib/ring/g_quote.ml4 b/contrib/quote/g_quote.ml4
index 808cbbf274..808cbbf274 100644
--- a/contrib/ring/g_quote.ml4
+++ b/contrib/quote/g_quote.ml4
diff --git a/contrib/ring/quote.ml b/contrib/quote/quote.ml
index 3b13283e13..9141dc2f52 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/quote/quote.ml
@@ -119,7 +119,7 @@ open Tacexpr
   We do that lazily, because this code can be linked before
   the constants are loaded in the environment *)
 
-let constant dir s = Coqlib.gen_constant "Quote" ("ring"::dir) s
+let constant dir s = Coqlib.gen_constant "Quote" ("quote"::dir) s
 
 let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
 let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
@@ -388,7 +388,7 @@ let rec sort_subterm gl l =
   [gl: goal sigma]\\ *)
 
 let quote_terms ivs lc gl =
-  Coqlib.check_required_library ["Coq";"ring";"Quote"];
+  Coqlib.check_required_library ["Coq";"quote";"Quote"];
   let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v
index ed1da9c56e..4ae85baf37 100644
--- a/contrib/ring/LegacyRing.v
+++ b/contrib/ring/LegacyRing.v
@@ -13,6 +13,7 @@ Require Export LegacyRing_theory.
 Require Export Quote.
 Require Export Ring_normalize.
 Require Export Ring_abstract.
+Declare ML Module "ring_plugin".
 
 (* As an example, we provide an instantation for bool. *)
 (* Other instatiations are given in ArithRing and ZArithRing in the
diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v
index b5cd6b1d0c..93b9bc7cf5 100644
--- a/contrib/ring/Setoid_ring.v
+++ b/contrib/ring/Setoid_ring.v
@@ -10,4 +10,5 @@
 
 Require Export Setoid_ring_theory.
 Require Export Quote.
-Require Export Setoid_ring_normalize.
\ No newline at end of file
+Require Export Setoid_ring_normalize.
+Declare ML Module "ring_plugin".
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 92f74d1d94..bb6aaea7de 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -752,7 +752,7 @@ let constants_to_unfold =
       "Coq.ring.Ring_normalize.interp_vl";
       "Coq.ring.Ring_abstract.interp_acs";
       "Coq.ring.Ring_abstract.interp_sacs";
-      "Coq.ring.Quote.varmap_find";
+      "Coq.quote.Quote.varmap_find";
       (* anciennement des Local devenus Definition *)
       "Coq.ring.Ring_normalize.ics_aux";
       "Coq.ring.Ring_normalize.ivl_aux";
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index 4281cc5736..3ddb6bed12 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -10,3 +10,5 @@ Require Import ReflOmegaCore.
 Require Export Setoid.
 Require Export PreOmega.
 Require Export ZArith_base.
+Require Import OmegaPlugin.
+Declare ML Module "romega_plugin".
\ No newline at end of file
diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v
index 342c03dbac..4b95097e2f 100644
--- a/contrib/rtauto/Rtauto.v
+++ b/contrib/rtauto/Rtauto.v
@@ -14,6 +14,8 @@ Require Export Bintree.
 Require Import Bool.
 Unset Boxed Definitions.
 
+Declare ML Module "rtauto_plugin".
+
 Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
 Ltac clean:=try (simpl;congruence).
 
diff --git a/contrib/setoid_ring/Ring_base.v b/contrib/setoid_ring/Ring_base.v
index 95b037e3b6..fd9dd8d0d3 100644
--- a/contrib/setoid_ring/Ring_base.v
+++ b/contrib/setoid_ring/Ring_base.v
@@ -10,7 +10,8 @@
    ring tactic. Abstract rings need more theory, depending on
    ZArith_base. *)
 
-Declare ML Module "newring".
+Require Import Quote.
+Declare ML Module "newring_plugin".
 Require Export Ring_theory.
 Require Export Ring_tac.
 Require Import InitialRing.
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 46d106d37a..2ff3322380 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -4,7 +4,8 @@ Require Import BinPos.
 Require Import Ring_polynom.
 Require Import BinList.
 Require Import InitialRing.
-Declare ML Module "newring".
+Require Import Quote.
+Declare ML Module "newring_plugin".
   
 
 (* adds a definition id' on the normal form of t and an hypothesis id
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index 8aadf8f5dd..e535a55683 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -177,7 +177,7 @@ assert (Z:  Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)).
   split;
    intros H;
    simpl; unfold g;
-   destruct (eq_nat_dec 0 n); try reflexivity.
+   destruct (eq_nat_dec 0 n) as [t|f]; try reflexivity.
    elim f; auto with *.
   elimtype False; omega.
  destruct IHa as [IHa0 IHa1].
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 529ca0ba54..3d93c8a908 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -246,11 +246,22 @@ let traite_fichier_Coq verbose f =
                	       try
               		 let mldir = Hashtbl.find mlKnown s in
 			 let filename = file_name ([String.uncapitalize s],mldir) in
-              		 if Coq_config.has_natdynlink then
+			 if Coq_config.has_natdynlink then
 			   printf " %s.cmo %s.cmxs" filename filename
 			 else
 			   printf " %s.cmo" filename
-              	       with Not_found -> ()
+		       with Not_found ->
+			 (** The .cmxs we want to load dynamically may come
+			     from a .cmxa, that has no corresponding .ml file.
+			     Idem with bytecode .cma. What dependency should
+			     we produce then ? For the moment, we suppose the
+			     .cmxs and .cma are at the same location. *)
+			 let mldir = Some (Filename.dirname f) in
+			 let filename = file_name ([String.uncapitalize s],mldir) in
+			 if Coq_config.has_natdynlink then
+			   printf " %s.cma %s.cmxs" filename filename
+			 else
+			   printf " %s.cma" filename
 		     end)
 		sl
 	  | Load str -> 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b2589d42f0..fa8fca66f5 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -78,7 +78,21 @@ let set_include d p =
   let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p)
 let set_rec_include d p =
   let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p)
- 
+
+let load_initial_plugins () =
+  (** Order matters ! For instance ground_plugin needs cc_plugin *)
+  let initial_plugins =
+    [ "extraction_plugin";
+      "jprover_plugin";
+      "cc_plugin";
+      "ground_plugin";
+      "dp_plugin";
+      "recdef_plugin";
+      (*"subtac_plugin";*)
+      "xml_plugin";
+    ] in
+  if Mltop.has_dynlink then Mltop.declare_ml_modules initial_plugins
+
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
   load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list
@@ -340,6 +354,7 @@ let init is_ide =
       if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
         Option.iter Declaremods.start_library !toplevel_name;
       init_library_roots ();
+      load_initial_plugins ();
       load_vernac_obj ();
       require ();
       load_rcfile();
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 57c1464286..611567af98 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -289,18 +289,20 @@ let cache_ml_module_object (_,{mnames=mnames}) =
     (fun name ->
        let mname = mod_of_name name in
        if not (module_is_known mname) then
-         let fname = file_of_name mname in
-         begin 
-	   try 
-	     if_verbose 
+	 if has_dynlink then
+           let fname = file_of_name mname in
+	   try
+	     if_verbose
 	       msg (str"[Loading ML file " ++ str fname ++ str" ...");
              load_object mname fname;
-             if_verbose msgnl (str"done]")
-           with e -> 
-	     if_verbose msgnl (str"failed]"); 
+             if_verbose msgnl (str"done]");
+             add_loaded_module mname
+           with e ->
+	     if_verbose msgnl (str"failed]");
 	     raise e
-	 end;
-         add_loaded_module mname)
+	 else
+	   if_verbose
+	     msgnl (str"[Ignoring ML file " ++ str mname ++ str "]"))
     mnames
 
 let export_ml_module_object x = Some x