Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 218 insertions, 695 deletions

diff --git a/Makefile.common b/Makefile.common
index 4d76e9e5..cc38980c 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -30,9 +30,14 @@ CHICKENOPT:=bin/coqchk.opt$(EXE)
 BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
 CHICKEN:=bin/coqchk$(EXE)
 
-ifeq ($(HASNATDYNLINK),true)
+ifneq ($(HASNATDYNLINK),false)
   DYNLINKCMXA:=dynlink.cmxa
   NATDYNLINKDEF:=-DHasDynlink
+  DEPNATDYN:=
+else
+  DYNLINKCMXA:=
+  NATDYNLINKDEF:=
+  DEPNATDYN:=-natdynlink no
 endif
 
 INSTALLBIN:=install
@@ -53,13 +58,29 @@ COQBINARIES:= $(COQMKTOP) $(COQC) \
 endif
 OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
 
-CSDPCERT:=contrib/micromega/csdpcert$(EXE)
+CSDPCERT:=plugins/micromega/csdpcert$(EXE)
+
+SRCDIRS:=\
+  config 	tools 		tools/coqdoc 	scripts		lib \
+  kernel	kernel/byterun	library 	proofs 		tactics \
+  pretyping	interp		toplevel 	parsing 	ide/utils \
+  ide		\
+  $(addprefix plugins/, \
+    omega	romega 		micromega 	quote		ring	dp \
+    setoid_ring xml 		extraction 	fourier \
+    cc 		funind 		firstorder 	field 		subtac \
+    rtauto 	nsatz           syntax)
+
+# Order is relevent here because kernel and checker contain files
+# with the same name
+CHKSRCDIRS:= checker lib config kernel
 
 ###########################################################################
 # tools
 ###########################################################################
 
 COQDEP:=bin/coqdep$(EXE)
+COQDEPBOOT:=bin/coqdep_boot$(EXE)
 COQMAKEFILE:=bin/coq_makefile$(EXE)
 GALLINA:=bin/gallina$(EXE)
 COQTEX:=bin/coq-tex$(EXE)
@@ -85,30 +106,26 @@ COQTEXOPTS:=-n 72 -image "$(COQSRC)/$(COQTOPEXE) -boot" -sl -small
 
 DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex 
 
