Makefile: ml dependencies of contribs are moved to .mllib files

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

23 files changed, 174 insertions, 182 deletions

diff --git a/Makefile b/Makefile
index 80fee764ba..b94cb34da5 100644
--- a/Makefile
+++ b/Makefile
@@ -51,6 +51,7 @@ export MLFILES  := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml'  ')' $(FIN
   $(GENMLFILES)
 export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \
   $(GENMLIFILES)
+export MLLIBFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mllib' ')' $(FIND_PRINTF_P))
 export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P))
 #export VFILES   := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v'   ')' $(FIND_PRINTF_P)) \
 #  $(GENVFILES)
diff --git a/Makefile.build b/Makefile.build
index 2c16be4b4b..ecc70a1e53 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -283,59 +283,13 @@ parsing/highparsing.cmxa: $(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)
-
-$(QUOTECMA): $(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)
-
-$(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)
+contrib/%.cma: | contrib/%.mllib.d
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^
 
-$(GBCMA): $(GBCMO)
-$(GBCMA:.cma=.cmxa): $(GBCMO:.cmo=.cmx)
+contrib/%.cmxa: | contrib/%.mllib.d
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^
 
 %.cma:
 	$(SHOW)'OCAMLC -a -o $@'
@@ -451,39 +405,30 @@ ifeq ($(HASNATDYNLINK),false)
 
 # old approach, via coqmktop
 
-PCOQPLUGINS:=
-
-bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(INTERFACE)
+bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(INTERFACECMA)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ $(INTERFACE)
+	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ $(INTERFACECMA)
 
-bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMX)
+bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMA:.cma=.cmxa)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(INTERFACECMX)
+	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(INTERFACECMA:.cma=.cmxa)
 
-bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO)
+bin/coq-parser$(EXE): $(PARSERREQUIRES)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(COQRUNBYTEFLAGS) -linkall $(BYTEFLAGS) -o $@ \
-	  dynlink.cma str.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO)
+	  dynlink.cma str.cma nums.cma $(CMA) $(PARSERREQUIRES)
 
-bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX)
+bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERREQUIRESCMX)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \
-	  $(LIBCOQRUN) $(DYNLINKCMXA) str.cmxa nums.cmxa $(CMXA) $(PARSERCMX)
+	  $(LIBCOQRUN) $(DYNLINKCMXA) str.cmxa nums.cmxa $(CMXA) \
+          $(PARSERREQUIRESCMX)
 
 else 
 
 # HASNATDYNLINK is available :
 # coq-interface and coq-parser are direct calls to coqtop with some dynlink
 
-PCOQPLUGINS:=contrib/interface/coqinterface_plugin.cma \
-             contrib/interface/coqparser_plugin.cma
-
-contrib/interface/coqinterface_plugin.cma: $(INTERFACE)
-contrib/interface/coqinterface_plugin.cmxa: $(INTERFACE:.cmo=.cmx)
-contrib/interface/coqparser_plugin.cma: $(PARSERCODE)
-contrib/interface/coqparser_plugin.cmxa: $(PARSERCODE:.cmo=.cmx)
-
 bin/coq-interface$(EXE):
 	echo "#!/bin/sh" > $@
 	echo "exec coqtop -require CoqInterface" >> $@
@@ -576,20 +521,20 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
 ###########################################################################
 
 contrib: $(CONTRIBVO)
-omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
-micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
-ring: $(RINGVO) $(RINGCMO)
-setoid_ring: $(NEWRINGVO) $(NEWRINGCMO)
-dp: $(DPCMO)
-xml: $(XMLVO) $(XMLCMO)
-extraction: $(EXTRACTIONCMO)
-field: $(FIELDVO) $(FIELDCMO)
-fourier: $(FOURIERVO) $(FOURIERCMO)
-funind: $(FUNINDCMO) $(FUNINDVO)
-cc: $(CCVO) $(CCCMO)
+omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
+micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
+ring: $(RINGVO) $(RINGCMA)
+setoid_ring: $(NEWRINGVO) $(NEWRINGCMA)
+dp: $(DPCMA)
+xml: $(XMLVO) $(XMLCMA)
+extraction: $(EXTRACTIONCMA)
+field: $(FIELDVO) $(FIELDCMA)
+fourier: $(FOURIERVO) $(FOURIERCMA)
+funind: $(FUNINDCMA) $(FUNINDVO)
+cc: $(CCVO) $(CCCMA)
 programs: $(PROGRAMSVO)
-subtac: $(SUBTACVO) $(SUBTACCMO)
-rtauto: $(RTAUTOVO) $(RTAUTOCMO)
+subtac: $(SUBTACVO) $(SUBTACCMA)
+rtauto: $(RTAUTOVO) $(RTAUTOCMA)
 
 ###########################################################################
 # rules to make theories, contrib and states
@@ -1033,6 +978,11 @@ checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC)
 	$(SHOW)'OCAMLDEP  $<'
 	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' > "$@"
 
+%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEP)
+	$(SHOW)'COQDEP  $<'
+	$(HIDE)$(COQDEP) -slash -boot -c "$<" > "$@" \
+	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
 ## Veerry nasty hack to keep ocamldep happy
 %.ml: | %.ml4
 	$(SHOW)'TOUCH     $@'
diff --git a/Makefile.common b/Makefile.common
index 2eff24fcf8..71e85d7f06 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -231,105 +231,40 @@ HIGHTACTICS:=$(addprefix tactics/, \
   eauto.cmo 	class_tactics.cmo	 tauto.cmo \
   eqdecide.cmo )
 
-OMEGACMA:=contrib/omega/omega_plugin.cma
-OMEGACMO:=$(addprefix contrib/omega/, \
-  omega.cmo coq_omega.cmo g_omega.cmo )
+# NB: Dependencies of contribs are now in separate files
+#  contrib/*/*_plugin.mllib
+# Format of these files are compatible with ocamlbuild,
+# Even if we don't use it (yet ?)
 
+OMEGACMA:=contrib/omega/omega_plugin.cma
 ROMEGACMA:=contrib/romega/romega_plugin.cma
-ROMEGACMO:=$(addprefix contrib/romega/, \
-  const_omega.cmo refl_omega.cmo g_romega.cmo )
-
 MICROMEGACMA:=contrib/micromega/micromega_plugin.cma
-MICROMEGACMO:=$(addprefix contrib/micromega/, \
-  mutils.cmo micromega.cmo mfourier.cmo certificate.cmo \
-  coq_micromega.cmo 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/ring.cmo contrib/ring/g_ring.cmo 
-
 NEWRINGCMA:=contrib/setoid_ring/newring_plugin.cma
-NEWRINGCMO:=contrib/setoid_ring/newring.cmo
-
 GBCMA:=contrib/groebner/groebner_plugin.cma
-GBCMO:=$(addprefix contrib/groebner/, \
-  utile.cmo polynom.cmo ideal.cmo groebner.cmo )
-
 DPCMA:=contrib/dp/dp_plugin.cma
-DPCMO:=$(addprefix contrib/dp/, \
-  dp_why.cmo dp_zenon.cmo dp.cmo dp_gappa.cmo g_dp.cmo )
-
-FIELDCMO:=contrib/field/field.cmo
 FIELDCMA:=contrib/field/field_plugin.cma
-
 XMLCMA:=contrib/xml/xml_plugin.cma
-XMLCMO:=$(addprefix contrib/xml/, \
-  unshare.cmo xml.cmo acic.cmo doubleTypeInference.cmo \
-  cic2acic.cmo acic2Xml.cmo proof2aproof.cmo \
-  xmlcommand.cmo proofTree2Xml.cmo xmlentries.cmo cic2Xml.cmo \
-  dumptree.cmo )
-
 FOURIERCMA:=contrib/fourier/fourier_plugin.cma
-FOURIERCMO:=$(addprefix contrib/fourier/, \
-  fourier.cmo fourierR.cmo g_fourier.cmo )
-
 EXTRACTIONCMA:=contrib/extraction/extraction_plugin.cma
-EXTRACTIONCMO:=$(addprefix contrib/extraction/, \
-  table.cmo mlutil.cmo modutil.cmo extraction.cmo common.cmo \
-  ocaml.cmo haskell.cmo scheme.cmo extract_env.cmo g_extraction.cmo )
-
 FUNINDCMA:=contrib/funind/recdef_plugin.cma
-FUNINDCMO:=$(addprefix contrib/funind/, \
-  indfun_common.cmo rawtermops.cmo \
-  recdef.cmo rawterm_to_relation.cmo \
-  functional_principles_proofs.cmo \
-  functional_principles_types.cmo \
-  invfun.cmo indfun.cmo merge.cmo g_indfun.cmo )
-
 FOCMA:=contrib/firstorder/ground_plugin.cma
-FOCMO:=$(addprefix contrib/firstorder/, \
-  formula.cmo unify.cmo sequent.cmo rules.cmo instances.cmo ground.cmo \
-  g_ground.cmo )
-
 CCCMA:=contrib/cc/cc_plugin.cma
-CCCMO:=$(addprefix contrib/cc/, \
-  ccalgo.cmo ccproof.cmo cctac.cmo g_congruence.cmo )
-
 SUBTACCMA:=contrib/subtac/subtac_plugin.cma
-SUBTACCMO:=$(addprefix contrib/subtac/, \
-  subtac_utils.cmo eterm.cmo g_eterm.cmo \
-  subtac_errors.cmo subtac_coercion.cmo \
-  subtac_obligations.cmo subtac_cases.cmo \
-  subtac_pretyping_F.cmo subtac_pretyping.cmo \
-  subtac_command.cmo subtac_classes.cmo \
-  subtac.cmo g_subtac.cmo equations.cmo )
-
 RTAUTOCMA:=contrib/rtauto/rtauto_plugin.cma
-RTAUTOCMO:=$(addprefix contrib/rtauto/, \
-  proof_search.cmo refl_tauto.cmo g_rtauto.cmo )
 
-CONTRIBSTATIC:=\
-	$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
-        $(QUOTECMO) $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \
-        $(FOURIERCMO) $(EXTRACTIONCMO) $(XMLCMO) \
-        $(CCCMO)  $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \
-        $(FUNINDCMO) $(GBCMO)
-
-CONTRIBCMA:=contrib/contrib.cma
+CONTRIBS:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \
+        $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \
+        $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
+        $(CCCMA)  $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \
+        $(FUNINDCMA) $(GBCMA)
 
 ifneq ($(HASNATDYNLINK),false)
  CONTRIBSTATIC:=
- CONTRIBCMA:=
  INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
 	$(XMLCMA) $(FUNINDCMA) $(SUBTACCMA)
- PLUGINS:=$(INITPLUGINS) \
-	$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \
-        $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \
-        $(FOURIERCMA) $(RTAUTOCMA) $(GBCMA)
+ PLUGINS:=$(CONTRIBS)
  INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
  PLUGINSOPT:=$(PLUGINS:.cma=.cmxs)
  ifeq ($(BEST),opt)
@@ -337,6 +272,8 @@ ifneq ($(HASNATDYNLINK),false)
  else
   INITPLUGINSBEST:=$(INITPLUGINS)
  endif
+else
+ CONTRIBSTATIC:=$(CONTRIBS)
 endif
 
 CMA:=$(CLIBS) $(CAMLP4OBJS)
@@ -350,14 +287,13 @@ CMXA:=$(CMA:.cma=.cmxa)
 LINKCMO:=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \
         pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
-        parsing/highparsing.cma tactics/hightactics.cma $(CONTRIBCMA)
-LINKCMOCMXA:=$(LINKCMO:.cma=.cmxa)
-LINKCMX:=$(LINKCMOCMXA:.cmo=.cmx)
+        parsing/highparsing.cma tactics/hightactics.cma $(CONTRIBSTATIC)
+LINKCMX:=$(patsubst %.cma,%.cmxa,$(patsubst %.cmo,%.cmx,$(LINKCMO)))
 
 # objects known by the toplevel of Coq
 OBJSCMO:=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \
         $(PROOFS) $(PARSING) $(TACTICS) $(TOPLEVEL) $(HIGHPARSING) \
-        $(HIGHTACTICS) $(CONTRIBSTATIC)
+        $(HIGHTACTICS)
 
 COQIDECMO:=\
   $(addprefix ide/utils/, \
@@ -383,33 +319,28 @@ COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx)
 COQCCMO:=$(COQENVCMO) $(REVISIONCMO) toplevel/usage.cmo scripts/coqc.cmo
 COQCCMX:=$(COQCCMO:.cmo=.cmx)
 
-INTERFACE:=$(addprefix contrib/interface/, \
-  vtp.cmo xlate.cmo paths.cmo translate.cmo pbp.cmo dad.cmo \
-  history.cmo name_to_ast.cmo debug_tac.cmo showproof_ct.cmo showproof.cmo \
-  blast.cmo depends.cmo centaur.cmo )
+## Pcoq tools : coq-interface, coq-parser
 
-INTERFACECMX:=$(INTERFACE:.cmo=.cmx)
+COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
 
-PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité...
-PARSERREQUIRESCMX:=$(LINKCMX)
+INTERFACECMA:=contrib/interface/coqinterface_plugin.cma
+PARSERCMA:=contrib/interface/coqparser_plugin.cma
 
-COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
-ifeq ($(BEST),opt)
 ifeq ($(HASNATDYNLINK),false)
+ ifeq ($(BEST),opt)
   COQINTERFACE:=$(COQINTERFACE) bin/coq-interface.opt$(EXE) bin/coq-parser.opt$(EXE)
-endif
+ endif
+ INTERFACERC:= contrib/interface/vernacrc
+ PCOQPLUGINS:=
+else
+ INTERFACERC:= contrib/interface/vernacrc contrib/interface/CoqParser.v
+ PCOQPLUGINS:=$(INTERFACECMA) $(PARSERCMA)
 endif
 
-PARSERCODE:=contrib/interface/line_parser.cmo contrib/interface/vtp.cmo \
-           contrib/interface/xlate.cmo contrib/interface/coqparser.cmo
-PARSERCMO:=$(PARSERREQUIRES) $(PARSERCODE)
-PARSERCMX:= $(PARSERREQUIRESCMX) $(PARSERCODE:.cmo=.cmx)
+PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) $(PARSERCMA) # Solution de facilité...
+PARSERREQUIRESCMX:=$(LINKCMX) $(PARSERCMA:.cma=.cmxa)
 
