Compilation via pack for plugins of the stdlib

 For now, the pack name reuse the previous .cma name of the plugin,
 (extraction_plugin, etc).

 The earlier .mllib files in plugins are now named .mlpack.
 They are also handled by bin/ocamllibdep, just as .mllib.
 We've slightly modified ocamllibdep to help setting the -for-pack
 options: in *.mlpack.d files, there are some extra variables such as
  foo/bar_FORPACK := -for-pack Baz
 when foo/bar.ml is mentioned in baz.mlpack.

 When a plugin is calling a function from another plugin, the name
 need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz).

 Btw, we discard the generated files plugins/*/*_mod.ml, they are
 obsolete now, replaced by DECLARE PLUGIN.

 Nota: there's a potential problem in the micromega directory,
 some .ml files are linked both in micromega_plugin and in csdpcert.
 And we now compile these files with a -for-pack, even if they are
 not packed in the case of csdpcert. In practice, csdpcert seems
 to work well, but we should verify with OCaml experts.

47 files changed, 141 insertions, 102 deletions

diff --git a/.gitignore b/.gitignore
index 116f88dd7e..1cbf56e3cb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -44,7 +44,6 @@ TAGS
 .pc
 bin/
 _build
-plugins/*/*_mod.ml
 myocamlbuild_config.ml
 config/Makefile
 config/coq_config.ml
@@ -114,7 +113,7 @@ tools/ocamllibdep.ml
 tools/coqdoc/cpretty.ml
 ide/xml_lexer.ml
 
-# .ml4 files
+# .ml4 / .mlp files
 
 g_*.ml
 
diff --git a/Makefile b/Makefile
index aeb54fba8c..93b89a4893 100644
--- a/Makefile
+++ b/Makefile
@@ -66,7 +66,7 @@ endef
 ## Files in the source tree
 
 LEXFILES := $(call find, '*.mll')
-export MLLIBFILES := $(call find, '*.mllib')
+export MLLIBFILES := $(call find, '*.mllib') $(call find, '*.mlpack')
 export ML4FILES := $(call find, '*.ml4')
 export CFILES := $(call find, '*.c')
 
@@ -80,9 +80,7 @@ EXISTINGMLI := $(call find, '*.mli')
 ## Files that will be generated
 
 GENML4FILES:= $(ML4FILES:.ml4=.ml)
-GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
-export GENMLFILES:=$(LEXFILES:.mll=.ml) $(GENPLUGINSMOD) \
-  tools/tolink.ml kernel/copcodes.ml
+export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
 export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
diff --git a/Makefile.build b/Makefile.build
index 69228e3791..4eafe1d619 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -502,6 +502,16 @@ endif
 	$(SHOW)'OCAMLOPT -a -o $@'
 	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
+# For plugin packs :
+
+%.cmo: %.mlpack
+	$(SHOW)'OCAMLC -pack -o $@'
+	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
+
+%.cmx: %.mlpack
+	$(SHOW)'OCAMLOPT -pack -o $@'
+	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
+
 COND_BYTEFLAGS= \
  $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS)
 
@@ -537,18 +547,22 @@ $(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi  # for .ml with .mli this is already the
 
 $(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo
 
+# NB: the *_FORPACK variables are generated in *.mlpack.d by ocamllibdep
+# The only exceptions are the sources of the csdpcert binary.
+# To avoid warnings, we set them manually here:
+plugins/micromega/sos_lib_FORPACK:=
+plugins/micromega/sos_FORPACK:=
+plugins/micromega/sos_print_FORPACK:=
+plugins/micromega/csdpcert_FORPACK:=
+
+plugins/%.cmx: plugins/%.ml
+	$(SHOW)'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<
+
 %.cmx: %.ml
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $<
 
-%.cmxs: %.cmxa
-	$(SHOW)'OCAMLOPT -shared -o $@'
-ifeq ($(HASNATDYNLINK),os5fixme)
-	$(HIDE)dev/ocamlopt_shared_os5fix.sh "$(OCAMLOPT)" $@
-else
-	$(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
-endif
-
 %.cmxs: %.cmx
 	$(SHOW)'OCAMLOPT -shared -o $@'
 	$(HIDE)$(OCAMLOPT) -shared -o $@ $<
@@ -557,11 +571,6 @@ endif
 	$(SHOW)'OCAMLLEX  $<'
 	$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
 
-plugins/%_mod.ml: plugins/%.mllib
-	$(SHOW)'ECHO... > $@'
-	$(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
-	$(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@
-
 %.ml: %.ml4 | $(CAMLP4DEPS)
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) \
@@ -573,7 +582,7 @@ plugins/%_mod.ml: plugins/%.mllib
 ###########################################################################
 
 # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12)
-OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4
+OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
 
 %.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
@@ -587,6 +596,10 @@ OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4
 	$(SHOW)'OCAMLLIBDEP  $<'
 	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
+%.mlpack.d: $(D_DEPEND_BEFORE_SRC) %.mlpack $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES)
+	$(SHOW)'OCAMLLIBDEP  $<'
+	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET)
+
 ###########################################################################
 # Compilation of .v files
 ###########################################################################
diff --git a/Makefile.common b/Makefile.common
index 463006c49d..4742bb51e8 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -97,28 +97,28 @@ OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib))
 # plugins object files
 ###########################################################################
 
-OMEGACMA:=plugins/omega/omega_plugin.cma
-ROMEGACMA:=plugins/romega/romega_plugin.cma
-MICROMEGACMA:=plugins/micromega/micromega_plugin.cma
-QUOTECMA:=plugins/quote/quote_plugin.cma
-RINGCMA:=plugins/setoid_ring/newring_plugin.cma
-NSATZCMA:=plugins/nsatz/nsatz_plugin.cma
-FOURIERCMA:=plugins/fourier/fourier_plugin.cma
-EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma
-FUNINDCMA:=plugins/funind/recdef_plugin.cma
-FOCMA:=plugins/firstorder/ground_plugin.cma
-CCCMA:=plugins/cc/cc_plugin.cma
-BTAUTOCMA:=plugins/btauto/btauto_plugin.cma
-RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma
-NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma
+OMEGACMA:=plugins/omega/omega_plugin.cmo
+ROMEGACMA:=plugins/romega/romega_plugin.cmo
+MICROMEGACMA:=plugins/micromega/micromega_plugin.cmo
+QUOTECMA:=plugins/quote/quote_plugin.cmo
+RINGCMA:=plugins/setoid_ring/newring_plugin.cmo
+NSATZCMA:=plugins/nsatz/nsatz_plugin.cmo
+FOURIERCMA:=plugins/fourier/fourier_plugin.cmo
+EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cmo
+FUNINDCMA:=plugins/funind/recdef_plugin.cmo
+FOCMA:=plugins/firstorder/ground_plugin.cmo
+CCCMA:=plugins/cc/cc_plugin.cmo
+BTAUTOCMA:=plugins/btauto/btauto_plugin.cmo
+RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cmo
+NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cmo
 OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
-        z_syntax_plugin.cma \
-        numbers_syntax_plugin.cma \
-        r_syntax_plugin.cma \
-	ascii_syntax_plugin.cma \
-        string_syntax_plugin.cma )
-DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
-DERIVECMA:=plugins/derive/derive_plugin.cma
+        z_syntax_plugin.cmo \
+        numbers_syntax_plugin.cmo \
+        r_syntax_plugin.cmo \
+	ascii_syntax_plugin.cmo \
+        string_syntax_plugin.cmo )
+DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cmo
+DERIVECMA:=plugins/derive/derive_plugin.cmo
 
 PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
         $(QUOTECMA) $(RINGCMA) \
@@ -131,17 +131,17 @@ ifneq ($(HASNATDYNLINK),false)
  STATICPLUGINS:=
  INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
 	$(FUNINDCMA) $(NATSYNTAXCMA)
- INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
+ INITPLUGINSOPT:=$(INITPLUGINS:.cmo=.cmxs)
  PLUGINS:=$(PLUGINSCMA)
- PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
+ PLUGINSOPT:=$(PLUGINSCMA:.cmo=.cmxs)
 else
 ifeq ($(BEST),byte)
  STATICPLUGINS:=
  INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
 	$(FUNINDCMA) $(NATSYNTAXCMA)
- INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
+ INITPLUGINSOPT:=$(INITPLUGINS:.cmo=.cmxs)
  PLUGINS:=$(PLUGINSCMA)
- PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
+ PLUGINSOPT:=$(PLUGINSCMA:.cmo=.cmxs)
 else
  STATICPLUGINS:=$(PLUGINSCMA)
  INITPLUGINS:=
@@ -152,7 +152,7 @@ endif
 endif
 
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
-LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
+LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
 
 ###########################################################################
 # vo files
diff --git a/plugins/btauto/btauto_plugin.mllib b/plugins/btauto/btauto_plugin.mlpack
index 319a9c302a..2410f906a3 100644
--- a/plugins/btauto/btauto_plugin.mllib
+++ b/plugins/btauto/btauto_plugin.mlpack
@@ -1,3 +1,2 @@
 Refl_btauto
 G_btauto
-Btauto_plugin_mod
diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mlpack
index 1bcfc5378b..27e903fd38 100644
--- a/plugins/cc/cc_plugin.mllib
+++ b/plugins/cc/cc_plugin.mlpack
@@ -2,4 +2,3 @@ Ccalgo
 Ccproof
 Cctac
 G_congruence
-Cc_plugin_mod
diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mlpack
index 39342dbd1c..1b84a0790f 100644
--- a/plugins/decl_mode/decl_mode_plugin.mllib
+++ b/plugins/decl_mode/decl_mode_plugin.mlpack
@@ -3,4 +3,3 @@ Decl_interp
 Decl_proof_instr
 Ppdecl_proof
 G_decl_mode
-Decl_mode_plugin_mod
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 78a95143df..0feba6365c 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "decl_mode_plugin"
+
 open Compat
 open Pp
 open Decl_expr
diff --git a/plugins/derive/derive_plugin.mllib b/plugins/derive/derive_plugin.mlpack
index 5ee0fc6da6..5ee0fc6da6 100644
--- a/plugins/derive/derive_plugin.mllib
+++ b/plugins/derive/derive_plugin.mlpack
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index 39cad4d03c..d4dc7e0eed 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -10,6 +10,8 @@ open Constrarg
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+DECLARE PLUGIN "derive_plugin"
+
 let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command
diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mlpack
index ad32124347..9184f65017 100644
--- a/plugins/extraction/extraction_plugin.mllib
+++ b/plugins/extraction/extraction_plugin.mlpack
@@ -9,4 +9,3 @@ Scheme
 Json
 Extract_env
 G_extraction
-Extraction_plugin_mod
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 0a8cb0ccd3..19fda4aead 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "extraction_plugin"
+
 (* ML names *)
 
 open Genarg
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index a78532e339..cec3505a97 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -153,6 +153,8 @@ TACTIC EXTEND gintuition
 END
 
 open Proofview.Notations
+open Cc_plugin
+open Decl_mode_plugin
 
 let default_declarative_automation =
   Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mlpack
index 447a1fb513..65fb2e9a1d 100644
--- a/plugins/firstorder/ground_plugin.mllib
+++ b/plugins/firstorder/ground_plugin.mlpack
@@ -5,4 +5,3 @@ Rules
 Instances
 Ground
 G_ground
-Ground_plugin_mod
diff --git a/plugins/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mlpack
index 0383b1a80b..b6262f8aeb 100644
--- a/plugins/fourier/fourier_plugin.mllib
+++ b/plugins/fourier/fourier_plugin.mlpack
@@ -1,4 +1,3 @@
 Fourier
 FourierR
 G_fourier
-Fourier_plugin_mod
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 80866e8b8c..95b4967faa 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1529,7 +1529,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let hook _ _ = 
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
-    let _ = Table.extraction_inline true [Ident (Loc.ghost,term_id)] in 
+    let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.ghost,term_id)] in
     (*     message "start second proof"; *)
     let stop = 
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mlpack
index ec1f5436ca..2b443f2a1b 100644
--- a/plugins/funind/recdef_plugin.mllib
+++ b/plugins/funind/recdef_plugin.mlpack
@@ -8,4 +8,3 @@ Invfun
 Indfun
 Merge
 G_indfun
-Recdef_plugin_mod
diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mlpack
index f53a9e3797..ed253da3fd 100644
--- a/plugins/micromega/micromega_plugin.mllib
+++ b/plugins/micromega/micromega_plugin.mlpack
@@ -7,4 +7,3 @@ Certificate
 Persistent_cache
 Coq_micromega
 G_micromega
-Micromega_plugin_mod
diff --git a/plugins/nsatz/nsatz_plugin.mllib b/plugins/nsatz/nsatz_plugin.mlpack
index e991fb76f7..b55adf43c0 100644
--- a/plugins/nsatz/nsatz_plugin.mllib
+++ b/plugins/nsatz/nsatz_plugin.mlpack
@@ -3,4 +3,3 @@ Polynom
 Ideal
 Nsatz
 G_nsatz
-Nsatz_plugin_mod
diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mlpack
index 2b387fdcee..df7f1047f2 100644
--- a/plugins/omega/omega_plugin.mllib
+++ b/plugins/omega/omega_plugin.mlpack
@@ -1,4 +1,3 @@
 Omega
 Coq_omega
 G_omega
-Omega_plugin_mod
diff --git a/plugins/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib
deleted file mode 100644
index d1b3ccbe1e..0000000000
--- a/plugins/quote/quote_plugin.mllib
+++ /dev/null
@@ -1,3 +0,0 @@
-Quote
-G_quote
-Quote_plugin_mod
diff --git a/plugins/quote/quote_plugin.mlpack b/plugins/quote/quote_plugin.mlpack
new file mode 100644
index 0000000000..2e9be09d8d
--- /dev/null
+++ b/plugins/quote/quote_plugin.mlpack
@@ -0,0 +1,2 @@
+Quote
+G_quote
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 007a9ec673..a059512d84 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -9,7 +9,7 @@
 open Pp
 open Util
 open Const_omega
-module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
+module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
 
 (* \section{Useful functions and flags} *)
diff --git a/plugins/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mlpack
index 1625009d06..38d0e94111 100644
--- a/plugins/romega/romega_plugin.mllib
+++ b/plugins/romega/romega_plugin.mlpack
@@ -1,4 +1,3 @@
 Const_omega
 Refl_omega
 G_romega
-Romega_plugin_mod
diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mlpack
index 0e34604495..61c5e945bc 100644
--- a/plugins/rtauto/rtauto_plugin.mllib
+++ b/plugins/rtauto/rtauto_plugin.mlpack
@@ -1,4 +1,3 @@
 Proof_search
 Refl_tauto
 G_rtauto
-Rtauto_plugin_mod
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 154ec6e1bf..7af72b07cf 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -106,6 +106,7 @@ let protect_tac_in map id =
 (****************************************************************************)
 
 let closed_term t l =
+  let open Quote_plugin in
   let l = List.map Universes.constr_of_global l in
   let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
   if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt())
diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib
deleted file mode 100644
index 7d6c495889..0000000000
--- a/plugins/setoid_ring/newring_plugin.mllib
+++ /dev/null
@@ -1,3 +0,0 @@
-Newring
-Newring_plugin_mod
-G_newring
diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack
new file mode 100644
index 0000000000..23663b4090
--- /dev/null
+++ b/plugins/setoid_ring/newring_plugin.mlpack
@@ -0,0 +1,2 @@
+Newring
+G_newring
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 67c9dd0a38..03b49e3336 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "ascii_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 open Pp
 open Errors
 open Util
diff --git a/plugins/syntax/ascii_syntax_plugin.mllib b/plugins/syntax/ascii_syntax_plugin.mllib
deleted file mode 100644
index b00f92506e..0000000000
--- a/plugins/syntax/ascii_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Ascii_syntax
-Ascii_syntax_plugin_mod
diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack
new file mode 100644
index 0000000000..7b9213a0e2
--- /dev/null
+++ b/plugins/syntax/ascii_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Ascii_syntax
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index fe9386039f..3142c8cf00 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "nat_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 (* This file defines the printer for natural numbers in [nat] *)
 
 (*i*)
diff --git a/plugins/syntax/nat_syntax_plugin.mllib b/plugins/syntax/nat_syntax_plugin.mllib
deleted file mode 100644
index 69b0cb20f6..0000000000
--- a/plugins/syntax/nat_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Nat_syntax
-Nat_syntax_plugin_mod
diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack
new file mode 100644
index 0000000000..39bdd62f47
--- /dev/null
+++ b/plugins/syntax/nat_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Nat_syntax
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index fe9f1319eb..57cb2f897a 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "numbers_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
 open Bigint
@@ -180,7 +184,7 @@ let bigN_of_pos_bigint dloc n =
   let word = word_of_pos_bigint dloc h n in
   let args =
     if h < n_inlined then [word]
-    else [Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word]
+    else [Nat_syntax_plugin.Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word]
   in
   GApp (dloc, ref_constructor, args)
 
diff --git a/plugins/syntax/numbers_syntax_plugin.mllib b/plugins/syntax/numbers_syntax_plugin.mllib
deleted file mode 100644
index ebc0bb2022..0000000000
--- a/plugins/syntax/numbers_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Numbers_syntax
-Numbers_syntax_plugin_mod
diff --git a/plugins/syntax/numbers_syntax_plugin.mlpack b/plugins/syntax/numbers_syntax_plugin.mlpack
new file mode 100644
index 0000000000..e48c00a0d0
--- /dev/null
+++ b/plugins/syntax/numbers_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Numbers_syntax
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 05d73f9ec1..3ae2d45f32 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -10,6 +10,10 @@ open Util
 open Names
 open Globnames
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "r_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 exception Non_closed_number
 
 (**********************************************************************)
diff --git a/plugins/syntax/r_syntax_plugin.mllib b/plugins/syntax/r_syntax_plugin.mllib
deleted file mode 100644
index 5c173a140f..0000000000
--- a/plugins/syntax/r_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-R_syntax
-R_syntax_plugin_mod
diff --git a/plugins/syntax/r_syntax_plugin.mlpack b/plugins/syntax/r_syntax_plugin.mlpack
new file mode 100644
index 0000000000..d4ee75ea48
--- /dev/null
+++ b/plugins/syntax/r_syntax_plugin.mlpack
@@ -0,0 +1 @@
+R_syntax
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 2e696f391f..de0fa77eff 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -7,10 +7,14 @@
 (***********************************************************************)
 
 open Globnames
-open Ascii_syntax
+open Ascii_syntax_plugin.Ascii_syntax
 open Glob_term
 open Coqlib
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "string_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 exception Non_closed_string
 
 (* make a string term from the string s *)
diff --git a/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib
deleted file mode 100644
index b108c9e007..0000000000
--- a/plugins/syntax/string_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-String_syntax
-String_syntax_plugin_mod
diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack
new file mode 100644
index 0000000000..45d6e0fa23
--- /dev/null
+++ b/plugins/syntax/string_syntax_plugin.mlpack
@@ -0,0 +1 @@
+String_syntax
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 53c1b5d7a0..ce86c0a65f 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -12,6 +12,10 @@ open Util
 open Names
 open Bigint
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "z_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 exception Non_closed_number
 
 (**********************************************************************)
diff --git a/plugins/syntax/z_syntax_plugin.mllib b/plugins/syntax/z_syntax_plugin.mllib
deleted file mode 100644
index 36d41acc20..0000000000
--- a/plugins/syntax/z_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Z_syntax
-Z_syntax_plugin_mod
diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack
new file mode 100644
index 0000000000..411260c04c
--- /dev/null
+++ b/plugins/syntax/z_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Z_syntax
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 670ff487c5..57fcd5dd21 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -33,10 +33,6 @@ rule mllib_list = parse
 open Printf
 open Unix
 
-(** [coqdep_boot] is a stripped-down version of [coqdep] used to treat
-    with mllib files.
-*)
-
 (* Makefile's escaping rules are awful: $ is escaped by doubling and
    other special characters are escaped by backslash prefixing while
    backslashes themselves must be escaped only if part of a sequence
@@ -132,6 +128,7 @@ let add_ml_known, search_ml_known = mkknown ()
 let add_mlpack_known, search_mlpack_known = mkknown ()
 
 let mllibAccu = ref ([] : (string * dir) list)
+let mlpackAccu = ref ([] : (string * dir) list)
 
 let add_caml_known phys_dir f =
   let basename,suff = get_extension f [".ml";".ml4";".mlpack"] in
@@ -148,18 +145,15 @@ let traite_fichier_modules md ext =
     let chan = open_in (md ^ ext) in
     let list = mllib_list (Lexing.from_channel chan) in
     List.fold_left
-      (fun a_faire str -> match search_mlpack_known str with
-	| Some mldir ->
-	  let file = file_name str mldir in
-	  a_faire^" "^file
-	| None ->
+      (fun acc str ->
+       match search_mlpack_known str with
+       | Some mldir -> (file_name str mldir) :: acc
+       | None ->
 	  match search_ml_known str with
-	    | Some mldir ->
-	      let file = file_name str mldir in
-	      a_faire^" "^file
-	    | None -> a_faire) "" list
+	  | Some mldir -> (file_name str mldir) :: acc
+	  | None -> acc) [] (List.rev list)
   with
-    | Sys_error _ -> ""
+    | Sys_error _ -> []
     | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j)
 
 let addQueue q v = q := v :: !q
@@ -167,22 +161,43 @@ let addQueue q v = q := v :: !q
 let treat_file old_name =
   let name = Filename.basename old_name in
   let dirname = Some (Filename.dirname old_name) in
-  match get_extension name [".mllib"] with
+  match get_extension name [".mllib";".mlpack"] with
   | (base,".mllib") -> addQueue mllibAccu (base,dirname)
+  | (base,".mlpack") -> addQueue mlpackAccu (base,dirname)
   | _ -> ()
 
 let mllib_dependencies () =
   List.iter
     (fun (name,dirname) ->
        let fullname = file_name name dirname in
-       let dep = traite_fichier_modules fullname ".mllib" in
+       let deps = traite_fichier_modules fullname ".mllib" in
+       let sdeps = String.concat " " deps in
        let efullname = escape fullname in
-       printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep;
-       printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
-       printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname efullname;
+       printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname sdeps;
+       printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n"
+         efullname efullname;
+       printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n"
+         efullname efullname efullname;
        flush Pervasives.stdout)
     (List.rev !mllibAccu)
 
+let mlpack_dependencies () =
+  List.iter
+    (fun (name,dirname) ->
+       let fullname = file_name name dirname in
+       let modname = String.capitalize name in
+       let deps = traite_fichier_modules fullname ".mlpack" in
+       let sdeps = String.concat " " deps in
+       let efullname = escape fullname in
+       printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname sdeps;
+       List.iter (fun d -> printf "%s_FORPACK:= -for-pack %s\n" d modname) deps;
+       printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n"
+         efullname efullname;
+       printf "%s.cmx %s.cmxs:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n"
+         efullname efullname efullname;
+       flush Pervasives.stdout)
+    (List.rev !mlpackAccu)
+
 let rec parse = function
   | "-I" :: r :: ll ->
        (* To solve conflict (e.g. same filename in kernel and checker)
@@ -192,10 +207,11 @@ let rec parse = function
   | f :: ll -> treat_file f; parse ll
   | [] -> ()
 
-let coqdep_boot () =
+let main () =
   if Array.length Sys.argv < 2 then exit 1;
   parse (List.tl (Array.to_list Sys.argv));
-  mllib_dependencies ()
+  mllib_dependencies ();
+  mlpack_dependencies ()
 
-let _ = Printexc.catch coqdep_boot ()
+let _ = Printexc.catch main ()
 }