-REFMANCOQTEXFILES:=\
-  doc/refman/RefMan-gal.v.tex doc/refman/RefMan-ext.v.tex \
-  doc/refman/RefMan-mod.v.tex doc/refman/RefMan-tac.v.tex \
-  doc/refman/RefMan-cic.v.tex doc/refman/RefMan-lib.v.tex \
-  doc/refman/RefMan-tacex.v.tex doc/refman/RefMan-syn.v.tex \
-  doc/refman/RefMan-oth.v.tex doc/refman/RefMan-ltac.v.tex \
-  doc/refman/RefMan-decl.v.tex \
-  doc/refman/Cases.v.tex doc/refman/Coercion.v.tex doc/refman/Extraction.v.tex \
-  doc/refman/Program.v.tex doc/refman/Omega.v.tex doc/refman/Micromega.v.tex doc/refman/Polynom.v.tex \
-  doc/refman/Setoid.v.tex doc/refman/Helm.tex doc/refman/Classes.v.tex
-
-REFMANTEXFILES:=\
-  doc/refman/headers.sty \
-  doc/refman/Reference-Manual.tex doc/refman/RefMan-pre.tex \
-  doc/refman/RefMan-int.tex doc/refman/RefMan-pro.tex \
-  doc/refman/RefMan-com.tex \
-  doc/refman/RefMan-uti.tex doc/refman/RefMan-ide.tex \
-  doc/refman/RefMan-add.tex doc/refman/RefMan-modr.tex \
-  doc/refman/ExternalProvers.tex \
+REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
+  RefMan-gal.v.tex RefMan-ext.v.tex \
+  RefMan-mod.v.tex RefMan-tac.v.tex \
+  RefMan-cic.v.tex RefMan-lib.v.tex \
+  RefMan-tacex.v.tex RefMan-syn.v.tex \
+  RefMan-oth.v.tex RefMan-ltac.v.tex \
+  RefMan-decl.v.tex \
+  Cases.v.tex Coercion.v.tex Extraction.v.tex \
+  Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
+  Setoid.v.tex Helm.tex Classes.v.tex )
+
+REFMANTEXFILES:=$(addprefix doc/refman/, \
+  headers.sty Reference-Manual.tex \
+  RefMan-pre.tex RefMan-int.tex RefMan-pro.tex RefMan-com.tex \
+  RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \
   $(REFMANCOQTEXFILES) \
 
 REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps
 
-REFMANFILES:=$(REFMANTEXFILES) $(COMMON) $(REFMANEPSFILES) doc/refman/biblio.bib
+REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib
 
 REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
 
@@ -126,351 +143,126 @@ CLIBS:=unix.cma
 
 CAMLP4OBJS:=gramlib.cma
 
-CONFIG:=\
-  config/coq_config.cmo
-
-LIBREP:=\
-  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
-  lib/util.cmo lib/bigint.cmo lib/hashcons.cmo lib/dyn.cmo lib/system.cmo \
-  lib/envars.cmo lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \
-  lib/tlm.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \
-  lib/predicate.cmo lib/rtree.cmo lib/heap.cmo lib/option.cmo
-# Rem: Cygwin already uses variable LIB 
-
-BYTERUN:=\
-  kernel/byterun/coq_fix_code.o kernel/byterun/coq_memory.o \
-  kernel/byterun/coq_values.o kernel/byterun/coq_interp.o 
-
-KERNEL:=\
-  kernel/names.cmo kernel/univ.cmo \
-  kernel/esubst.cmo kernel/term.cmo \
-  kernel/mod_subst.cmo kernel/sign.cmo \
-  kernel/cbytecodes.cmo kernel/copcodes.cmo \
-  kernel/cemitcodes.cmo kernel/vm.cmo \
-  kernel/declarations.cmo \
-  kernel/retroknowledge.cmo kernel/pre_env.cmo \
-  kernel/cbytegen.cmo  kernel/environ.cmo  \
-  kernel/csymtable.cmo kernel/conv_oracle.cmo \
-  kernel/closure.cmo kernel/reduction.cmo kernel/type_errors.cmo \
-  kernel/entries.cmo kernel/modops.cmo \
-  kernel/inductive.cmo kernel/vconv.cmo kernel/typeops.cmo \
-  kernel/indtypes.cmo kernel/cooking.cmo kernel/term_typing.cmo \
-  kernel/subtyping.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo
-
-LIBRARY:=\
-  library/nameops.cmo library/libnames.cmo library/libobject.cmo \
-  library/summary.cmo library/nametab.cmo library/global.cmo library/lib.cmo \
-  library/declaremods.cmo library/library.cmo library/states.cmo \
-  library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo \
-  library/decls.cmo library/heads.cmo
-
-PRETYPING:=\
-  pretyping/termops.cmo pretyping/evd.cmo \
-  pretyping/reductionops.cmo pretyping/vnorm.cmo pretyping/inductiveops.cmo \
-  pretyping/retyping.cmo pretyping/cbv.cmo \
-  pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \
-  pretyping/tacred.cmo pretyping/evarutil.cmo pretyping/evarconv.cmo \
-  pretyping/typeclasses_errors.cmo pretyping/typeclasses.cmo \
-  pretyping/classops.cmo pretyping/coercion.cmo \
-  pretyping/unification.cmo pretyping/clenv.cmo \
-  pretyping/rawterm.cmo pretyping/pattern.cmo \
-  pretyping/detyping.cmo  pretyping/indrec.cmo\
-  pretyping/cases.cmo pretyping/pretyping.cmo pretyping/matching.cmo
-
-INTERP:=\
-  parsing/lexer.cmo interp/topconstr.cmo interp/ppextend.cmo \
-  interp/notation.cmo interp/dumpglob.cmo \
-  interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \
-  library/impargs.cmo interp/implicit_quantifiers.cmo interp/constrintern.cmo \
-  interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \
-  toplevel/discharge.cmo library/declare.cmo
-
-PROOFS:=\
-  proofs/tacexpr.cmo proofs/proof_type.cmo proofs/redexpr.cmo \
-  proofs/proof_trees.cmo proofs/logic.cmo \
-  proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \
-  proofs/pfedit.cmo proofs/tactic_debug.cmo \
-  proofs/clenvtac.cmo proofs/decl_mode.cmo
-
-PARSING:=\
-  parsing/extend.cmo \
-  parsing/pcoq.cmo parsing/egrammar.cmo parsing/g_xml.cmo \
-  parsing/ppconstr.cmo parsing/printer.cmo \
-  parsing/pptactic.cmo parsing/ppdecl_proof.cmo parsing/tactic_printer.cmo \
-  parsing/printmod.cmo parsing/prettyp.cmo parsing/search.cmo 
-
-HIGHPARSING:=\
-  parsing/g_constr.cmo parsing/g_vernac.cmo parsing/g_prim.cmo \
-  parsing/g_proofs.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo \
-  parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \
-  parsing/g_ascii_syntax.cmo parsing/g_string_syntax.cmo \
-  parsing/g_decl_mode.cmo parsing/g_intsyntax.cmo 
-
-TACTICS:=\
-  tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
-  tactics/nbtermdn.cmo tactics/tacticals.cmo \
-  tactics/hipattern.cmo tactics/tactics.cmo \
-  tactics/hiddentac.cmo tactics/elim.cmo \
-  tactics/dhyp.cmo tactics/auto.cmo \
-  toplevel/ind_tables.cmo tactics/equality.cmo \
-  tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \
-  tactics/tacinterp.cmo tactics/autorewrite.cmo tactics/evar_tactics.cmo \
-  tactics/decl_interp.cmo tactics/decl_proof_instr.cmo
-
-TOPLEVEL:=\
-  toplevel/himsg.cmo toplevel/cerrors.cmo \
-  toplevel/class.cmo toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \
-  toplevel/auto_ind_decl.cmo \
-  toplevel/command.cmo toplevel/record.cmo \
-  parsing/ppvernac.cmo toplevel/classes.cmo \
-  toplevel/vernacinterp.cmo toplevel/mltop.cmo \
-  toplevel/vernacentries.cmo toplevel/whelp.cmo toplevel/vernac.cmo \
-  toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \
-  toplevel/toplevel.cmo $(REVISIONCMO) toplevel/usage.cmo \
-  toplevel/coqinit.cmo toplevel/coqtop.cmo
-
-HIGHTACTICS:=\
-  tactics/refine.cmo tactics/extraargs.cmo \
-  tactics/extratactics.cmo tactics/eauto.cmo tactics/class_tactics.cmo \
-  tactics/tauto.cmo tactics/eqdecide.cmo
-
-OMEGACMO:=\
-  contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
-  contrib/omega/g_omega.cmo 
-
-ROMEGACMO:=\
-  contrib/romega/const_omega.cmo \
-  contrib/romega/refl_omega.cmo contrib/romega/g_romega.cmo
-
-MICROMEGACMO:=\
-  contrib/micromega/mutils.cmo contrib/micromega/vector.cmo \
-  contrib/micromega/micromega.cmo contrib/micromega/mfourier.cmo \
-  contrib/micromega/certificate.cmo \
-  contrib/micromega/coq_micromega.cmo contrib/micromega/g_micromega.cmo
-
-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
-
-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 
-
-XMLCMO:=\
-  contrib/xml/unshare.cmo contrib/xml/xml.cmo contrib/xml/acic.cmo \
-  contrib/xml/doubleTypeInference.cmo \
-  contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \
-  contrib/xml/proof2aproof.cmo \
-  contrib/xml/xmlcommand.cmo contrib/xml/proofTree2Xml.cmo \
-  contrib/xml/xmlentries.cmo 	contrib/xml/cic2Xml.cmo \
-  contrib/xml/dumptree.cmo
-
-FOURIERCMO:=\
-  contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo \
-  contrib/fourier/g_fourier.cmo
-
-EXTRACTIONCMO:=\
-  contrib/extraction/table.cmo\
-  contrib/extraction/mlutil.cmo\
-  contrib/extraction/modutil.cmo \
-  contrib/extraction/extraction.cmo \
-  contrib/extraction/common.cmo \
-  contrib/extraction/ocaml.cmo \
-  contrib/extraction/haskell.cmo \
-  contrib/extraction/scheme.cmo \
-  contrib/extraction/extract_env.cmo \
-  contrib/extraction/g_extraction.cmo
-
-FUNINDCMO:=\
-  contrib/funind/indfun_common.cmo contrib/funind/rawtermops.cmo \
-  contrib/funind/recdef.cmo \
-  contrib/funind/rawterm_to_relation.cmo \
-  contrib/funind/functional_principles_proofs.cmo \
-  contrib/funind/functional_principles_types.cmo \
-  contrib/funind/invfun.cmo contrib/funind/indfun.cmo \
-  contrib/funind/merge.cmo contrib/funind/g_indfun.cmo
-
-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
-
-CCCMO:=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \
-  contrib/cc/g_congruence.cmo 
-
-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 \
-  contrib/subtac/subtac_obligations.cmo contrib/subtac/subtac_cases.cmo \
-  contrib/subtac/subtac_pretyping_F.cmo contrib/subtac/subtac_pretyping.cmo \
-  contrib/subtac/subtac_command.cmo contrib/subtac/subtac_classes.cmo \
-  contrib/subtac/subtac.cmo contrib/subtac/g_subtac.cmo \
-  contrib/subtac/equations.cmo
-
-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) $(XMLCMO) \
-	$(CCCMO)  $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \
-	$(FUNINDCMO)
+CONFIG:=config/coq_config.cmo
 
-CMA:=$(CLIBS) $(CAMLP4OBJS)
-CMXA:=$(CMA:.cma=.cmxa)
+BYTERUN:=$(addprefix kernel/byterun/, \
+  coq_fix_code.o coq_memory.o coq_values.o coq_interp.o )
 
 # LINK ORDER:
 # Beware that highparsing.cma should appear before hightactics.cma
 # respecting this order is useful for developers that want to load or link
 # the libraries directly
 
-LINKCMO:=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \
+CORECMA:=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 contrib/contrib.cma
-LINKCMOCMXA:=$(LINKCMO:.cma=.cmxa)
-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)
-
-COQIDECMO:=ide/utils/okey.cmo ide/utils/config_file.cmo \
-	  ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \
-	  ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \
-	  ide/utils/configwin.cmo \
-	  ide/utils/editable_cells.cmo ide/config_parser.cmo \
-	  ide/config_lexer.cmo ide/utf8_convert.cmo ide/preferences.cmo \
-	  ide/ideutils.cmo ide/blaster_window.cmo ide/undo.cmo \
-	  ide/find_phrase.cmo \
-          ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo \
-	  ide/coq_tactics.cmo  ide/command_windows.cmo ide/coqide.cmo
-
-COQIDECMX:=$(COQIDECMO:.cmo=.cmx)
-
-COQENVCMO:=$(CONFIG) lib/pp_control.cmo lib/pp.cmo  lib/compat.cmo lib/flags.cmo \
-	lib/util.cmo lib/system.cmo lib/envars.cmo
+        parsing/highparsing.cma tactics/hightactics.cma 
+
+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/ring/ring_plugin.cma
+NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma
+NSATZCMA:=plugins/nsatz/nsatz_plugin.cma
+DPCMA:=plugins/dp/dp_plugin.cma
+FIELDCMA:=plugins/field/field_plugin.cma
+XMLCMA:=plugins/xml/xml_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
+SUBTACCMA:=plugins/subtac/subtac_plugin.cma
+RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma
+NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma
+OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
+        z_syntax_plugin.cma \
+        numbers_syntax_plugin.cma \
+        r_syntax_plugin.cma \
+	ascii_syntax_plugin.cma \
+        string_syntax_plugin.cma )
+
+PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \
+        $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \
+        $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
+        $(CCCMA)  $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \
+        $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA)
+
+ifneq ($(HASNATDYNLINK),false)
+ STATICPLUGINS:=
+ INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
+	$(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA)
+ INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
+ PLUGINS:=$(PLUGINSCMA)
+ PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
+else
+ STATICPLUGINS:=$(PLUGINSCMA)
+ INITPLUGINS:=
+ INITPLUGINSOPT:=
+ PLUGINS:=
+ PLUGINSOPT:=
+endif
 
-COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo 
-COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx)
+ifeq ($(BEST),opt)
+  INITPLUGINSBEST:=$(INITPLUGINSOPT)
+else
+  INITPLUGINSBEST:=$(INITPLUGINS)
+endif
 
-COQCCMO:=$(COQENVCMO) $(REVISIONCMO) toplevel/usage.cmo scripts/coqc.cmo
-COQCCMX:=$(COQCCMO:.cmo=.cmx)
+CMA:=$(CLIBS) $(CAMLP4OBJS)
+CMXA:=$(CMA:.cma=.cmxa)
 
-INTERFACE:=\
-  contrib/interface/vtp.cmo contrib/interface/xlate.cmo \
-  contrib/interface/paths.cmo contrib/interface/translate.cmo \
-  contrib/interface/pbp.cmo \
-  contrib/interface/dad.cmo \
-  contrib/interface/history.cmo \
-  contrib/interface/name_to_ast.cmo contrib/interface/debug_tac.cmo \
-  contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo \
-  contrib/interface/blast.cmo contrib/interface/depends.cmo \
-  contrib/interface/centaur.cmo
+LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS)
+LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
-INTERFACECMX:=$(INTERFACE:.cmo=.cmx)
+IDECMA:=ide/ide.cma
 
-PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité...
-PARSERREQUIRESCMX:=$(LINKCMX)
+# modules known by the toplevel of Coq
 
-ifeq ($(BEST),opt)
-  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/coq-parser$(EXE) bin/coq-parser.opt$(EXE)
-else
-  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
-endif
+OBJSMOD:=Coq_config \
+ $(foreach lib,$(CORECMA),$(shell cat $(lib:.cma=.mllib)))
 
-PARSERCODE:=contrib/interface/line_parser.cmo contrib/interface/vtp.cmo \
-           contrib/interface/xlate.cmo contrib/interface/parse.cmo
-PARSERCMO:=$(PARSERREQUIRES) $(PARSERCODE)
-PARSERCMX:= $(PARSERREQUIRESCMX) $(PARSERCODE:.cmo=.cmx)
+IDEMOD:=$(shell cat ide/ide.mllib)
 
-INTERFACERC:= contrib/interface/vernacrc
+# coqmktop, coqc
+
+COQENVCMO:=$(CONFIG) \
+  lib/pp_control.cmo lib/pp.cmo  lib/compat.cmo lib/flags.cmo \
+  lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/system.cmo \
+  lib/envars.cmo
+
+COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo 
+COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx)
+
+COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo
+COQCCMX:=$(COQCCMO:.cmo=.cmx)
+
+## Misc
+
+CSDPCERTCMO:=$(addprefix plugins/micromega/, \
+  mutils.cmo 	micromega.cmo 	mfourier.cmo 	certificate.cmo \
+  sos_types.cmo sos_lib.cmo sos.cmo 	csdpcert.cmo )
 
-CSDPCERTCMO:= contrib/micromega/mutils.cmo contrib/micromega/micromega.cmo \
-              contrib/micromega/vector.cmo contrib/micromega/mfourier.cmo \
-              contrib/micromega/certificate.cmo \
-              contrib/micromega/sos.cmo contrib/micromega/csdpcert.cmo
 CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx)
 
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
 
-COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep.cmo
+COQDEPBOOTML:=tools/coqdep_lexer.ml tools/coqdep_common.ml tools/coqdep_boot.ml
+COQDEPML:=tools/coqdep_lexer.ml tools/coqdep_common.ml tools/coqdep.ml
+
+COQDEPCMO:=$(COQENVCMO) $(COQDEPML:.ml=.cmo)
 COQDEPCMX:=$(COQDEPCMO:.cmo=.cmx)
 
 GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo
 GALLINACMX:=$(GALLINACMO:.cmo=.cmx)
 
-COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
-	tools/coqdoc/index.cmo tools/coqdoc/output.cmo \
-	tools/coqdoc/pretty.cmo tools/coqdoc/main.cmo
+COQDOCCMO:=$(CONFIG) $(addprefix tools/coqdoc/, \
+  cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
 COQDOCCMX:=$(COQDOCCMO:.cmo=.cmx)
 
-# checker
-
-MCHECKER:=\
-  config/coq_config.cmo \
-  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo \
-  lib/flags.cmo lib/util.cmo lib/option.cmo lib/hashcons.cmo \
-  lib/system.cmo lib/envars.cmo \
-  lib/predicate.cmo lib/rtree.cmo \
-  kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo \
-  checker/validate.cmo \
-  checker/term.cmo \
-  checker/declarations.cmo checker/environ.cmo \
-  checker/closure.cmo checker/reduction.cmo \
-  checker/type_errors.cmo \
-  checker/modops.cmo \
-  checker/inductive.cmo checker/typeops.cmo \
-  checker/indtypes.cmo checker/subtyping.cmo checker/mod_checking.cmo \
-  checker/safe_typing.cmo checker/check.cmo \
-  checker/check_stat.cmo checker/checker.cmo
-
 # grammar modules with camlp4
 
-GRAMMARNEEDEDCMO:=\
-  lib/profile.cmo lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
-  lib/util.cmo lib/bigint.cmo lib/dyn.cmo lib/hashcons.cmo lib/predicate.cmo \
-  lib/rtree.cmo lib/option.cmo \
-  kernel/names.cmo kernel/univ.cmo \
-  kernel/esubst.cmo kernel/term.cmo kernel/mod_subst.cmo kernel/sign.cmo \
-  kernel/cbytecodes.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo \
-  kernel/declarations.cmo \
-  kernel/retroknowledge.cmo kernel/pre_env.cmo \
-  kernel/cbytegen.cmo kernel/conv_oracle.cmo kernel/environ.cmo \
-  kernel/closure.cmo kernel/reduction.cmo kernel/type_errors.cmo\
-  kernel/entries.cmo \
-  kernel/modops.cmo \
-  kernel/inductive.cmo kernel/typeops.cmo \
-  kernel/indtypes.cmo kernel/cooking.cmo kernel/term_typing.cmo \
-  kernel/subtyping.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo \
-  library/nameops.cmo library/libnames.cmo library/summary.cmo \
-  library/nametab.cmo library/libobject.cmo library/lib.cmo \
-  library/goptions.cmo library/decl_kinds.cmo library/global.cmo \
-  pretyping/termops.cmo pretyping/evd.cmo pretyping/reductionops.cmo \
-  pretyping/inductiveops.cmo pretyping/rawterm.cmo pretyping/detyping.cmo \
-  pretyping/pattern.cmo \
-  interp/topconstr.cmo interp/genarg.cmo interp/ppextend.cmo \
-  proofs/tacexpr.cmo \
-  parsing/lexer.cmo parsing/extend.cmo \
-  toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_util.cmo \
-  parsing/q_coqast.cmo 
-
-CAMLP4EXTENSIONSCMO:=\
-  parsing/argextend.cmo parsing/tacextend.cmo parsing/vernacextend.cmo 
-
-GRAMMARSCMO:=\
-  parsing/g_prim.cmo parsing/g_tactic.cmo \
-  parsing/g_ltac.cmo parsing/g_constr.cmo
-
-GRAMMARCMO:=config/coq_config.cmo $(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO)
-
 GRAMMARCMA:=parsing/grammar.cma
 
 GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \
@@ -480,412 +272,143 @@ GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \
   parsing/lexer.ml4 parsing/q_coqast.ml4
 
 STAGE1_ML4:=$(GRAMMARML4) parsing/q_constr.ml4
-STAGE1_CMO:=$(GRAMMARCMO) parsing/q_constr.cmo
 STAGE1:=parsing/grammar.cma parsing/q_constr.cmo
 
-PRINTERSCMO:=\
-  config/coq_config.cmo lib/lib.cma \
-  kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo	\
-  kernel/mod_subst.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo	\
-  kernel/sign.cmo kernel/declarations.cmo kernel/retroknowledge.cmo \
-  kernel/pre_env.cmo \
-  kernel/retroknowledge.cmo kernel/pre_env.cmo \
-  kernel/cbytecodes.cmo kernel/cbytegen.cmo kernel/environ.cmo \
-  kernel/conv_oracle.cmo kernel/closure.cmo kernel/reduction.cmo	\
-  kernel/modops.cmo kernel/type_errors.cmo kernel/inductive.cmo		\
-  kernel/typeops.cmo kernel/subtyping.cmo kernel/indtypes.cmo		\
-  kernel/cooking.cmo 		\
-  kernel/term_typing.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo	\
-  library/summary.cmo library/global.cmo library/nameops.cmo		\
-  library/libnames.cmo library/nametab.cmo library/libobject.cmo	\
-  library/lib.cmo library/goptions.cmo library/decls.cmo library/heads.cmo \
-  pretyping/termops.cmo pretyping/evd.cmo pretyping/rawterm.cmo \
-  pretyping/reductionops.cmo pretyping/inductiveops.cmo			    \
-  pretyping/retyping.cmo pretyping/cbv.cmo				    \
-  pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \
-  pretyping/evarutil.cmo pretyping/evarconv.cmo pretyping/tacred.cmo \
-  pretyping/classops.cmo pretyping/typeclasses_errors.cmo pretyping/typeclasses.cmo \
-  pretyping/detyping.cmo pretyping/indrec.cmo pretyping/coercion.cmo \
-  pretyping/unification.cmo pretyping/cases.cmo \
-  pretyping/pretyping.cmo pretyping/clenv.cmo pretyping/pattern.cmo \
-  parsing/lexer.cmo interp/ppextend.cmo interp/genarg.cmo \
-  interp/topconstr.cmo interp/notation.cmo  interp/dumpglob.cmo interp/reserve.cmo		\
-  library/impargs.cmo interp/constrextern.cmo \
-  interp/syntax_def.cmo interp/implicit_quantifiers.cmo \
-  interp/constrintern.cmo proofs/proof_trees.cmo proofs/tacexpr.cmo \
-  proofs/proof_type.cmo proofs/logic.cmo proofs/refiner.cmo \
-  proofs/evar_refiner.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo \
-  proofs/decl_mode.cmo \
-  parsing/ppconstr.cmo parsing/extend.cmo parsing/pcoq.cmo \
-  parsing/printer.cmo parsing/pptactic.cmo \
-  parsing/ppdecl_proof.cmo \
-  parsing/tactic_printer.cmo \
-  parsing/egrammar.cmo toplevel/himsg.cmo toplevel/cerrors.cmo \
-  toplevel/vernacexpr.cmo toplevel/vernacinterp.cmo \
-  dev/top_printers.cmo
 
 ###########################################################################
 # vo files
 ###########################################################################
 
-## Theories
-
-INITVO:=$(addprefix theories/Init/, \
- Notations.vo	Datatypes.vo	Peano.vo	Logic.vo	\
- Specif.vo	Logic_Type.vo  	Wf.vo		Tactics.vo	\
- Prelude.vo )
-
-LOGICVO:=$(addprefix theories/Logic/, \
- Hurkens.vo               ProofIrrelevance.vo      Classical.vo 	\
- Classical_Type.vo        Classical_Pred_Set.vo    Eqdep.vo     	\
- Classical_Prop.vo        Classical_Pred_Type.vo   ClassicalFacts.vo 	\
- ChoiceFacts.vo           Berardi.vo               Eqdep_dec.vo 	\
- Decidable.vo             JMeq.vo                  ClassicalChoice.vo 	\
- ClassicalDescription.vo  RelationalChoice.vo      Diaconescu.vo 	\
- EqdepFacts.vo            ProofIrrelevanceFacts.vo ClassicalEpsilon.vo 	\
- ClassicalUniqueChoice.vo DecidableType.vo         DecidableTypeEx.vo 	\
- Epsilon.vo               ConstructiveEpsilon.vo   Description.vo 	\
- IndefiniteDescription.vo SetIsType.vo             FunctionalExtensionality.vo )
-
-ARITHVO:=$(addprefix theories/Arith/, \
- Arith.vo	Gt.vo          	Between.vo	Le.vo         	\
- Compare.vo	Lt.vo          	Compare_dec.vo	Min.vo        	\
- Div2.vo	Minus.vo       	Mult.vo		Even.vo       	\
- EqNat.vo	Peano_dec.vo   	Euclid.vo	Plus.vo		\
- Wf_nat.vo  	Max.vo		Bool_nat.vo	Factorial.vo	\
- Arith_base.vo )
-
-SORTINGVO:=$(addprefix theories/Sorting/, \
- Heap.vo 	Permutation.vo	Sorting.vo 	PermutSetoid.vo \
- PermutEq.vo )
-
-BOOLVO:=$(addprefix theories/Bool/, \
- Bool.vo  	IfProp.vo    	Zerob.vo 	DecBool.vo 	\
- Sumbool.vo 	BoolEq.vo    	Bvector.vo )
-
-NARITHVO:=$(addprefix theories/NArith/, \
- BinPos.vo	Pnat.vo      	BinNat.vo   	NArith.vo 	\
- Nnat.vo	Ndigits.vo   	Ndec.vo	 	Ndist.vo 	)
-
-ZARITHVO:=$(addprefix theories/ZArith/, \
- BinInt.vo      Wf_Z.vo 	ZArith.vo      	ZArith_dec.vo 	\
- auxiliary.vo   Zmisc.vo 	Zcompare.vo    	Znat.vo 	\
- Zorder.vo      Zabs.vo 	Zmin.vo        	Zmax.vo 	\
- Zminmax.vo     Zeven.vo 	Zhints.vo	Zlogarithm.vo 	\
- Zpower.vo 	Zcomplements.vo Zdiv.vo		Zsqrt.vo 	\
- Zwf.vo		ZArith_base.vo 	Zbool.vo	Zbinary.vo 	\
- Znumtheory.vo  Int.vo 		Zpow_def.vo	Zpow_facts.vo 	\
- ZOdiv_def.vo   ZOdiv.vo 	Zgcd_alt.vo )
-
-QARITHVO:=$(addprefix theories/QArith/, \
- QArith_base.vo Qreduction.vo 	Qring.vo	Qreals.vo 	\
- QArith.vo	Qcanon.vo 	Qfield.vo	Qpower.vo 	\
- Qabs.vo        Qround.vo )
-
-LISTSVO:=$(addprefix theories/Lists/, \
- MonoList.vo  	ListSet.vo   	Streams.vo 	StreamMemo.vo  \
- TheoryList.vo	List.vo 	SetoidList.vo   ListTactics.vo )
-
-STRINGSVO:=$(addprefix theories/Strings/, \
- Ascii.vo      	String.vo )
-
-SETSVO:=$(addprefix theories/Sets/, \
- Classical_sets.vo    	Permut.vo \
- Constructive_sets.vo 	Powerset.vo \
- Cpo.vo               	Powerset_Classical_facts.vo \
- Ensembles.vo         	Powerset_facts.vo \
- Finite_sets.vo       	Relations_1.vo \
- Finite_sets_facts.vo 	Relations_1_facts.vo \
- Image.vo             	Relations_2.vo \
- Infinite_sets.vo     	Relations_2_facts.vo \
- Integers.vo          	Relations_3.vo \
- Multiset.vo          	Relations_3_facts.vo \
- Partial_Order.vo     	Uniset.vo )
-
-FSETSBASEVO:=$(addprefix theories/FSets/, \
- OrderedType.vo		OrderedTypeEx.vo	OrderedTypeAlt.vo	\
- FSetInterface.vo	FSetList.vo 		FSetBridge.vo        	\
- FSetFacts.vo 		FSetProperties.vo	FSetEqProperties.vo 	\
- FSetWeakList.vo 	FSetAVL.vo           	FSetDecide.vo 		\
- FSets.vo \
- FMapInterface.vo       FMapList.vo		FMapFacts.vo 		\
- FMapWeakList.vo      	FMapPositive.vo		FSetToFiniteSet.vo   	\
- FMaps.vo )            
-
-FSETS_basic:=
-
-FSETS_all:=$(addprefix theories/FSets/, \
- FSetFullAVL.vo 	FMapAVL.vo 		FMapFullAVL.vo )
-
-FSETSVO:=$(FSETSBASEVO) $(FSETS_$(FSETS))
-
-ALLFSETS:=$(FSETSBASEVO) $(FSETS_all)
-
-RELATIONSVO:=$(addprefix theories/Relations/, \
- Operators_Properties.vo	Relation_Definitions.vo \
- Relation_Operators.vo 		Relations.vo )
-
-WELLFOUNDEDVO:=$(addprefix theories/Wellfounded/, \
- Disjoint_Union.vo 	Inclusion.vo 	Inverse_Image.vo \
- Transitive_Closure.vo  Union.vo 	Wellfounded.vo 	 \
- Well_Ordering.vo 	Lexicographic_Product.vo         \
- Lexicographic_Exponentiation.vo )
-
-REALSBASEVO:=$(addprefix theories/Reals/, \
- Rdefinitions.vo Raxioms.vo      RIneq.vo	DiscrR.vo \
- Rbase.vo 	 LegacyRfield.vo Rpow_def.vo )
-
-REALS_basic:= 
-
-REALS_all:=$(addprefix theories/Reals/, \
- R_Ifp.vo 	Rbasic_fun.vo	R_sqr.vo	SplitAbsolu.vo	\
- SplitRmult.vo	ArithProp.vo    Rfunctions.vo	Rseries.vo      \
- SeqProp.vo 	Rcomplete.vo    PartSum.vo	AltSeries.vo    \
- Binomial.vo	Rsigma.vo       Rprod.vo	Cauchy_prod.vo  \
- Alembert.vo	SeqSeries.vo    Rtrigo_fun.vo	Rtrigo_def.vo   \
- Rtrigo_alt.vo  Cos_rel.vo      Cos_plus.vo	Rtrigo.vo       \
- Rlimit.vo	Rderiv.vo       RList.vo	Ranalysis1.vo   \
- Ranalysis2.vo	Ranalysis3.vo   Rtopology.vo	MVT.vo          \
- PSeries_reg.vo Exp_prop.vo     Rtrigo_reg.vo	Rsqrt_def.vo    \
- R_sqrt.vo	Rtrigo_calc.vo  Rgeom.vo	Sqrt_reg.vo     \
- Ranalysis4.vo	Rpower.vo       Ranalysis.vo	NewtonInt.vo    \
- RiemannInt_SF.vo		RiemannInt.vo   Integration.vo 	\
- Rlogic.vo	Reals.vo )
-
-REALSVO:=$(REALSBASEVO) $(REALS_$(REALS))
-
-ALLREALS:=$(REALSBASEVO) $(REALS_all)
-
-NUMBERSCOMMONVO:=$(addprefix theories/Numbers/, \
- NaryFunctions.vo NumPrelude.vo BigNumPrelude.vo )
-
-CYCLICABSTRACTVO:=$(addprefix theories/Numbers/Cyclic/Abstract/, \
- CyclicAxioms.vo NZCyclic.vo )
-
-CYCLICINT31VO:=$(addprefix theories/Numbers/Cyclic/Int31/, \
- Int31.vo Cyclic31.vo )
-
-CYCLICDOUBLECYCLICVO:=$(addprefix theories/Numbers/Cyclic/DoubleCyclic/, \
- DoubleType.vo	DoubleBase.vo	DoubleAdd.vo	DoubleSub.vo	\
- DoubleMul.vo	DoubleDivn1.vo 	DoubleDiv.vo	DoubleSqrt.vo	\
- DoubleLift.vo 	DoubleCyclic.vo )
-
-CYCLICZMODULOVO := $(addprefix theories/Numbers/Cyclic/ZModulo/, \
- ZModulo.vo )
-
-CYCLICVO:=$(CYCLICABSTRACTVO) $(CYCLICINT31VO) $(CYCLICDOUBLECYCLICVO) \
- $(CYCLICZMODULOVO)
-
-NATINTVO:=$(addprefix theories/Numbers/NatInt/, \
- NZAxioms.vo	NZBase.vo	NZAdd.vo	NZMul.vo	\
- NZOrder.vo 	NZAddOrder.vo	NZMulOrder.vo )
-
-NATURALABSTRACTVO:=$(addprefix theories/Numbers/Natural/Abstract/, \
- NAxioms.vo 	NBase.vo 	NAdd.vo 	NMul.vo 	\
- NOrder.vo 	NAddOrder.vo	NMulOrder.vo 	NSub.vo	\
- NIso.vo )
-
-NATURALPEANOVO:=$(addprefix theories/Numbers/Natural/Peano/, \
- NPeano.vo )
-
-NATURALBINARYVO:=$(addprefix theories/Numbers/Natural/Binary/, \
- NBinDefs.vo 	NBinary.vo )
-
-NATURALSPECVIAZVO:=$(addprefix theories/Numbers/Natural/SpecViaZ/, \
- NSig.vo	NSigNAxioms.vo )
-
-NATURALBIGNVO:=$(addprefix theories/Numbers/Natural/BigN/, \
- Nbasic.vo 	NMake.vo 	BigN.vo )
-
-NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) \
- $(NATURALSPECVIAZVO) $(NATURALBIGNVO)
-
-INTEGERABSTRACTVO:=$(addprefix theories/Numbers/Integer/Abstract/, \
- ZAxioms.vo 	ZBase.vo 	ZAdd.vo 	ZMul.vo 	\
- ZLt.vo 	ZAddOrder.vo 	ZMulOrder.vo )
+## we now retrieve the names of .vo file to compile in */vo.itarget files
 
-INTEGERBINARYVO:=$(addprefix theories/Numbers/Integer/Binary/, \
- ZBinary.vo )
+cat_vo_itarget = $(addprefix $(1)/,$(shell cat $(1)/vo.itarget))
 
-INTEGERNATPAIRSVO:=$(addprefix theories/Numbers/Integer/NatPairs/, \
- ZNatPairs.vo )
-
-INTEGERSPECVIAZVO:=$(addprefix theories/Numbers/Integer/SpecViaZ/, \
- ZSig.vo	ZSigZAxioms.vo )
-
-INTEGERBIGZVO:=$(addprefix theories/Numbers/Integer/BigZ/, \
- ZMake.vo 	BigZ.vo )
-
-INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) \
- $(INTEGERSPECVIAZVO) $(INTEGERBIGZVO)
-
-RATIONALSPECVIAQVO:=$(addprefix theories/Numbers/Rational/SpecViaQ/, \
- QSig.vo )
-
-RATIONALBIGQVO:=$(addprefix theories/Numbers/Rational/BigQ/, \
- QMake.vo	BigQ.vo )
-
-RATIONALVO:=$(RATIONALSPECVIAQVO) $(RATIONALBIGQVO)
-
-NUMBERSVO:= $(NUMBERSCOMMONVO) $(NATURALVO) $(INTEGERVO) $(NATINTVO) $(CYCLICVO) $(RATIONALVO)
-
-SETOIDSVO:=$(addprefix theories/Setoids/, \
- Setoid.vo ) 
-
-UNICODEVO:=$(addprefix theories/Unicode/, \
- Utf8.vo )
-
-CLASSESVO:=$(addprefix theories/Classes/, \
- Init.vo	RelationClasses.vo	Morphisms.vo	Morphisms_Prop.vo \
- Morphisms_Relations.vo	Functions.vo 	Equivalence.vo  SetoidTactics.vo  \
- SetoidClass.vo 	SetoidAxioms.vo EquivDec.vo 	SetoidDec.vo )
+## Theories
 
-PROGRAMVO:=$(addprefix theories/Program/, \
- Tactics.vo 	Equality.vo 	Subset.vo	Utils.vo 	\
- Wf.vo 		Basics.vo	Combinators.vo	Syntax.vo 	Program.vo )
+INITVO:=$(call cat_vo_itarget, theories/Init)
+LOGICVO:=$(call cat_vo_itarget, theories/Logic)
+STRUCTURESVO:=$(call cat_vo_itarget, theories/Structures)
+ARITHVO:=$(call cat_vo_itarget, theories/Arith)
+SORTINGVO:=$(call cat_vo_itarget, theories/Sorting)
+BOOLVO:=$(call cat_vo_itarget, theories/Bool)
+NARITHVO:=$(call cat_vo_itarget, theories/NArith)
+ZARITHVO:=$(call cat_vo_itarget, theories/ZArith)
+QARITHVO:=$(call cat_vo_itarget, theories/QArith)
+LISTSVO:=$(call cat_vo_itarget, theories/Lists)
+STRINGSVO:=$(call cat_vo_itarget, theories/Strings)
+SETSVO:=$(call cat_vo_itarget, theories/Sets)
+FSETSVO:=$(call cat_vo_itarget, theories/FSets)
+MSETSVO:=$(call cat_vo_itarget, theories/MSets)
+RELATIONSVO:=$(call cat_vo_itarget, theories/Relations)
+WELLFOUNDEDVO:=$(call cat_vo_itarget, theories/Wellfounded)
+REALSVO:=$(call cat_vo_itarget, theories/Reals)
+NUMBERSVO:=$(call cat_vo_itarget, theories/Numbers)
+SETOIDSVO:=$(call cat_vo_itarget, theories/Setoids)
+UNICODEVO:=$(call cat_vo_itarget, theories/Unicode)
+CLASSESVO:=$(call cat_vo_itarget, theories/Classes)
+PROGRAMVO:=$(call cat_vo_itarget, theories/Program)
 
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
-  $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) \
+  $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(MSETSVO) \
   $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
-  $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO)
+  $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO)
 
 THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO)
 
-## Contribs
-
-OMEGAVO:=$(addprefix contrib/omega/, \
- PreOmega.vo	OmegaLemmas.vo 	Omega.vo )
-
-ROMEGAVO:=$(addprefix contrib/romega/, \
- ReflOmegaCore.vo 	ROmega.vo )
-
-MICROMEGAVO:=$(addprefix contrib/micromega/, \
-  CheckerMaker.vo       Refl.vo \
-  Env.vo                RingMicromega.vo \
-  EnvRing.vo            VarMap.vo \
-  OrderedRing.vo        ZCoeff.vo \
-  Psatz.vo	       ZMicromega.vo \
-  QMicromega.vo         RMicromega.vo \
-  Tauto.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.vo		Setoid_ring_theory.vo )
-
-FIELDVO:=$(addprefix contrib/field/, \
- LegacyField_Compl.vo   LegacyField_Theory.vo \
- LegacyField_Tactic.vo  LegacyField.vo )
-
-NEWRINGVO:=$(addprefix contrib/setoid_ring/, \
- BinList.vo   		Ring_theory.vo \
- Ring_polynom.vo	Ring_tac.vo \
- Ring_base.vo 		InitialRing.vo \
- Ring_equiv.vo 		Ring.vo \
- ArithRing.vo		NArithRing.vo \
- ZArithRing.vo		\
- Field_theory.vo	Field_tac.vo \
- Field.vo		RealField.vo )
-
-XMLVO:= 
-
-FOURIERVO:=$(addprefix contrib/fourier/, \
- Fourier_util.vo    	Fourier.vo )
-
-FUNINDVO:= 
-
-RECDEFVO:=$(addprefix contrib/funind/, \
- Recdef.vo )
-
+## Plugins
+
+OMEGAVO:=$(call cat_vo_itarget, plugins/omega)
+ROMEGAVO:=$(call cat_vo_itarget, plugins/romega)
+MICROMEGAVO:=$(call cat_vo_itarget, plugins/micromega)
+QUOTEVO:=$(call cat_vo_itarget, plugins/quote)
+RINGVO:=$(call cat_vo_itarget, plugins/ring)
+FIELDVO:=$(call cat_vo_itarget, plugins/field)
+NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring)
+NSATZVO:=$(call cat_vo_itarget, plugins/nsatz)
+FOURIERVO:=$(call cat_vo_itarget, plugins/fourier)
+FUNINDVO:=$(call cat_vo_itarget, plugins/funind)
+DPVO:=$(call cat_vo_itarget, plugins/dp)
+RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto)
+EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
+XMLVO:=
 CCVO:=
 
-DPVO:=$(addprefix contrib/dp/, \
- Dp.vo )
-
-RTAUTOVO:=$(addprefix contrib/rtauto/, \
- Bintree.vo	Rtauto.vo )
-
-CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
+PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
 	    $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
-	    $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO)
+	    $(RTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \
+            $(NSATZVO) $(EXTRACTIONVO)
 
-ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
+ALLVO:= $(THEORIESVO) $(PLUGINSVO)
 VFILES:= $(ALLVO:.vo=.v)
 
 # convert a (stdlib) filename into a module name:
-# remove .vo, replace theories and contrib by Coq, and replace slashes by dots
-vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst contrib/%,Coq.%,$(1:.vo=))))
+# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
+vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
 
 ALLMODS:=$(call vo_to_mod,$(ALLVO))
 
-LIBFILES:=$(THEORIESVO) $(CONTRIBVO)
+LIBFILES:=$(THEORIESVO) $(PLUGINSVO)
 LIBFILESLIGHT:=$(THEORIESLIGHTVO)
 
-## Specials
-
-INTERFACEVO:=
 
+###########################################################################
+# Miscellaneous
+###########################################################################
 
 MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 	man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
 	man/coqwc.1 man/coqdoc.1 man/coqide.1 \
-	man/coq_makefile.1 man/coqmktop.1
+	man/coq_makefile.1 man/coqmktop.1 man/coqchk.1
 
-PCOQMANPAGES:=man/coq-interface.1 man/coq-parser.1
+DATE=$(shell LANG=C date +"%B %Y")
 
-RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \
-  parsing/pptactic.ml 
+SOURCEDOCDIR=dev/source-doc
 
+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
 
-#########################################################
-# .mli files by directory (used for dependencies graphs #
-#########################################################
+### Targets forwarded by Makefile to a specific stage:
 
-# We use wildcard to get rid of .cmo that do not have a .mli 
-KERNELMLI:=$(wildcard $(KERNEL:.cmo=.mli))
-INTERPMLI:=$(wildcard $(INTERP:.cmo=.mli))
-PRETYPINGMLI:=$(wildcard $(PRETYPING:.cmo=.mli))
-TOPLEVELMLI:=$(wildcard $(TOPLEVEL:.cmo=.mli))
-PROOFSMLI:=$(wildcard $(PROOFS:.cmo=.mli))
-LIBRARYMLI:=$(wildcard $(LIBRARY:.cmo=.mli))
-PARSINGMLI:=$(wildcard $(PARSING:.cmo=.mli) $(HIGHPARSING:.cmo=.mli))
-TACTICSMLI:=$(wildcard $(TACTICS:.cmo=.mli) $(HIGHTACTICS:.cmo=.mli))
-COQMLI:=$(KERNELMLI) $(INTERPMLI) $(PRETYPINGMLI) $(TOPLEVELMLI) $(PROOFSMLI) \
-	$(LIBRARYMLI) $(PARSINGMLI) $(TACTICSMLI)
+## Enumeration of targets that require being done at stage1
 
+STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
+  $(GENFILES) \
+  source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
+  $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
 
-###########################################################################
-# Miscellaneous
-###########################################################################
+ifdef CM_STAGE1
+ STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
+endif
 
-DATE=$(shell LANG=C date +"%B %Y")
+## Enumeration of targets that require being done at stage2
 
-SOURCEDOCDIR=dev/source-doc
+VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
+  fsets relations wellfounded ints reals \
+  setoids sorting natural integer rational numbers noreal \
+  omega micromega ring setoid_ring dp xml extraction field fourier \
+  funind cc subtac rtauto
+
+DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq \
+  rectutorial refman-quick refman-nodep stdlib-nodep \
+  install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-url \
+  ide/index_urls.txt
+
+DOC_TARGET_PATTERNS:=%.dvi %.ps %.eps %.pdf %.html %.v.tex %.hva
 
-## Targets forwarded by Makefile to a specific stage
-STAGE1_TARGETS:= $(STAGE1) \
-  $(filter-out parsing/q_constr.cmo,$(STAGE1_CMO)) \
-  $(STAGE1_CMO:.cmo=.cmi) $(STAGE1_CMO:.cmo=.cmx) $(GENFILES) \
-  source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
-  $(STAGE1_ML4:.ml4=.ml4-preprocessed)
 STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
   interp parsing pretyping highparsing toplevel hightactics \
   coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \
-  pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \
-  printers debug initplugins
-VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
-  fsets allfsets relations wellfounded ints reals allreals \
-  setoids sorting natural integer rational numbers noreal \
-  omega micromega ring setoid_ring dp xml extraction field fourier \
-  funind cc programs subtac rtauto
-DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial refman-quick refman-nodep stdlib-nodep
-STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \
-  coqlight states pcoq-files check init theories theories-light contrib \
-  $(DOC_TARGETS) $(VO_TARGETS) validate
+  $(CSDPCERT) coqbinaries $(TOOLS) tools \
+  printers debug initplugins plugins \
+  world install coqide coqide-files coq coqlib \
+  coqlight states check init theories theories-light \
+  $(DOC_TARGETS) $(VO_TARGETS) validate \
+  %.vo %.glob states/% install-% %.ml4-preprocessed \
+  $(DOC_TARGET_PATTERNS)
+
+ifndef CM_STAGE1
+ STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS)
+endif
 
 
 # For emacs: