Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 890 insertions, 0 deletions

diff --git a/Makefile.common b/Makefile.common
new file mode 100644
index 00000000..509ceedb
--- /dev/null
+++ b/Makefile.common
@@ -0,0 +1,890 @@
+#######################################################################
+#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
+# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
+#   \VV/  #############################################################
+#    //   #      This file is distributed under the terms of the      #
+#         #       GNU Lesser General Public License Version 2.1       #
+#######################################################################
+
+-include config/Makefile
+
+###########################################################################
+# Executables
+###########################################################################
+
+COQMKTOPBYTE:=bin/coqmktop.byte$(EXE)
+COQMKTOPOPT:=bin/coqmktop.opt$(EXE)
+BESTCOQMKTOP:=bin/coqmktop.$(BEST)$(EXE)
+COQMKTOP:=bin/coqmktop$(EXE) 
+COQCBYTE:=bin/coqc.byte$(EXE)
+COQCOPT:=bin/coqc.opt$(EXE)
+BESTCOQC:=bin/coqc.$(BEST)$(EXE)
+COQC:=bin/coqc$(EXE)
+COQTOPBYTE:=bin/coqtop.byte$(EXE)
+COQTOPOPT:=bin/coqtop.opt$(EXE)
+BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE)
+COQTOP:=bin/coqtop$(EXE)
+CHICKENBYTE:=bin/coqchk.byte$(EXE)
+CHICKENOPT:=bin/coqchk.opt$(EXE)
+BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
+CHICKEN:=bin/coqchk$(EXE)
+
+INSTALLBIN:=install
+INSTALLLIB:=install -m 644 
+MKDIR:=install -d
+
+COQIDEBYTE:=bin/coqide.byte$(EXE)
+COQIDEOPT:=bin/coqide.opt$(EXE)
+COQIDE:=bin/coqide$(EXE)
+
+ifeq ($(BEST),opt)
+COQBINARIES:= $(COQMKTOP) $(COQC) \
+  $(COQTOPBYTE) $(COQTOPOPT) $(COQTOP) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN)
+else
+COQBINARIES:= $(COQMKTOP) $(COQC) \
+  $(COQTOPBYTE)              $(COQTOP) $(CHICKENBYTE)               $(CHICKEN)
+endif
+OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
+
+MINICOQ:=bin/minicoq$(EXE)
+
+CSDPCERT:=bin/csdpcert$(EXE)
+
+###########################################################################
+# tools
+###########################################################################
+
+COQDEP:=bin/coqdep$(EXE)
+COQMAKEFILE:=bin/coq_makefile$(EXE)
+GALLINA:=bin/gallina$(EXE)
+COQTEX:=bin/coq-tex$(EXE)
+COQWC:=bin/coqwc$(EXE)
+COQDOC:=bin/coqdoc$(EXE)
+
+TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) \
+      $(COQWC) $(COQDOC)
+
+###########################################################################
+# Documentation
+###########################################################################
+
+LATEX:=latex
+BIBTEX:=bibtex -min-crossrefs=10
+MAKEINDEX:=makeindex
+PDFLATEX:=pdflatex
+HEVEA:=hevea
+HEVEAOPTS:=-fix -exec xxdate.exe
+HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
+export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB):
+COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOP) -v -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/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) \
+
+REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps
+
+REFMANFILES:=$(REFMANTEXFILES) $(COMMON) $(REFMANEPSFILES) doc/refman/biblio.bib
+
+REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
+
+
+
+###########################################################################
+# Object and Source files 
+###########################################################################
+
+LIBCOQRUN:=kernel/byterun/libcoqrun.a
+
+CLIBS:=unix.cma
+
+CAMLP4OBJS:=gramlib.cma
+
+CONFIG:=\
+  config/coq_config.cmo
+
+LIBREP:=\
+  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bigint.cmo \
+  lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/flags.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/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/evar_tactics.cmo \
+  tactics/hiddentac.cmo tactics/elim.cmo \
+  tactics/dhyp.cmo tactics/auto.cmo \
+  toplevel/ind_tables.cmo \
+  tactics/setoid_replace.cmo tactics/equality.cmo \
+  tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \
+  tactics/tacinterp.cmo tactics/autorewrite.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 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
+
+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
+
+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
+
+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)
+
+CMA:=$(CLIBS) $(CAMLP4OBJS)
+CMXA:=$(CMA:.cma=.cmxa)
+
+# 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 \
+        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)
+
+COQMKTOPCMO:=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo 
+
+COQMKTOPCMX:=config/coq_config.cmx scripts/tolink.cmx scripts/coqmktop.cmx 
+COQCCMO:=$(CONFIG) toplevel/usage.cmo scripts/coqc.cmo
+COQCCMX:=config/coq_config.cmx toplevel/usage.cmx scripts/coqc.cmx
+
+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
+
+INTERFACECMX:=$(INTERFACE:.cmo=.cmx)
+
+PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité...
+PARSERREQUIRESCMX:=$(LINKCMX)
+
+ifeq ($(BEST),opt)
+  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/parser$(EXE) bin/parser.opt$(EXE)
+else
+  COQINTERFACE:=bin/coq-interface$(EXE) bin/parser$(EXE)
+endif
+
+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)
+
+INTERFACERC:= contrib/interface/vernacrc
+
+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:=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo
+GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo
+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
+
+
+# checker
+
+MCHECKER:=\
+  config/coq_config.cmo \
+  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo \
+  lib/util.cmo lib/option.cmo lib/hashcons.cmo \
+  lib/system.cmo lib/flags.cmo \
+  lib/predicate.cmo lib/rtree.cmo \
+  kernel/names.cmo kernel/univ.cmo \
+  kernel/esubst.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/validate.cmo \
+  checker/safe_typing.cmo checker/check.cmo \
+  checker/check_stat.cmo checker/checker.cmo
+
+# minicoq
+
+MINICOQCMO:=$(CONFIG) $(LIBREP) $(KERNEL) \
+	   parsing/lexer.cmo parsing/g_minicoq.cmo \
+	   toplevel/fhimsg.cmo toplevel/minicoq.cmo
+
+# grammar modules with camlp4
+
+GRAMMARNEEDEDCMO:=\
+  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bigint.cmo \
+  lib/dyn.cmo lib/flags.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:=$(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO)
+
+GRAMMARCMA:=parsing/grammar.cma
+
+GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \
+  parsing/argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4 \
+  parsing/g_prim.ml4 parsing/g_tactic.ml4 \
+  parsing/g_ltac.ml4 parsing/g_constr.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/reserve.cmo		\
+  library/impargs.cmo interp/constrextern.cmo \
+  interp/syntax_def.cmo interp/implicit_quantifiers.cmo  interp/constrintern.cmo \
+  proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \
+  proofs/tacexpr.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 )
+
+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/, \
+ Newman.vo 		Operators_Properties.vo	Relation_Definitions.vo \
+ Relation_Operators.vo 	Relations.vo 		Rstar.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 )
+
+INTEGERBINARYVO:=$(addprefix theories/Numbers/Integer/Binary/, \
+ ZBinary.vo )
+
+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_base.vo	QpMake.vo	QvMake.vo	Q0Make.vo 	\
+ QifMake.vo 	QbiMake.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 )
+
+PROGRAMVO:=$(addprefix theories/Program/, \
+ Tactics.vo 	Equality.vo 	Subset.vo	Utils.vo 	\
+ Wf.vo 		Basics.vo	FunctionalExtensionality.vo 	\
+ Combinators.vo	Syntax.vo 	Program.vo )
+
+THEORIESVO:=\
+  $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
+  $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) \
+  $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
+  $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO)
+
+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 \
+  Micromegatac.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 )
+
+JPROVERVO:= 
+
+CCVO:=
+
+DPVO:=$(addprefix contrib/dp/, \
+ Dp.vo )
+
+RTAUTOVO:=$(addprefix contrib/rtauto/, \
+ Bintree.vo	Rtauto.vo )
+
+CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
+	    $(XMLVO) $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) \
+	    $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO)
+
+ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
+VFILES:= $(ALLVO:.vo=.v)
+
+LIBFILES:=$(THEORIESVO) $(CONTRIBVO)
+LIBFILESLIGHT:=$(THEORIESLIGHTVO)
+
+## Specials
+
+INTERFACEVO:=
+
+
+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/coq_makefile.1 man/coqmktop.1
+
+PCOQMANPAGES:=man/coq-interface.1 man/parser.1
+
+RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \
+  parsing/pptactic.ml 
+
+
+#########################################################
+# .mli files by directory (used for dependencies graphs #
+#########################################################
+
+# 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)
+
+
+###########################################################################
+# Miscellaneous
+###########################################################################
+
+SOURCEDOCDIR=dev/source-doc
+
+## 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 $(MINICOQ) debug
+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 jprover \
+  funind cc programs subtac rtauto
+DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial
+STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \
+  coqlight states pcoq-files check init theories theories-light contrib \
+  $(DOC_TARGETS) $(VO_TARGETS)
+
+
+# For emacs: 
+# Local Variables: 
+# mode: makefile 
+# End: