Makefile.build split in many smaller files : Makefile.{ide,checker,dev,install}

 General idea : Makefile.build was far too big to be easy to grasp or
 maintain, with information scattered everywhere. Let's try to tidy that!
 Normally, this commit is transparent for the user. We simply regroup
 some parts of Makefile.build in several new dedicated files:
  - Makefile.ide
  - Makefile.checker
  - Makefile.dev (for printers, revision, extra partial targets, otags)
  - Makefile.install
 These new files are "included" at the start of Makefile.build, to provide
 the same behavior as before, but with a Makefile.build shrinked by 50%
 (to approx 600 lines). Makefile.build now handles in priority the build
 of coqtop, minor tools, theories and plugins.

 Note: this is *not* a separate build system for coqchk nor coqide,
 even if this can be seen as a first step in this direction (won't be easy
 anyway to continue, due to the sharing of various stuff in lib and more).
 In particular Makefile.{coqchk,ide} may rely here and there on some generic
 rules left in Mafefile.build. Conversely, be sure to prefix rules in
 Makefile.{coqchk,ide} by checker/... or ide/... in order to avoid
 interferences with generic rules.

 Makefile.common is still there, but quite simplified. For instance,
 some variables that were used only once (e.g. lists of cmo files to link
 in the various tools) are now defined in Makefile.build, directly
 where they're needed. THEORIESVO and PLUGINSVO are made directly out of
 the theories/*/vo.itarget and plugins/*/vo.itarget files, no long manual
 list of subdirs anymore. Specific sub-targets such as 'reals' still
 exist, but in Makefile.dev, and they aren't mandatory.

 Makefile.doc is augmented by the rules building the documentation of
 the sources via ocamldoc.

 This classification attempt could probably be improved. For instance,
 the install rules for coqide are currently in Makefile.ide, but could
 also go in Makefile.install. Note that I've removed install-library-light
 which was broken anyway (arith isn't self-contained anymore).

8 files changed, 1066 insertions, 976 deletions

diff --git a/Makefile b/Makefile
index c8bfe8e01..aeb54fba8 100644
--- a/Makefile
+++ b/Makefile
@@ -153,7 +153,7 @@ noconfig:
 
 # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
 
-Makefile Makefile.build Makefile.common config/Makefile : ;
+Makefile $(wildcard Makefile.*) config/Makefile : ;
 
 ###########################################################################
 # Cleaning
@@ -173,7 +173,7 @@ cruftclean: ml4clean
 
 indepclean:
 	rm -f $(GENFILES)
-	rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(FAKEIDE)
+	rm -f $(COQTOPBYTE) $(CHICKENBYTE)
 	find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete
 	rm -f */*.pp[iox] plugins/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
@@ -206,8 +206,8 @@ archclean: clean-ide optclean voclean
 	rm -f $(ALLSTDLIB).*
 
 optclean:
-	rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT)
-	rm -f $(TOOLS) $(CSDPCERT)
+	rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN)
+	rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT)
 	find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 
 clean-ide:
diff --git a/Makefile.build b/Makefile.build
index 7edc62028..69228e379 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -10,30 +10,40 @@
 # some variables.
 
 ###########################################################################
-# Starting rule
+# Default starting rule
 ###########################################################################
 
-# build the different subsystems: coq, coqide
-world: revision coq coqide documentation
+# build the different subsystems:
 
-.PHONY: world
+world: coq coqide documentation revision
+
+coq: coqlib coqbinaries tools printers
+
+.PHONY: world coq
 
 ###########################################################################
 # Includes
 ###########################################################################
 
-include Makefile.common
-include Makefile.doc
-
+# This list of ml files used to be in the main Makefile, we moved it here
+# to avoid exhausting the variable env in Win32
 MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
-DEPENDENCIES := \
- $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES))
 
-# This include below will lauch the build of all concerned .d.
+include Makefile.common
+include Makefile.doc      ## provides the 'documentation' rule
+include Makefile.checker
+include Makefile.ide      ## provides the 'coqide' rule
+include Makefile.install
+include Makefile.dev      ## provides the 'printers' and 'revision' rules
+
+# This include below will lauch the build of all .d.
 # The - at front is for disabling warnings about currently missing ones.
 # For creating the missing .d, make will recursively build things like
 # coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d).
 
+DEPENDENCIES := \
+ $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES))
+
 -include $(DEPENDENCIES)
 
 # All dependency includes must be declared secondary, otherwise make will
@@ -43,7 +53,6 @@ DEPENDENCIES := \
 
 .SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml)
 
-
 ###########################################################################
 # Compilation options
 ###########################################################################
@@ -56,7 +65,6 @@ NO_RECALC_DEPS=
 READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
 VALIDATE=
 COQ_XML=	# is "-xml" when building XML library
-VM=		# is "-no-vm" to not use the vm"
 
 TIMED=          # non-empty will activate a default time command
                 # when compiling .v (see $(STDTIME) below)
@@ -75,7 +83,7 @@ TIMECMD=	# if you prefer a specific time command instead of $(STDTIME)
 STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
-COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE)
+COQOPTS=$(COQ_XML) $(NATIVECOMPUTE)
 BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
@@ -104,12 +112,32 @@ LINKMETADATA=
 CODESIGN=true
 endif
 
+# Best OCaml compiler, used in a generic way
+
+ifeq ($(BEST),opt)
+OPT:=opt
+BESTOBJ:=.cmx
+BESTLIB:=.cmxa
+BESTDYN:=.cmxs
+else
+OPT:=
+BESTOBJ:=.cmo
+BESTLIB:=.cma
+BESTDYN:=.cma
+endif
+
+define bestobj
+$(patsubst %.cma,%$(BESTLIB),$(patsubst %.cmo,%$(BESTOBJ),$(1)))
+endef
+
 define bestocaml
 $(if $(OPT),\
 $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@,\
 $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
 endef
 
+# Camlp4 / Camlp5 settings
+
 CAMLP4DEPS:=tools/compat5.cmo grammar/grammar.cma
 ifeq ($(CAMLP4),camlp5)
 CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
@@ -172,13 +200,11 @@ endif
 TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
 
 ###########################################################################
-# Compilation option for .c files
+# Compilation of .c files
 ###########################################################################
 
 CINCLUDES= -I $(CAMLHLIB)
 
-# libcoqrun.a, dllcoqrun.so
-
 # NB: We used to do a ranlib after ocamlmklib, but it seems that
 # ocamlmklib is already doing it
 
@@ -186,7 +212,6 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
 	cd $(dir $(LIBCOQRUN)) && \
 	$(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
 
-#coq_jumptbl.h is required only if you have GCC 2.0 or later
 kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h
 	sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
                -e '/^}/q' $< $(TOTARGET)
@@ -195,6 +220,17 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
 	sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' $< | \
 	awk -f kernel/make-opcodes $(TOTARGET)
 
+%.o: %.c
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<)
+
+%_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC)
+	$(SHOW)'CCDEP	$<'
+	$(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@
+
+%.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES)
+	$(SHOW)'CCDEP     $<'
+	$(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET)
 
 ###########################################################################
 #  grammar/grammar.cma
@@ -264,25 +300,16 @@ grammar/%.cmi: grammar/%.mli
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
 
-.PHONY: coqbinaries coq coqlib coqlight states
+.PHONY: coqbinaries
 
-coqbinaries: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE}
+coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \
+ $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE)
 
-coq: coqlib tools coqbinaries
-
-coqlib: theories plugins
-
-coqlight: theories-light tools coqbinaries
-
-states: theories/Init/Prelude.vo
-
-miniopt: $(COQTOPEXE) pluginsopt
-minibyte: $(COQTOPBYTE) pluginsbyte
 
 ifeq ($(BEST),opt)
 $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
 	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -thread -o $@
+	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@
 	$(STRIP) $@
 	$(CODESIGN) $@
 else
@@ -292,28 +319,13 @@ endif
 
 $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA)
 	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@
+	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@
 
-LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) )
-CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB)
-
-ifeq ($(BEST),opt)
-$(CHICKEN): checker/check.cmxa checker/main.ml
-	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ $(SYSCMXA) $^
-	$(STRIP) $@
-	$(CODESIGN) $@
-else
-$(CHICKEN): $(CHICKENBYTE)
-	cp $< $@
-endif
+# coqmktop
 
-$(CHICKENBYTE): checker/check.cma checker/main.ml
-	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -thread -o $@ $(SYSCMA) $^
+COQMKTOPCMO:=lib/clib.cma lib/errors.cmo tools/tolink.cmo tools/coqmktop.cmo
 
-# coqmktop
-$(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ)))
+$(COQMKTOP): $(call bestobj, $(COQMKTOPCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
 
@@ -324,351 +336,19 @@ tools/tolink.ml: Makefile.build Makefile.common
 	$(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@
 
 # coqc
-$(COQC):  $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ)))
-	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
-
-# Target for libraries .cma and .cmxa
-
-# The dependency over the .mllib is somewhat artificial, since
-# ocamlc -a won't use this file, hence the $(filter-out ...) below.
-# But this ensures that the .cm(x)a is rebuilt when needed,
-# (especially when removing a module in the .mllib).
-# We used to have a "order-only" dependency over .mllib.d here,
-# but the -include mechanism should already ensure that we have
-# up-to-date dependencies.
-
-%.cma: %.mllib
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
-
-%.cmxa: %.mllib
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
-
-# For the checker, different flags may be used
-
-checker/check.cma: checker/check.mllib | md5chk
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
-checker/check.cmxa: checker/check.mllib | md5chk
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
-
-###########################################################################
-# Csdp to micromega special targets
-###########################################################################
+COQCCMO:=lib/clib.cma lib/errors.cmo toplevel/usage.cmo tools/coqc.cmo
 
-plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ))  \
-		$(addsuffix $(BESTLIB), lib/clib)
+$(COQC): $(call bestobj, $(COQCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,,nums unix clib)
-
-###########################################################################
-# CoqIde special targets
-###########################################################################
-
-.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
-
-# target to build CoqIde
-coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
-
-COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
-
-.SUFFIXES:.vo
-
-IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
-
-coqide-binaries: coqide-$(HASCOQIDE) ide-toploop
-coqide-no:
-coqide-byte: $(COQIDEBYTE) $(COQIDE)
-coqide-opt:  $(COQIDEBYTE) $(COQIDE)
-coqide-files: $(IDEFILES)
-ifeq ($(BEST),opt)
-ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs)
-else
-ide-toploop: $(IDETOPLOOPCMA)
-endif
-
-ifeq ($(HASCOQIDE),opt)
-$(COQIDE): $(LINKIDEOPT)
-	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \
-		lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^
-	$(STRIP) $@
-else
-$(COQIDE): $(COQIDEBYTE)
-	cp $< $@
-endif
-
-$(COQIDEBYTE): $(LINKIDE)
-	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \
-	        lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^
-
-# install targets
-
-.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
-
-ifeq ($(HASCOQIDE),no)
-install-coqide: install-ide-toploop
-else
-install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
-endif
-
-install-ide-bin:
-	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQIDE) $(FULLBINDIR)
-
-install-ide-toploop:
-	$(MKDIR) $(FULLCOQLIB)/toploop
-	$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
-ifeq ($(BEST),opt)
-	$(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
-endif
-
-install-ide-devfiles:
-	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
-	  $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
-ifeq ($(BEST),opt)
-	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a)
-endif
-
-install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time
-	$(MKDIR) $(FULLDATADIR)
-	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR)
-	$(MKDIR) $(FULLCONFIGDIR)
-	if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi
-
-install-ide-info:
-	$(MKDIR) $(FULLDOCDIR)
-	$(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde
-
-###########################################################################
-# CoqIde MacOS special targets
-###########################################################################
-
-.PHONY: $(COQIDEAPP)/Contents
-
-$(COQIDEAPP)/Contents:
-	rm -rdf $@
-	$(MKDIR) $@
-	sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist
-	$(MKDIR) "$@/MacOS"
-
-$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
-	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
-		unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \
-		threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^
-	$(STRIP) $@
-
-$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
-	$(MKDIR) $@/coq/
-	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/
-	$(MKDIR) $@/gtksourceview-2.0/{language-specs,styles}
-	$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/
-	$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/
-	cp -R "$(GTKSHARE)/"locale $@
-	cp -R "$(GTKSHARE)/"icons $@
-	cp -R "$(GTKSHARE)/"themes $@
-
-$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents
-	$(MKDIR) $@
-	$(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@
-
-$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents
-	$(MKDIR) $@
-	$(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@
-
-
-$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib
-	$(MKDIR) $@/xdg/coq
-	$(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys
-	$(MKDIR) $@/gtk-2.0
-	{ "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\
-	 sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \
-	> $@/gtk-2.0/gdk-pixbuf.loaders
-	{ "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\
-	 sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\
-	 sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \
-	> $@/gtk-2.0/gtk-immodules.loaders
-	$(MKDIR) $@/pango
-	echo "[Pango]" > $@/pango/pangorc
-
-$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP)
-	$(MKDIR) $@
-	$(INSTALLLIB) $(GTKLIBS)/charset.alias $@/
-	$(MKDIR) $@/pango/1.8.0/modules
-	$(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/
-	{ "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\
-	 sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \
-	> $@/pango/1.8.0/modules.cache
-
-	for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
-	    do cp $$i $@/; \
-	    ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \
-	done
-	for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \
-	    do \
-		for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
-		do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
-		ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \
-	    done
-	EXTRAWORK=1; \
-	while [ $${EXTRAWORK} -eq 1 ]; \
-	do EXTRAWORK=0; \
-	    for i in $@/*.dylib; \
-	    do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
-		do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
-	    done; \
-	done
-	ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@
-
-$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share
-	$(INSTALLLIB) ide/MacOS/*.icns $@
-
-$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources
-	$(CODESIGN) $@
-
-###########################################################################
-# tests
-###########################################################################
-
-.PHONY: validate check test-suite $(ALLSTDLIB).v md5chk
-
-md5chk:
-	$(SHOW)'MD5SUM cic.mli'
-	$(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \
-	       then true; else echo "Error: outdated checker/values.ml"; false; fi
-
-VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m
-
-validate: $(CHICKEN) | $(ALLVO)
-	$(SHOW)'COQCHK <theories & plugins>'
-	$(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
-
-$(ALLSTDLIB).v:
-	$(SHOW)'MAKE $(notdir $@)'
-	$(HIDE)echo "Require $(ALLMODS)." > $@
-
-MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)
-
-check: validate test-suite
-
-test-suite: world $(ALLSTDLIB).v
-	$(MAKE) $(MAKE_TSOPTS) clean
-	$(MAKE) $(MAKE_TSOPTS) all
-	$(MAKE) $(MAKE_TSOPTS) report
-
-##################################################################
-# partial targets: 1) core ML parts
-##################################################################
-
-.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
-.PHONY: engine highparsing stm toplevel ltac
-
-lib: lib/clib.cma lib/lib.cma
-kernel: kernel/kernel.cma
-byterun: $(BYTERUN)
-library: library/library.cma
-engine: engine/engine.cma
-proofs: proofs/proofs.cma
-tactics: tactics/tactics.cma
-interp: interp/interp.cma
-parsing: parsing/parsing.cma
-pretyping: pretyping/pretyping.cma
-highparsing: parsing/highparsing.cma
-stm: stm/stm.cma
-toplevel: toplevel/toplevel.cma
-ltac: ltac/ltac.cma
-
-###########################################################################
-# 2) theories and plugins files
-###########################################################################
-
-.PHONY: init theories theories-light
-.PHONY: logic arith bool narith zarith qarith lists strings sets
-.PHONY: fsets relations wellfounded reals setoids sorting numbers noreal
-.PHONY: msets mmaps compat
-
-init: $(INITVO)
-
-theories: $(THEORIESVO)
-theories-light: $(THEORIESLIGHTVO)
-
-logic: $(LOGICVO)
-arith: $(ARITHVO)
-bool: $(BOOLVO)
-narith: $(NARITHVO)
-zarith: $(ZARITHVO)
-qarith: $(QARITHVO)
-lists: $(LISTSVO)
-strings: $(STRINGSVO)
-sets: $(SETSVO)
-fsets: $(FSETSVO)
-relations: $(RELATIONSVO)
-wellfounded: $(WELLFOUNDEDVO)
-reals: $(REALSVO)
-setoids: $(SETOIDSVO)
-sorting: $(SORTINGVO)
-numbers: $(NUMBERSVO)
-unicode: $(UNICODEVO)
-classes: $(CLASSESVO)
-program: $(PROGRAMVO)
-structures: $(STRUCTURESVO)
-vectors: $(VECTORSVO)
-msets: $(MSETSVO)
-compat: $(COMPATVO)
-
-noreal: unicode logic arith bool zarith qarith lists sets fsets \
-	relations wellfounded setoids sorting
-
-###########################################################################
-# 3) plugins
-###########################################################################
-
-.PHONY: plugins omega micromega setoid_ring nsatz extraction
-.PHONY: fourier funind cc rtauto btauto pluginsopt pluginsbyte
-
-plugins: $(PLUGINSVO)
-omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
-micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
-setoid_ring: $(RINGVO) $(RINGCMA)
-nsatz: $(NSATZVO) $(NSATZCMA)
-extraction: $(EXTRACTIONCMA)
-fourier: $(FOURIERVO) $(FOURIERCMA)
-funind: $(FUNINDCMA) $(FUNINDVO)
-cc: $(CCVO) $(CCCMA)
-rtauto: $(RTAUTOVO) $(RTAUTOCMA)
-btauto: $(BTAUTOVO) $(BTAUTOCMA)
-
-pluginsopt: $(PLUGINSOPT)
-pluginsbyte: $(PLUGINS)
-
-###########################################################################
-# rules to make theories and plugins
-###########################################################################
-
-theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP)
-	$(SHOW)'COQC $(COQ_XML) -noinit $<'
-	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq
-
-theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
-	$(OCAML) $< $(TOTARGET)
+	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
 
 ###########################################################################
-# tools
+# other tools
 ###########################################################################
 
-.PHONY: printers tools
-
-printers: $(DEBUGPRINTERS)
-
-tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP)
+.PHONY:
+tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT)
 
 # coqdep_boot : a basic version of coqdep, with almost no dependencies.
 
@@ -694,355 +374,139 @@ $(OCAMLLIBDEP): tools/ocamllibdep.ml
 
 # The full coqdep (unused by this build, but distributed by make install)
 
-$(COQDEP): $(patsubst %.cma,%$(BESTLIB),$(COQDEPCMO:.cmo=$(BESTOBJ)))
+COQDEPCMO:=lib/clib.cma lib/errors.cmo lib/minisys.cmo lib/system.cmo \
+  tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
+
+$(COQDEP): $(call bestobj, $(COQDEPCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
 
-$(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina)
+$(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,)
 
-$(COQMAKEFILE):  $(patsubst %.cma,%$(BESTLIB),$(COQMAKEFILECMO:.cmo=$(BESTOBJ)))
+COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo
+
+$(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,str unix threads)
 
-$(COQTEX): tools/coq_tex$(BESTOBJ)
+$(COQTEX): $(call bestobj, tools/coq_tex.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,str)
 
-$(COQWC): tools/coqwc$(BESTOBJ)
+$(COQWC): $(call bestobj, tools/coqwc.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,)
 
-$(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ)))
+COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \
+  cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
+
+$(COQDOC): $(call bestobj, $(COQDOCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,str unix)
 
-$(COQWORKMGR): $(addsuffix $(BESTOBJ), stm/coqworkmgrApi tools/coqworkmgr) \
-		$(addsuffix $(BESTLIB), lib/clib)
+$(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml,, $(SYSMOD) clib)
+	$(HIDE)$(call bestocaml,, $(SYSMOD))
 
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
-$(FAKEIDE): lib/clib$(BESTLIB) lib/errors$(BESTOBJ)			\
-	    lib/spawn$(BESTOBJ) ide/document$(BESTOBJ)			\
-	    ide/serialize$(BESTOBJ) ide/xml_lexer$(BESTOBJ)		\
-	    ide/xml_parser$(BESTOBJ) ide/xml_printer$(BESTOBJ)		\
-	    ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) |	\
-	    $(IDETOPLOOPCMA:.cma=$(BESTDYN))
+FAKEIDECMO:= lib/clib.cma lib/errors.cmo lib/spawn.cmo ide/document.cmo \
+ ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \
+ ide/xmlprotocol.cmo tools/fake_ide.cmo
+
+$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,-I ide,str unix threads)
 
 # votour: a small vo explorer (based on the checker)
 
-bin/votour: lib/cObj$(BESTOBJ) checker/analyze$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml
+bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo) checker/votour.ml
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I checker,)
 
-# Special rule for the compatibility-with-camlp5 extension for camlp4
-
-ifeq ($(CAMLP4),camlp4)
-tools/compat5.cmo: tools/compat5.mlp
-	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $<
-tools/compat5b.cmo: tools/compat5b.mlp
-	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $<
-else
-tools/compat5.cmo: tools/compat5.ml
-	$(OCAMLC) -c $<
-endif
-
 ###########################################################################
-# Documentation : cf Makefile.doc
+# Csdp to micromega special targets
 ###########################################################################
 
-documentation: doc-$(WITHDOC)
-doc-all: doc
-doc-no:
+CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \
+  mutils.cmo 	micromega.cmo \
+  sos_types.cmo sos_lib.cmo sos.cmo 	csdpcert.cmo )
 
-.PHONY: documentation doc-all doc-no
+$(CSDPCERT): $(call bestobj, $(CSDPCERTCMO))
+	$(SHOW)'OCAMLBEST -o $@'
+	$(HIDE)$(call bestocaml,,nums unix)
 
 ###########################################################################
-# Installation
+# tests
 ###########################################################################
 
-ifeq ($(LOCAL),true)
-install:
-	@echo "Nothing to install in a local build!"
-else
-install: install-coq install-coqide install-doc-$(WITHDOC)
-endif
-
-install-doc-all: install-doc
-install-doc-no:
-
-.PHONY: install install-doc-all install-doc-no
+.PHONY: validate check test-suite $(ALLSTDLIB).v
 
-#These variables are intended to be set by the caller to make
-#COQINSTALLPREFIX=
-#OLDROOT=
-
-  # Can be changed for a local installation (to make packages).
-  # You must NOT put a "/" at the end (Cygnus for win32 does not like "//").
-
-ifdef COQINSTALLPREFIX
-FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-else
-FULLBINDIR=$(BINDIR)
-FULLCOQLIB=$(COQLIBINSTALL)
-FULLCONFIGDIR=$(CONFIGDIR)
-FULLDATADIR=$(DATADIR)
-FULLMANDIR=$(MANDIR)
-FULLEMACSLIB=$(EMACSLIB)
-FULLCOQDOCDIR=$(COQDOCDIR)
-FULLDOCDIR=$(DOCDIR)
-endif
-
-.PHONY: install-coq install-coqlight install-binaries install-byte install-opt
-.PHONY: install-tools install-library install-library-light install-devfiles
-.PHONY: install-coq-info install-coq-manpages install-emacs install-latex
-
-install-coq: install-binaries install-library install-coq-info install-devfiles
-install-coqlight: install-binaries install-library-light
-
-install-binaries: install-tools
-	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
-	$(MKDIR) $(FULLCOQLIB)/toploop
-	$(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/
-ifeq ($(BEST),opt)
-	$(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
-endif
-
-
-install-tools:
-	$(MKDIR) $(FULLBINDIR)
-	# recopie des fichiers de style pour coqide
-	$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
-	touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
-	$(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
-	$(INSTALLBIN) $(TOOLS) $(FULLBINDIR)
-
-# The list of .cmi to install, including the ones obtained
-# from .mli without .ml, and the ones obtained from .ml without .mli
-
-INSTALLCMI = $(sort \
-	$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
-	$(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES)))))
-
-install-devfiles:
-	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR)
-	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA)
-	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
-ifeq ($(BEST),opt)
-	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
-endif
-
-install-library:
-	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
-	$(MKDIR) $(FULLCOQLIB)/user-contrib
-ifndef CUSTOM
-	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
-endif
-ifeq ($(BEST),opt)
-	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
-endif
-# csdpcert is not meant to be directly called by the user; we install
-# it with libraries
-	-$(MKDIR) $(FULLCOQLIB)/plugins/micromega
-	$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega
-	rm -f $(FULLCOQLIB)/revision
-	-$(INSTALLLIB) revision $(FULLCOQLIB)
-
-install-library-light:
-	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS)
-	rm -f $(FULLCOQLIB)/revision
-	-$(INSTALLLIB) revision $(FULLCOQLIB)
-ifndef CUSTOM
-	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
-endif
-ifeq ($(BEST),opt)
-	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
-	$(INSTALLSH)  $(FULLCOQLIB) $(INITPLUGINSOPT)
-endif
+VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m
 
-install-coq-info: install-coq-manpages install-emacs install-latex
+validate: $(CHICKEN) | $(ALLVO)
+	$(SHOW)'COQCHK <theories & plugins>'
+	$(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
 
-install-coq-manpages:
-	$(MKDIR) $(FULLMANDIR)/man1
-	$(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1
+$(ALLSTDLIB).v:
+	$(SHOW)'MAKE $(notdir $@)'
+	$(HIDE)echo "Require $(ALLMODS)." > $@
 
-install-emacs:
-	$(MKDIR) $(FULLEMACSLIB)
-	$(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB)
+MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)
 
-# command to update TeX' kpathsea database
-#UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null
+check: validate test-suite
 
-install-latex:
-	$(MKDIR) $(FULLCOQDOCDIR)
-	$(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)	
-#	-$(UPDATETEX)
+test-suite: world $(ALLSTDLIB).v
+	$(MAKE) $(MAKE_TSOPTS) clean
+	$(MAKE) $(MAKE_TSOPTS) all
+	$(MAKE) $(MAKE_TSOPTS) report
 
 ###########################################################################
-# Documentation of the source code (using ocamldoc)
+### Special rules (Camlp5 / Camlp4)
 ###########################################################################
 
-.PHONY: source-doc mli-doc ml-doc
-
-source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
-
-$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
-	$(SHOW)'OCAMLDOC -latex -o $@'
-	$(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
-	$(DOCMLIS) -noheader -t "Coq mlis documentation" \
-	-intro $(OCAMLDOCDIR)/docintro -o $@.tmp
-	$(SHOW)'OCAMLDOC utf8 fix'
-	$(HIDE)$(OCAMLDOCDIR)/fix-ocamldoc-utf8 $@.tmp
-	$(HIDE)cat $(OCAMLDOCDIR)/header.tex $@.tmp > $@
-	rm $@.tmp
-
-mli-doc: $(DOCMLIS:.mli=.cmi)
-	$(SHOW)'OCAMLDOC -html'
-	$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \
-	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
-	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
-	-css-style style.css
-
-ml-dot: $(MLFILES)
-	$(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \
-	$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
-
-%_dep.png: %.dot
-	$(DOT) -Tpng $< -o $@
-
-%_types.dot: %.mli
-	$(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
-
-OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
-  $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
-
-%.dot: | %.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-ml-doc:
-	$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
-
-parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-grammar/grammar.dot : | grammar/grammar.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-%.dot: %.mli
-	$(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
+# Special rule for the compatibility-with-camlp5 extension for camlp4
 
-$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
-	$(SHOW)'PDFLATEX $*.tex'
-	$(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex)
-	$(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log)
+ifeq ($(CAMLP4),camlp4)
+tools/compat5.cmo: tools/compat5.mlp
+	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $<
+tools/compat5b.cmo: tools/compat5b.mlp
+	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $<
+else
+tools/compat5.cmo: tools/compat5.ml
+	$(OCAMLC) -c $<
+endif
 
 ###########################################################################
-### Special rules
+# Default rules for compiling ML code
 ###########################################################################
 
-dev/printers.cma: dev/printers.mllib
-	$(SHOW)'Testing $@'
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer
-	@rm -f test-printer
-	$(SHOW)'OCAMLC -a $@'   
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@
+# Target for libraries .cma and .cmxa
 
-ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
-	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@
-
-# pretty printing of the revision number when compiling a checked out
-# source tree
-.PHONY: revision
-
-revision:
-	$(SHOW)'CHECK revision'
-	$(HIDE)rm -f revision.new
-ifeq ($(CHECKEDOUT),svn)
-	$(HIDE)set -e; \
-        if test -x "`which svn`"; then \
-	  export LC_ALL=C;\
-	  svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \
-	  svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \
-	fi
-endif
-ifeq ($(CHECKEDOUT),gnuarch)
-	$(HIDE)set -e; \
-        if test -x "`which tla`"; then \
-	  LANG=C; export LANG; \
-	  tla tree-version  >  revision.new ; \
-	  tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \
-	fi
-endif
-ifeq ($(CHECKEDOUT),git)
-	$(HIDE)set -e; \
-	if test -x "`which git`"; then \
-	  LANG=C; export LANG; \
-	  GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \
-	  GIT_HOST=$$(hostname); \
-	  GIT_PATH=$$(pwd); \
-	  (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \
-	  (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \
-	fi
-endif
-	$(HIDE)set -e; \
-	if test -e revision.new; then \
-          if test -e revision; then \
-	    if test "`cat revision`" = "`cat revision.new`" ; then \
-	       rm -f revision.new; \
-            else \
-               mv -f revision.new revision; \
-            fi; \
-          else \
-            mv -f revision.new revision; \
-          fi \
-	fi
+# The dependency over the .mllib is somewhat artificial, since
+# ocamlc -a won't use this file, hence the $(filter-out ...) below.
+# But this ensures that the .cm(x)a is rebuilt when needed,
+# (especially when removing a module in the .mllib).
+# We used to have a "order-only" dependency over .mllib.d here,
+# but the -include mechanism should already ensure that we have
+# up-to-date dependencies.
 
-###########################################################################
-# Default rules
-###########################################################################
+%.cma: %.mllib
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
-## Three flavor of flags: checker/* ide/* and normal files
+%.cmxa: %.mllib
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
 COND_BYTEFLAGS= \
- $(if $(filter checker/%,$<), $(CHKLIBS) -thread, \
-   $(if $(filter ide/%,$<), $(COQIDEFLAGS), \
-     $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) -thread)) $(BYTEFLAGS)
+ $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS)
 
 COND_OPTFLAGS= \
- $(if $(filter checker/%,$<), $(CHKLIBS) -thread, \
-   $(if $(filter ide/%,$<), $(COQIDEFLAGS), \
-     $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) -thread)) $(OPTFLAGS)
-
-%.o: %.c
-	$(SHOW)'OCAMLC    $<'
-	$(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<)
-
-%.o: %.rc
-	$(SHOW)'WINDRES    $<'
-	$(HIDE)i686-w64-mingw32-windres -i $< -o $@
+ $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(OPTFLAGS)
 
 %.cmi: %.mli
 	$(SHOW)'OCAMLC    $<'
@@ -1103,87 +567,75 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) \
 	  $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
 
-%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP)
-	$(SHOW)'COQC      $<'
-	$(HIDE)rm -f $*.glob 
-	$(HIDE)$(BOOTCOQC) $<
-ifdef VALIDATE
-	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
-	$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
-	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
-endif
 
 ###########################################################################
-# Dependencies
+# Dependencies of ML code
 ###########################################################################
 
-# Since OCaml 3.12.1, we could use again ocamldep directly, thanks to
-# the option -ml-synonym
-
-OCAMLDEP_NG = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4
-
-checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(GENFILES)
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET)
-
-checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(GENFILES)
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET)
+# Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12)
+OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4
 
 %.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
+	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
 %.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
-
-checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES)
-	$(SHOW)'OCAMLLIBDEP  $<'
-	$(HIDE)$(OCAMLLIBDEP) $(LOCALCHKLIBS) "$<" $(TOTARGET)
-
-dev/%.mllib.d: $(D_DEPEND_BEFORE_SRC) dev/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES)
-	$(SHOW)'OCAMLLIBDEP  $<'
-	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) -I dev "$<" $(TOTARGET)
+	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
 %.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES)
 	$(SHOW)'OCAMLLIBDEP  $<'
 	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
-%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
-	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET)
+###########################################################################
+# Compilation of .v files
+###########################################################################
 
-%_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC)
-	$(SHOW)'CCDEP	$<'
-	$(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@
+# NB: for make world, no need to mention explicitly the .cmxs of the plugins,
+# since they are all mentioned in at least one Declare ML Module in some .v
 
-%.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES)
-	$(SHOW)'CCDEP     $<'
-	$(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET)
+coqlib: theories plugins
 
-###########################################################################
-# this sets up developper supporting stuff
-###########################################################################
+theories: $(THEORIESVO)
+plugins: $(PLUGINSVO)
 
-.PHONY: devel otags
-devel: $(DEBUGPRINTERS)
+.PHONY: coqlib theories plugins
 
-# NOTA : otags only accepts camlp4 as preprocessor, so the following rule
-# won't build tags of .ml4 when compiling with camlp5
-otags:
-	otags $(MLIFILES) $(filter-out configure.ml, $(MLSTATICFILES)) \
-	$(if $(filter camlp5,$(CAMLP4)), , \
-          -pa op -pa g -pa m -pa rq $(addprefix -pa , $(CAMLP4DEPS)) \
-          $(addprefix -impl , $(ML4FILES)))
+# One of the .v files is macro-generated
 
+theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
+	$(OCAML) $< $(TOTARGET)
+
+# The .vo files in Init are built with the -noinit option
+
+theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP)
+	$(SHOW)'COQC $(COQ_XML) -noinit $<'
+	$(HIDE)rm -f theories/Init/$*.glob
+	$(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq
+
+# The general rule for building .vo files :
+
+%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP)
+	$(SHOW)'COQC      $<'
+	$(HIDE)rm -f $*.glob
+	$(HIDE)$(BOOTCOQC) $<
+ifdef VALIDATE
+	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
+	$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
+	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
+endif
+
+# Dependencies of .v files
+
+%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
+	$(SHOW)'COQDEP    $<'
+	$(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET)
 
 ###########################################################################
 
 # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
 
-Makefile Makefile.build Makefile.common config/Makefile : ;
-
+Makefile $(wildcard Makefile.*) config/Makefile : ;
 
 # For emacs: 
 # Local Variables: 
diff --git a/Makefile.checker b/Makefile.checker
new file mode 100644
index 000000000..3ea0baced
--- /dev/null
+++ b/Makefile.checker
@@ -0,0 +1,86 @@
+#######################################################################
+#  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       #
+#######################################################################
+
+## Makefile rules for building Coqchk
+
+## NB: For the moment, the build system of Coqchk is part of
+## the one of Coq. In particular, this Makefile.checker is included in
+## Makefile.build. Please ensure that the rules define here are
+## indeed specific to files of the form checker/*
+
+# The binaries
+
+CHICKENBYTE:=bin/coqchk.byte$(EXE)
+CHICKEN:=bin/coqchk$(EXE)
+
+# The sources
+
+CHKLIBS:= -I config -I lib -I checker
+
+## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread
+
+# The rules
+
+ifeq ($(BEST),opt)
+$(CHICKEN): checker/check.cmxa checker/main.ml
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(SYSCMXA) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
+	$(STRIP) $@
+	$(CODESIGN) $@
+else
+$(CHICKEN): $(CHICKENBYTE)
+	cp $< $@
+endif
+
+$(CHICKENBYTE): checker/check.cma checker/main.ml
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(OCAMLC) $(SYSCMA) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^
+
+checker/check.cma: checker/check.mllib | md5chk
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
+
+checker/check.cmxa: checker/check.mllib | md5chk
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
+
+checker/%.ml.d: checker/%.ml
+	$(SHOW)'OCAMLDEP  $<'
+	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET)
+
+checker/%.mli.d: checker/%.mli
+	$(SHOW)'OCAMLDEP  $<'
+	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET)
+
+checker/%.mllib.d: checker/%.mllib | $(OCAMLLIBDEP)
+	$(SHOW)'OCAMLLIBDEP  $<'
+	$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) "$<" $(TOTARGET)
+
+checker/%.cmi: checker/%.mli
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -c $<
+
+checker/%.cmo: checker/%.ml
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -c $<
+
+checker/%.cmx: checker/%.ml
+	$(SHOW)'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $<
+
+md5chk:
+	$(SHOW)'MD5SUM cic.mli'
+	$(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \
+	       then true; else echo "Error: outdated checker/values.ml"; false; fi
+
+.PHONY: md5chk
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End:
diff --git a/Makefile.common b/Makefile.common
index 86a7ea847..463006c49 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -14,19 +14,32 @@
 
 COQMKTOP:=bin/coqmktop$(EXE) 
 
-COQC:=bin/coqc$(EXE)
-
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
 COQTOPEXE:=bin/coqtop$(EXE)
 
-CHICKENBYTE:=bin/coqchk.byte$(EXE)
-CHICKEN:=bin/coqchk$(EXE)
+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)
+COQC:=bin/coqc$(EXE)
+COQWORKMGR:=bin/coqworkmgr$(EXE)
 
-ifeq ($(CAMLP4),camlp4)
-CAMLP4MOD:=camlp4lib
-else
-CAMLP4MOD:=gramlib
-endif
+TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
+	$(COQWORKMGR)
+
+COQDEPBOOT:=bin/coqdep_boot$(EXE)
+OCAMLLIBDEP:=bin/ocamllibdep$(EXE)
+FAKEIDE:=bin/fake_ide$(EXE)
+
+PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT)
+
+CSDPCERT:=plugins/micromega/csdpcert$(EXE)
+
+###########################################################################
+# Object and Source files
+###########################################################################
 
 ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
   DEPNATDYN:=
@@ -39,27 +52,6 @@ INSTALLLIB:=install -m 644
 INSTALLSH:=./install.sh
 MKDIR:=install -d
 
-COQIDEBYTE:=bin/coqide.byte$(EXE)
-COQIDE:=bin/coqide$(EXE)
-COQIDEAPP:=bin/CoqIDE_$(VERSION).app
-COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
-
-ifeq ($(BEST),opt)
-OPT:=opt
-else
-OPT:=
-endif
-
-BESTOBJ:=$(if $(OPT),.cmx,.cmo)
-BESTLIB:=$(if $(OPT),.cmxa,.cma)
-BESTDYN:=$(if $(OPT),.cmxs,.cma)
-
-COQBINARIES:= $(COQMKTOP) \
-  $(COQTOPBYTE) $(COQTOPEXE) \
-  $(CHICKENBYTE) $(CHICKEN)
-
-CSDPCERT:=plugins/micromega/csdpcert$(EXE)
-
 CORESRCDIRS:=\
   config 	lib		kernel		kernel/byterun	library \
   proofs 	tactics 	pretyping	interp		stm \
@@ -76,82 +68,6 @@ SRCDIRS:=\
   tools 	tools/coqdoc	\
   $(addprefix plugins/, $(PLUGINS))
 
-IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
-
-CHKSRCDIRS:= config lib checker
-
-###########################################################################
-# Tools
-###########################################################################
-
-COQDEP:=bin/coqdep$(EXE)
-COQDEPBOOT:=bin/coqdep_boot$(EXE)
-OCAMLLIBDEP:=bin/ocamllibdep$(EXE)
-COQMAKEFILE:=bin/coq_makefile$(EXE)
-GALLINA:=bin/gallina$(EXE)
-COQTEX:=bin/coq-tex$(EXE)
-COQWC:=bin/coqwc$(EXE)
-COQDOC:=bin/coqdoc$(EXE)
-FAKEIDE:=bin/fake_ide$(EXE)
-COQWORKMGR:=bin/coqworkmgr$(EXE)
-
-TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
-	$(COQWORKMGR)
-
-PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT)
-
-###########################################################################
-# Documentation
-###########################################################################
-
-LATEX:=latex
-BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10
-MAKEINDEX:=makeindex
-PDFLATEX:=pdflatex
-DVIPS:=dvips
-FIG2DEV:=fig2dev
-CONVERT:=convert
-HEVEA:=hevea
-HACHA:=hacha
-HEVEAOPTS:=-fix -exec xxdate.exe
-HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
-HTMLSTYLE:=simple
-export TEXINPUTS:=$(HEVEALIB):
-COQTEXOPTS:=-boot -n 72 -sl -small
-
-DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.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 RefMan-pro.v.tex RefMan-sch.v.tex \
-  Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
-  Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
-  Setoid.v.tex Classes.v.tex Universes.v.tex \
-  Misc.v.tex)
-
-REFMANTEXFILES:=$(addprefix doc/refman/, \
-  headers.sty Reference-Manual.tex \
-  RefMan-pre.tex RefMan-int.tex RefMan-com.tex \
-  RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \
-  AsyncProofs.tex ) \
-  $(REFMANCOQTEXFILES) \
-
-REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps
-
-REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib
-
-REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
-
-
-
-###########################################################################
-# Object and Source files 
-###########################################################################
-
 COQRUN := coqrun
 LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
 DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT)
@@ -173,6 +89,14 @@ TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
 GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma
 
+# modules known by the toplevel of Coq
+
+OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib))
+
+###########################################################################
+# plugins object files
+###########################################################################
+
 OMEGACMA:=plugins/omega/omega_plugin.cma
 ROMEGACMA:=plugins/romega/romega_plugin.cma
 MICROMEGACMA:=plugins/micromega/micromega_plugin.cma
@@ -230,169 +154,47 @@ endif
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
-IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo
-IDECMA:=ide/ide.cma
-IDETOPLOOPCMA=ide/coqidetop.cma
-
-LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
-
-# modules known by the toplevel of Coq
-
-OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib))
-
-IDEMOD:=$(shell cat ide/ide.mllib)
-
-# coqmktop, coqc
-
-COQENVCMO:=lib/clib.cma lib/errors.cmo
-
-COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo
-
-COQCCMO:=$(COQENVCMO) toplevel/usage.cmo tools/coqc.cmo
-
-## Misc
-
-CSDPCERTCMO:=$(addprefix plugins/micromega/, \
-  mutils.cmo 	micromega.cmo \
-  sos_types.cmo sos_lib.cmo sos.cmo 	csdpcert.cmo )
-
-DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
-
-COQDEPCMO:=$(COQENVCMO) lib/minisys.cmo lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
-
-COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \
-  cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
-
-COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo
-
 ###########################################################################
 # vo files
 ###########################################################################
 
 ## we now retrieve the names of .vo file to compile in */vo.itarget files
 
-cat_vo_itarget = $(addprefix $(1)/,$(shell cat $(1)/vo.itarget))
-
-## Theories
-
-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)
-PARITHVO:=$(call cat_vo_itarget, theories/PArith)
-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)
-VECTORSVO:=$(call cat_vo_itarget, theories/Vectors)
-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)
-COMPATVO:=$(call cat_vo_itarget, theories/Compat)
-
-THEORIESVO:=\
-  $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) \
-  $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) \
-  $(RELATIONSVO) $(WELLFOUNDEDVO) $(SETOIDSVO) \
-  $(LISTSVO) $(STRINGSVO) \
-  $(PARITHVO) $(NARITHVO) $(ZARITHVO) \
-  $(SETSVO) $(FSETSVO) $(MSETSVO) \
-  $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
-  $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO) \
-  $(COMPATVO)
-
-THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(UNICODEVO) $(ARITHVO)
-
-## 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/setoid_ring)
-NSATZVO:=$(call cat_vo_itarget, plugins/nsatz)
-FOURIERVO:=$(call cat_vo_itarget, plugins/fourier)
-FUNINDVO:=$(call cat_vo_itarget, plugins/funind)
-BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto)
-RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto)
-EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
-CCVO:=
-DERIVEVO:=$(call cat_vo_itarget, plugins/derive)
-
-PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \
-	    $(FOURIERVO) $(CCVO) $(FUNINDVO) \
-	    $(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \
-            $(NSATZVO) $(EXTRACTIONVO) $(DERIVEVO)
+THEORIESVO:= $(foreach f, $(wildcard theories/*/vo.itarget), \
+                $(addprefix $(dir $(f)),$(shell cat $(f))))
+
+PLUGINSVO:=  $(foreach f, $(wildcard plugins/*/vo.itarget), \
+                $(addprefix $(dir $(f)),$(shell cat $(f))))
 
 ALLVO:= $(THEORIESVO) $(PLUGINSVO)
 VFILES:= $(ALLVO:.vo=.v)
+
+## More specific targets
+
+THEORIESLIGHTVO:= \
+ $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO))
+
 ALLSTDLIB := test-suite/misc/universes/all_stdlib
 
 # convert a (stdlib) filename into a module name:
 # 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))