-ifneq ($(HASNATDYNLINK),false)
-INTERFACERC:= contrib/interface/vernacrc
-else
-INTERFACERC:= contrib/interface/vernacrc contrib/interface/CoqParser.v
-endif
+## Misc
 
 CSDPCERTCMO:=$(addprefix contrib/micromega/, \
   mutils.cmo 	micromega.cmo 	mfourier.cmo 	certificate.cmo \
diff --git a/Makefile.stage1 b/Makefile.stage1
index a60d388fc6..a558e3aa61 100644
--- a/Makefile.stage1
+++ b/Makefile.stage1
@@ -18,6 +18,8 @@ include Makefile.build
 .SECONDARY: $(MLFILES:.ml=.ml.d)
 -include $(MLIFILES:.mli=.mli.d)
 .SECONDARY: $(MLIFILES:.mli=.mli.d)
+-include $(MLLIBFILES:.mllib=.mllib.d)
+.SECONDARY: $(MLLIBFILES:.mli=.mllib.d)
 ##Depends upon the fact that all .ml4.d for stage1 files are empty
 -include $(STAGE1_ML4:.ml4=.ml4.ml.d)
 .SECONDARY: $(STAGE1_ML4:.ml4=.ml4.ml.d)
diff --git a/contrib/cc/cc_plugin.mllib b/contrib/cc/cc_plugin.mllib
new file mode 100644
index 0000000000..27e903fd38
--- /dev/null
+++ b/contrib/cc/cc_plugin.mllib
@@ -0,0 +1,4 @@
+Ccalgo
+Ccproof
+Cctac
+G_congruence
diff --git a/contrib/dp/dp_plugin.mllib b/contrib/dp/dp_plugin.mllib
new file mode 100644
index 0000000000..361d6f8323
--- /dev/null
+++ b/contrib/dp/dp_plugin.mllib
@@ -0,0 +1,5 @@
+Dp_why
+Dp_zenon
+Dp
+Dp_gappa
+G_dp
diff --git a/contrib/extraction/extraction_plugin.mllib b/contrib/extraction/extraction_plugin.mllib
new file mode 100644
index 0000000000..bb87b9e325
--- /dev/null
+++ b/contrib/extraction/extraction_plugin.mllib
@@ -0,0 +1,10 @@
+Table
+Mlutil
+Modutil
+Extraction
+Common
+Ocaml
+Haskell
+Scheme
+Extract_env
+G_extraction
diff --git a/contrib/field/field_plugin.mllib b/contrib/field/field_plugin.mllib
new file mode 100644
index 0000000000..63492a64f0
--- /dev/null
+++ b/contrib/field/field_plugin.mllib
@@ -0,0 +1 @@
+Field
diff --git a/contrib/firstorder/ground_plugin.mllib b/contrib/firstorder/ground_plugin.mllib
new file mode 100644
index 0000000000..863ccb50e8
--- /dev/null
+++ b/contrib/firstorder/ground_plugin.mllib
@@ -0,0 +1,7 @@
+Formula
+Unify
+Sequent
+Rules
+Instances
+Ground 
+G_ground
\ No newline at end of file
diff --git a/contrib/fourier/fourier_plugin.mllib b/contrib/fourier/fourier_plugin.mllib
new file mode 100644
index 0000000000..b6262f8aeb
--- /dev/null
+++ b/contrib/fourier/fourier_plugin.mllib
@@ -0,0 +1,3 @@
+Fourier
+FourierR
+G_fourier
diff --git a/contrib/funind/recdef_plugin.mllib b/contrib/funind/recdef_plugin.mllib
new file mode 100644
index 0000000000..c30ee212f5
--- /dev/null
+++ b/contrib/funind/recdef_plugin.mllib
@@ -0,0 +1,10 @@
+Indfun_common
+Rawtermops
+Recdef
+Rawterm_to_relation
+Functional_principles_proofs
+Functional_principles_types
+Invfun
+Indfun
+Merge
+G_indfun
diff --git a/contrib/groebner/groebner_plugin.mllib b/contrib/groebner/groebner_plugin.mllib
new file mode 100644
index 0000000000..1da12fcf2e
--- /dev/null
+++ b/contrib/groebner/groebner_plugin.mllib
@@ -0,0 +1,4 @@
+Utile
+Polynom
+Ideal
+Groebner
diff --git a/contrib/interface/coqinterface_plugin.mllib b/contrib/interface/coqinterface_plugin.mllib
new file mode 100644
index 0000000000..e4b575b136
--- /dev/null
+++ b/contrib/interface/coqinterface_plugin.mllib
@@ -0,0 +1,14 @@
+Vtp
+Xlate
+Paths
+Translate
+Pbp
+Dad
+History
+Name_to_ast
+Debug_tac
+Showproof_ct
+Showproof
+Blast
+Depends
+Centaur
diff --git a/contrib/interface/coqparser_plugin.mllib b/contrib/interface/coqparser_plugin.mllib
new file mode 100644
index 0000000000..65ec577153
--- /dev/null
+++ b/contrib/interface/coqparser_plugin.mllib
@@ -0,0 +1,4 @@
+Line_parser
+Vtp
+Xlate
+Coqparser
\ No newline at end of file
diff --git a/contrib/micromega/micromega_plugin.mllib b/contrib/micromega/micromega_plugin.mllib
new file mode 100644
index 0000000000..41753542f6
--- /dev/null
+++ b/contrib/micromega/micromega_plugin.mllib
@@ -0,0 +1,6 @@
+Mutils
+Micromega
+Mfourier
+Certificate
+Coq_micromega
+G_micromega
diff --git a/contrib/omega/omega_plugin.mllib b/contrib/omega/omega_plugin.mllib
new file mode 100644
index 0000000000..0209013762
--- /dev/null
+++ b/contrib/omega/omega_plugin.mllib
@@ -0,0 +1,3 @@
+Omega
+Coq_omega
+G_omega
\ No newline at end of file
diff --git a/contrib/quote/quote_plugin.mllib b/contrib/quote/quote_plugin.mllib
new file mode 100644
index 0000000000..21810acdff
--- /dev/null
+++ b/contrib/quote/quote_plugin.mllib
@@ -0,0 +1,2 @@
+Quote
+G_quote
\ No newline at end of file
diff --git a/contrib/ring/ring_plugin.mllib b/contrib/ring/ring_plugin.mllib
new file mode 100644
index 0000000000..183884ca6d
--- /dev/null
+++ b/contrib/ring/ring_plugin.mllib
@@ -0,0 +1,2 @@
+Ring
+G_ring
diff --git a/contrib/romega/romega_plugin.mllib b/contrib/romega/romega_plugin.mllib
new file mode 100644
index 0000000000..38d0e94111
--- /dev/null
+++ b/contrib/romega/romega_plugin.mllib
@@ -0,0 +1,3 @@
+Const_omega
+Refl_omega
+G_romega
diff --git a/contrib/rtauto/rtauto_plugin.mllib b/contrib/rtauto/rtauto_plugin.mllib
new file mode 100644
index 0000000000..61c5e945bc
--- /dev/null
+++ b/contrib/rtauto/rtauto_plugin.mllib
@@ -0,0 +1,3 @@
+Proof_search
+Refl_tauto
+G_rtauto
diff --git a/contrib/setoid_ring/newring_plugin.mllib b/contrib/setoid_ring/newring_plugin.mllib
new file mode 100644
index 0000000000..54b7c8e676
--- /dev/null
+++ b/contrib/setoid_ring/newring_plugin.mllib
@@ -0,0 +1 @@
+Newring
diff --git a/contrib/subtac/subtac_plugin.mllib b/contrib/subtac/subtac_plugin.mllib
new file mode 100644
index 0000000000..81b9ee2bab
--- /dev/null
+++ b/contrib/subtac/subtac_plugin.mllib
@@ -0,0 +1,14 @@
+Subtac_utils
+Eterm
+G_eterm
+Subtac_errors
+Subtac_coercion
+Subtac_obligations
+Subtac_cases
+Subtac_pretyping_F
+Subtac_pretyping
+Subtac_command
+Subtac_classes
+Subtac
+G_subtac
+Equations
diff --git a/contrib/xml/xml_plugin.mllib b/contrib/xml/xml_plugin.mllib
new file mode 100644
index 0000000000..3297ff0684
--- /dev/null
+++ b/contrib/xml/xml_plugin.mllib
@@ -0,0 +1,12 @@
+Unshare
+Xml
+Acic
+DoubleTypeInference
+Cic2acic
+Acic2Xml
+Proof2aproof
+Xmlcommand
+ProofTree2Xml
+Xmlentries
+Cic2Xml
+Dumptree