+
+
 # Converting a stdlib filename into native compiler filenames
 # Used for install targets
 vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
 
 vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
 
-ALLMODS:=$(call vo_to_mod,$(ALLVO))
-
 LIBFILES:=$(THEORIESVO) $(PLUGINSVO) $(call vo_to_cm,$(THEORIESVO)) \
 	    $(call vo_to_cm,$(PLUGINSVO)) $(call vo_to_obj,$(THEORIESVO)) \
 	    $(call vo_to_obj,$(PLUGINSVO)) \
 	    $(PLUGINSVO:.vo=.v) $(THEORIESVO:.vo=.v) \
 	    $(PLUGINSVO:.vo=.glob) $(THEORIESVO:.vo=.glob)
 
-LIBFILESLIGHT:=$(THEORIESLIGHTVO)
-
-###########################################################################
-# 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/coqchk.1
-
-###########################################################################
-# Source documentation
-###########################################################################
-
-OCAMLDOCDIR=dev/ocamldoc
-
-DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
-	./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \
-	./parsing/*.mli ./proofs/*.mli \
-	./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli)
-
-# Defining options to generate dependencies graphs
-DOT=dot
-ODOCDOTOPTS=-dot -dot-reduce
-
-###########################################################################
-# GTK for Coqide MacOS bundle
-###########################################################################
-
-GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share
-GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin
-GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
-
-
 # For emacs: 
 # Local Variables: 
 # mode: makefile 
diff --git a/Makefile.dev b/Makefile.dev
new file mode 100644
index 000000000..f35b861c1
--- /dev/null
+++ b/Makefile.dev
@@ -0,0 +1,223 @@
+#######################################################################
+#  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       #
+#######################################################################
+
+# Extra targets for developpers :
+# debug printers, revision, partial targets ...
+
+#########################
+# Debug printers in dev/
+#########################
+
+.PHONY: devel printers
+
+DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
+
+devel: printers
+printers: $(DEBUGPRINTERS)
+
+dev/printers.cma: dev/printers.mllib
+	$(SHOW)'Testing $@'
+	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer
+	@rm -f test-printer
+	$(SHOW)'OCAMLC -a $@'
+	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@
+
+dev/%.mllib.d: dev/%.mllib | $(OCAMLLIBDEP) $(GENFILES)
+	$(SHOW)'OCAMLLIBDEP  $<'
+	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) -I dev "$<" $(TOTARGET)
+
+############
+# revision
+############
+
+# display the revision number when compiling a checked out source tree
+
+revision:
+	$(SHOW)'CHECK revision'
+	$(HIDE)rm -f revision.new
+ifeq ($(CHECKEDOUT),svn)
+	$(HIDE)set -e; \
+        if test -x "`which svn`"; then \
+	  export LC_ALL=C;\
+	  svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \
+	  svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \
+	fi
+endif
+ifeq ($(CHECKEDOUT),gnuarch)
+	$(HIDE)set -e; \
+        if test -x "`which tla`"; then \
+	  LANG=C; export LANG; \
+	  tla tree-version  >  revision.new ; \
+	  tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \
+	fi
+endif
+ifeq ($(CHECKEDOUT),git)
+	$(HIDE)set -e; \
+	if test -x "`which git`"; then \
+	  LANG=C; export LANG; \
+	  GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \
+	  GIT_HOST=$$(hostname); \
+	  GIT_PATH=$$(pwd); \
+	  (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \
+	  (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \
+	fi
+endif
+	$(HIDE)set -e; \
+	if test -e revision.new; then \
+          if test -e revision; then \
+	    if test "`cat revision`" = "`cat revision.new`" ; then \
+	       rm -f revision.new; \
+            else \
+               mv -f revision.new revision; \
+            fi; \
+          else \
+            mv -f revision.new revision; \
+          fi \
+	fi
+
+.PHONY: revision
+
+###################
+# Partial builds
+###################
+
+# The following partial targets are normally not necessary
+# for a complete build of coq, see instead 'make world' for that.
+# But these partial targets could be quite handy for quick builds
+# of specific components of Coq.
+
+###############################
+### 1) general-purpose targets
+###############################
+
+coqlight: theories-light tools coqbinaries
+
+states: theories/Init/Prelude.vo
+
+miniopt: $(COQTOPEXE) pluginsopt
+minibyte: $(COQTOPBYTE) pluginsbyte
+
+pluginsopt: $(PLUGINSOPT)
+pluginsbyte: $(PLUGINS)
+
+.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte
+
+##########################
+### 2) core ML components
+##########################
+
+lib: lib/clib.cma lib/lib.cma
+kernel: kernel/kernel.cma
+byterun: $(BYTERUN)
+library: library/library.cma
+engine: engine/engine.cma
+proofs: proofs/proofs.cma
+tactics: tactics/tactics.cma
+interp: interp/interp.cma
+parsing: parsing/parsing.cma
+pretyping: pretyping/pretyping.cma
+highparsing: parsing/highparsing.cma
+stm: stm/stm.cma
+toplevel: toplevel/toplevel.cma
+ltac: ltac/ltac.cma
+
+.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
+.PHONY: engine highparsing stm toplevel ltac
+
+######################
+### 3) theories files
+######################
+
+init: $(filter theories/Init/%, $(THEORIESVO))
+logic: $(filter theories/Logic/%, %(THEORIESVO))
+arith: $(filter theories/Arith/%, $(THEORIESVO))
+bool: $(filter theories/Bool/%, $(THEORIESVO))
+parith: $(filter theories/PArith/%, $(THEORIESVO))
+narith: $(filter theories/NArith/%, $(THEORIESVO))
+zarith: $(filter theories/ZArith/%, $(THEORIESVO))
+qarith: $(filter theories/QArith/%, $(THEORIESVO))
+lists: $(filter theories/Lists/%, $(THEORIESVO))
+strings: $(filter theories/Strings/%, $(THEORIESVO))
+sets: $(filter theories/Sets/%, $(THEORIESVO))
+fsets: $(filter theories/FSets/%, $(THEORIESVO))
+relations: $(filter theories/Relations/%, $(THEORIESVO))
+wellfounded: $(filter theories/Wellfounded/%, $(THEORIESVO))
+reals: $(filter theories/Reals/%, $(THEORIESVO))
+setoids: $(filter theories/Setoids/%, $(THEORIESVO))
+sorting: $(filter theories/Sorting/%, $(THEORIESVO))
+numbers: $(filter theories/Numbers/%, $(THEORIESVO))
+unicode: $(filter theories/Unicode/%, $(THEORIESVO))
+classes: $(filter theories/Classes/%, $(THEORIESVO))
+program: $(filter theories/Program/%, $(THEORIESVO))
+structures: $(filter theories/Structures/%, $(THEORIESVO))
+vectors: $(filter theories/Vectors/%, $(THEORIESVO))
+msets: $(filter theories/MSets/%, $(THEORIESVO))
+compat: $(filter theories/Compat/%, $(THEORIESVO))
+
+theories-light: $(THEORIESLIGHTVO)
+
+noreal: unicode logic arith bool zarith qarith lists sets fsets \
+	relations wellfounded setoids sorting
+
+.PHONY: init theories-light noreal
+.PHONY: logic arith bool narith zarith qarith lists strings sets
+.PHONY: fsets relations wellfounded reals setoids sorting numbers
+.PHONY: msets mmaps compat
+
+################
+### 4) plugins
+################
+
+OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO))
+ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO))
+MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO))
+QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO))
+RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO))
+NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO))
+FOURIERVO:=$(filter plugins/fourier/%, $(PLUGINSVO))
+FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO))
+BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO))
+RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO))
+EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO))
+CCVO:=
+DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO))
+
+omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
+micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
+setoid_ring: $(RINGVO) $(RINGCMA)
+nsatz: $(NSATZVO) $(NSATZCMA)
+extraction: $(EXTRACTIONCMA)
+fourier: $(FOURIERVO) $(FOURIERCMA)
+funind: $(FUNINDCMA) $(FUNINDVO)
+cc: $(CCVO) $(CCCMA)
+rtauto: $(RTAUTOVO) $(RTAUTOCMA)
+btauto: $(BTAUTOVO) $(BTAUTOCMA)
+
+.PHONY: omega micromega setoid_ring nsatz extraction
+.PHONY: fourier funind cc rtauto btauto
+
+#################################
+### Misc other development rules
+#################################
+
+# NOTA : otags only accepts camlp4 as preprocessor, so the following rule
+# won't build tags of .ml4 when compiling with camlp5
+
+otags:
+	otags $(MLIFILES) $(filter-out configure.ml, $(MLSTATICFILES)) \
+	$(if $(filter camlp5,$(CAMLP4)), , \
+          -pa op -pa g -pa m -pa rq $(addprefix -pa , $(CAMLP4DEPS)) \
+          $(addprefix -impl , $(ML4FILES)))
+
+.PHONY: otags
+
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End:
diff --git a/Makefile.doc b/Makefile.doc
index b7251ce57..6c345025a 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -1,3 +1,11 @@
+#######################################################################
+#  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       #
+#######################################################################
+
 # Makefile for the Coq documentation
 
 # To compile documentation, you need the following tools:
@@ -5,6 +13,61 @@
 # Pdf: pdflatex
 # Html: hevea (http://hevea.inria.fr) >= 1.05
 
+# The main entry point :
+
+documentation: doc-$(WITHDOC)  ## see $(WITHDOC) in config/Makefile
+doc-all: doc
+doc-no:
+
+.PHONY: documentation doc-all doc-no
+
+######################################################################
+### Variables
+######################################################################
+
+LATEX:=latex
+BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10
+MAKEINDEX:=makeindex
+PDFLATEX:=pdflatex
+DVIPS:=dvips
+FIG2DEV:=fig2dev
+CONVERT:=convert
+HEVEA:=hevea
+HACHA:=hacha
+HEVEAOPTS:=-fix -exec xxdate.exe
+HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
+HTMLSTYLE:=simple
+export TEXINPUTS:=$(HEVEALIB):
+COQTEXOPTS:=-boot -n 72 -sl -small
+
+DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.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 RefMan-pro.v.tex RefMan-sch.v.tex \
+  Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
+  Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
+  Setoid.v.tex Classes.v.tex Universes.v.tex \
+  Misc.v.tex)
+
+REFMANTEXFILES:=$(addprefix doc/refman/, \
+  headers.sty Reference-Manual.tex \
+  RefMan-pre.tex RefMan-int.tex RefMan-com.tex \
+  RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \
+  AsyncProofs.tex ) \
+  $(REFMANCOQTEXFILES) \
+
+REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps
+
+REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib
+
+REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
+
+
 ######################################################################
 ### General rules
 ######################################################################
@@ -339,6 +402,80 @@ install-doc-index-urls:
 	$(MKDIR) $(FULLDATADIR)
 	$(INSTALLLIB) $(INDEXURLS) $(FULLDATADIR)
 
+
+###########################################################################
+# Documentation of the source code (using ocamldoc)
+###########################################################################
+
+OCAMLDOCDIR=dev/ocamldoc
+
+DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
+	./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \
+	./parsing/*.mli ./proofs/*.mli \
+	./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli)
+
+# Defining options to generate dependencies graphs
+DOT=dot
+ODOCDOTOPTS=-dot -dot-reduce
+
+.PHONY: source-doc mli-doc ml-doc
+
+source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
+
+$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
+	$(SHOW)'OCAMLDOC -latex -o $@'
+	$(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+	$(DOCMLIS) -noheader -t "Coq mlis documentation" \
+	-intro $(OCAMLDOCDIR)/docintro -o $@.tmp
+	$(SHOW)'OCAMLDOC utf8 fix'
+	$(HIDE)$(OCAMLDOCDIR)/fix-ocamldoc-utf8 $@.tmp
+	$(HIDE)cat $(OCAMLDOCDIR)/header.tex $@.tmp > $@
+	rm $@.tmp
+
+mli-doc: $(DOCMLIS:.mli=.cmi)
+	$(SHOW)'OCAMLDOC -html'
+	$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \
+	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
+	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
+	-css-style style.css
+
+ml-dot: $(MLFILES)
+	$(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \
+	$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
+
+%_dep.png: %.dot
+	$(DOT) -Tpng $< -o $@
+
+%_types.dot: %.mli
+	$(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
+
+OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
+  $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
+
+%.dot: | %.mllib.d
+	$(OCAMLDOC_MLLIBD)
+
+ml-doc:
+	$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
+
+parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
+	$(OCAMLDOC_MLLIBD)
+
+grammar/grammar.dot : | grammar/grammar.mllib.d
+	$(OCAMLDOC_MLLIBD)
+
+tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d
+	$(OCAMLDOC_MLLIBD)
+
+%.dot: %.mli
+	$(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
+
+$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
+	$(SHOW)'PDFLATEX $*.tex'
+	$(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex)
+	$(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log)
+
+
 # For emacs:
 # Local Variables:
 # mode: makefile
diff --git a/Makefile.ide b/Makefile.ide
new file mode 100644
index 000000000..8d6b5de36
--- /dev/null
+++ b/Makefile.ide
@@ -0,0 +1,254 @@
+#######################################################################
+#  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       #
+#######################################################################
+
+## Makefile rules for building the CoqIDE interface
+
+## NB: For the moment, the build system of CoqIDE is part of
+## the one of Coq. In particular, this Makefile.ide is included in
+## Makefile.build. Please ensure that the rules define here are
+## indeed specific to files of the form ide/*
+
+## Coqide-related variables set by ./configure in config/Makefile
+
+#COQIDEINCLUDES : something like -I +lablgtk2
+#HASCOQIDE : opt / byte / no
+#IDEFLAGS : some extra cma, for instance
+#IDEOPTCDEPS : on windows, ide/ide_win32_stubs.o ide/coq_icon.o
+#IDECDEPS
+#IDECDEPSFLAGS
+#IDEINT : X11 / QUARTZ / WIN32
+
+## CoqIDE Executable
+
+COQIDEBYTE:=bin/coqide.byte$(EXE)
+COQIDE:=bin/coqide$(EXE)
+COQIDEAPP:=bin/CoqIDE_$(VERSION).app
+COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
+
+## CoqIDE source directory and files
+
+# Note : for just building bin/coqide, we could only consider
+# config, lib, ide and ide/utils. But the coqidetop plugin (the
+# one that will be loaded by coqtop -ideslave) refers to some
+# core modules of coq, for instance printing/*.
+
+IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
+
+COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
+
+IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo
+IDECMA:=ide/ide.cma
+IDETOPLOOPCMA=ide/coqidetop.cma
+
+LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
+
+IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
+
+## GTK for Coqide MacOS bundle
+
+GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share
+GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin
+GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
+
+
+###########################################################################
+# CoqIde special targets
+###########################################################################
+
+.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
+
+# target to build CoqIde
+coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
+
+coqide-binaries: coqide-$(HASCOQIDE) ide-toploop
+coqide-no:
+coqide-byte: $(COQIDEBYTE) $(COQIDE)
+coqide-opt:  $(COQIDEBYTE) $(COQIDE)
+coqide-files: $(IDEFILES)
+ifeq ($(BEST),opt)
+ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs)
+else
+ide-toploop: $(IDETOPLOOPCMA)
+endif
+
+ifeq ($(HASCOQIDE),opt)
+$(COQIDE): $(LINKIDEOPT)
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \
+		lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^
+	$(STRIP) $@
+else
+$(COQIDE): $(COQIDEBYTE)
+	cp $< $@
+endif
+
+$(COQIDEBYTE): $(LINKIDE)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \
+	        lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^
+
+ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
+	$(SHOW)'CAMLP4O   $<'
+	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@
+
+
+ide/%.cmi: ide/%.mli
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+
+ide/%.cmo: ide/%.ml
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+
+ide/%.cmx: ide/%.ml
+	$(SHOW)'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $<
+
+
+####################
+## Install targets
+####################
+
+.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
+
+ifeq ($(HASCOQIDE),no)
+install-coqide: install-ide-toploop
+else
+install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
+endif
+
+install-ide-bin:
+	$(MKDIR) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQIDE) $(FULLBINDIR)
+
+install-ide-toploop:
+	$(MKDIR) $(FULLCOQLIB)/toploop
+	$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
+ifeq ($(BEST),opt)
+	$(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
+endif
+
+install-ide-devfiles:
+	$(MKDIR) $(FULLCOQLIB)
+	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
+	  $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
+ifeq ($(BEST),opt)
+	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a)
+endif
+
+install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time
+	$(MKDIR) $(FULLDATADIR)
+	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR)
+	$(MKDIR) $(FULLCONFIGDIR)
+	if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi
+
+install-ide-info:
+	$(MKDIR) $(FULLDOCDIR)
+	$(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde
+
+###########################################################################
+# CoqIde MacOS special targets
+###########################################################################
+
+.PHONY: $(COQIDEAPP)/Contents
+
+$(COQIDEAPP)/Contents:
+	rm -rdf $@
+	$(MKDIR) $@
+	sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist
+	$(MKDIR) "$@/MacOS"
+
+$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
+		unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \
+		threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^
+	$(STRIP) $@
+
+$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
+	$(MKDIR) $@/coq/
+	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/
+	$(MKDIR) $@/gtksourceview-2.0/{language-specs,styles}
+	$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/
+	$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/
+	cp -R "$(GTKSHARE)/"locale $@
+	cp -R "$(GTKSHARE)/"icons $@
+	cp -R "$(GTKSHARE)/"themes $@
+
+$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents
+	$(MKDIR) $@
+	$(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@
+
+$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents
+	$(MKDIR) $@
+	$(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@
+
+
+$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib
+	$(MKDIR) $@/xdg/coq
+	$(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys
+	$(MKDIR) $@/gtk-2.0
+	{ "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\
+	 sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \
+	> $@/gtk-2.0/gdk-pixbuf.loaders
+	{ "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\
+	 sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\
+	 sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \
+	> $@/gtk-2.0/gtk-immodules.loaders
+	$(MKDIR) $@/pango
+	echo "[Pango]" > $@/pango/pangorc
+
+$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP)
+	$(MKDIR) $@
+	$(INSTALLLIB) $(GTKLIBS)/charset.alias $@/
+	$(MKDIR) $@/pango/1.8.0/modules
+	$(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/
+	{ "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\
+	 sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \
+	> $@/pango/1.8.0/modules.cache
+
+	for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
+	    do cp $$i $@/; \
+	    ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \
+	done
+	for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \
+	    do \
+		for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
+		do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
+		ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \
+	    done
+	EXTRAWORK=1; \
+	while [ $${EXTRAWORK} -eq 1 ]; \
+	do EXTRAWORK=0; \
+	    for i in $@/*.dylib; \
+	    do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
+		do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
+	    done; \
+	done
+	ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@
+
+$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share
+	$(INSTALLLIB) ide/MacOS/*.icns $@
+
+$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources
+	$(CODESIGN) $@
+
+###########################################################################
+# CoqIde for Windows special targets
+###########################################################################
+
+%.o: %.rc
+	$(SHOW)'WINDRES    $<'
+	$(HIDE)i686-w64-mingw32-windres -i $< -o $@
+
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End:
diff --git a/Makefile.install b/Makefile.install
new file mode 100644
index 000000000..ed29bc1e7
--- /dev/null
+++ b/Makefile.install
@@ -0,0 +1,136 @@
+#######################################################################
+#  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       #
+#######################################################################
+
+# This makefile regroups installation rules
+# It is included by Makefile.build
+
+ifeq ($(LOCAL),true)
+install:
+	@echo "Nothing to install in a local build!"
+else
+install: install-coq install-coqide install-doc-$(WITHDOC)
+endif
+
+install-doc-all: install-doc
+install-doc-no:
+
+.PHONY: install install-doc-all install-doc-no
+
+#These variables are intended to be set by the caller to make
+#COQINSTALLPREFIX=
+#OLDROOT=
+
+  # Can be changed for a local installation (to make packages).
+  # You must NOT put a "/" at the end (Cygnus for win32 does not like "//").
+
+ifdef COQINSTALLPREFIX
+FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+else
+FULLBINDIR=$(BINDIR)
+FULLCOQLIB=$(COQLIBINSTALL)
+FULLCONFIGDIR=$(CONFIGDIR)
+FULLDATADIR=$(DATADIR)
+FULLMANDIR=$(MANDIR)
+FULLEMACSLIB=$(EMACSLIB)
+FULLCOQDOCDIR=$(COQDOCDIR)
+FULLDOCDIR=$(DOCDIR)
+endif
+
+.PHONY: install-coq install-binaries install-byte install-opt
+.PHONY: install-tools install-library install-devfiles
+.PHONY: install-coq-info install-coq-manpages install-emacs install-latex
+
+install-coq: install-binaries install-library install-coq-info install-devfiles
+
+install-binaries: install-tools
+	$(MKDIR) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
+	$(MKDIR) $(FULLCOQLIB)/toploop
+	$(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/
+ifeq ($(BEST),opt)
+	$(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
+endif
+
+
+install-tools:
+	$(MKDIR) $(FULLBINDIR)
+	# recopie des fichiers de style pour coqide
+	$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
+	touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
+	$(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
+	$(INSTALLBIN) $(TOOLS) $(FULLBINDIR)
+
+# The list of .cmi to install, including the ones obtained
+# from .mli without .ml, and the ones obtained from .ml without .mli
+
+INSTALLCMI = $(sort \
+	$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
+	$(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES)))))
+
+install-devfiles:
+	$(MKDIR) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR)
+	$(MKDIR) $(FULLCOQLIB)
+	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA)
+	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
+ifeq ($(BEST),opt)
+	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
+endif
+
+install-library:
+	$(MKDIR) $(FULLCOQLIB)
+	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
+	$(MKDIR) $(FULLCOQLIB)/user-contrib
+ifndef CUSTOM
+	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
+endif
+ifeq ($(BEST),opt)
+	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
+	$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
+endif
+# csdpcert is not meant to be directly called by the user; we install
+# it with libraries
+	-$(MKDIR) $(FULLCOQLIB)/plugins/micromega
+	$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega
+	rm -f $(FULLCOQLIB)/revision
+	-$(INSTALLLIB) revision $(FULLCOQLIB)
+
+install-coq-info: install-coq-manpages install-emacs install-latex
+
+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/coqchk.1
+
+install-coq-manpages:
+	$(MKDIR) $(FULLMANDIR)/man1
+	$(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1
+
+install-emacs:
+	$(MKDIR) $(FULLEMACSLIB)
+	$(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB)
+
+# command to update TeX' kpathsea database
+#UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null
+
+install-latex:
+	$(MKDIR) $(FULLCOQDOCDIR)
+	$(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
+#	-$(UPDATETEX)
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End: