Imported Upstream version 8.6upstream/8.6

1 files changed, 368 insertions, 808 deletions

diff --git a/Makefile.build b/Makefile.build
index 48f448ce..95df69c2 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -10,123 +10,152 @@
 # some variables.
 
 ###########################################################################
-# Starting rule
+# User-customizable variables
 ###########################################################################
 
-# build the different subsystems: coq, coqide
-world: revision coq coqide documentation
+# The following variables could be modified via the command-line of make,
+# either with the syntax 'make XYZ=1' or 'XYZ=1 make'
 
-.PHONY: world
+# To see the actual commands launched by make instead of shortened versions,
+# set this variable to 1 (or any non-empty value):
+VERBOSE ?=
+
+# If set to 1 (or non-empty) then *.ml files corresponding to *.ml4 files
+# will be generated in a human-readable format rather than in a binary format.
+READABLE_ML4 ?=
+
+# When non-empty, a time command is performed at each .v compilation.
+# To collect compilation timings of .v and import them in a spreadsheet,
+# you could hence consider: make TIMED=1 2> timings.csv
+TIMED ?=
+
+# When $(TIMED) is set, the time command used by default is $(STDTIME)
+# (see below), unless the following variable is non-empty. For instance,
+# it could be set to "'/usr/bin/time -p'".
+TIMECMD ?=
+
+# Non-empty skips the update of all dependency .d files:
+NO_RECALC_DEPS ?=
+
+# Non-empty runs the checker on all produced .vo files:
+VALIDATE ?=
+
+# Is "-xml" when building XML library:
+COQ_XML ?=
+
+###########################################################################
+# Default starting rule
+###########################################################################
+
+# build the different subsystems:
+
+world: coq coqide documentation revision
+
+coq: coqlib coqbinaries tools printers
+
+.PHONY: world coq
 
 ###########################################################################
 # Includes
 ###########################################################################
 
+# 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)
+
 include Makefile.common
-include Makefile.doc
+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
 
-# In a first phase, we restrict to the basic .ml4 (the ones without grammar.cma)
+# 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).
 
-ifdef BUILDGRAMMAR
- MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4BASEFILES:.ml4=.ml)
- CURFILES := $(MLFILES) $(MLIFILES) $(ML4BASEFILES) grammar/grammar.mllib
-else
- MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
- CURFILES := $(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(CFILES) $(VFILES)
-endif
+DEPENDENCIES := \
+ $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES))
 
-CURDEPS:=$(addsuffix .d, $(CURFILES))
+-include $(DEPENDENCIES)
 
 # All dependency includes must be declared secondary, otherwise make will
 # delete them if it decided to build them by dependency instead of because
 # of include, and they will then be automatically deleted, leading to an
 # infinite loop.
 
-.SECONDARY: $(CURDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
-
-# This include below will lauch the build of all concerned .d.
-# The - at front is for disabling warnings about currently missing ones.
-
--include $(CURDEPS)
-
+.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml)
 
 ###########################################################################
 # Compilation options
 ###########################################################################
 
-# Variables meant to be modifiable via the command-line of make
-
-VERBOSE=
-NO_RECOMPILE_ML4=
-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)
+# Default timing command
+STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 
-TIMECMD=	# if you prefer a specific time command instead of $(STDTIME)
-                # e.g. "'time -p'"
-CAMLFLAGS:=${CAMLFLAGS} -w -3
-# NB: if you want to collect compilation timings of .v and import them
-# in a spreadsheet, I suggest something like:
-#   make TIMED=1 2> timings.csv
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
 # NB: do not use a variable named TIME, since this variable controls
 # the output format of the unix command time. For instance:
 #   TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
-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 
-# or only abbreviated versions. 
-# Quiet mode is ON by default except if VERBOSE=1 option is given to make
-
-SHOW := $(if $(VERBOSE),@true "",@echo "")
-HIDE := $(if $(VERBOSE),,@)
-
 LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
-OCAMLC := $(OCAMLC) $(CAMLFLAGS)
-OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS)
+OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
+OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
 
 BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
 DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils
 
+# On MacOS, the binaries are signed, except our private ones
 ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
-LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist"
-CODESIGN:=codesign -s -
+LINKMETADATA=$(if $(filter $(PRIVATEBINARIES),$@),,-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist")
+CODESIGN=$(if $(filter $(PRIVATEBINARIES),$@),true,codesign -s -)
 else
 LINKMETADATA=
-CODESIGN:=true
+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),\
-$(if $(findstring $@,$(PRIVATEBINARIES)),\
-  $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\
-  $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@),\
+$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@,\
 $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
 endef
 
-CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#))
+# Camlp4 / Camlp5 settings
+
+CAMLP4DEPS:=grammar/compat5.cmo grammar/grammar.cma
 ifeq ($(CAMLP4),camlp5)
 CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
 else
 CAMLP4USE=-D$(CAMLVERSION)
 endif
 
-CAMLP4FLAGS=-I $(CAMLLIB) -I $(CAMLLIB)/threads -I $(MYCAMLP4LIB) unix.cma threads.cma
-
-PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4
+PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo)
 
 SYSMOD:=str unix dynlink threads
 SYSCMA:=$(addsuffix .cma,$(SYSMOD))
@@ -139,11 +168,17 @@ else
 P4CMA:=camlp4lib.cma
 endif
 
-
 ###########################################################################
 # Infrastructure for the rest of the Makefile
 ###########################################################################
 
+# The SHOW and HIDE variables control whether make will echo complete commands
+# or only abbreviated versions.
+# Quiet mode is ON by default except if VERBOSE=1 option is given to make
+
+SHOW := $(if $(VERBOSE),@true "",@echo "")
+HIDE := $(if $(VERBOSE),,@)
+
 define order-only-template
  ifeq "order-only" "$(1)"
    ORDER_ONLY_SEP:=|
@@ -164,13 +199,8 @@ ifdef VALIDATE
  VO_TOOLS_DEP += $(CHICKEN)
 endif
 
-ifdef NO_RECALC_DEPS
-  D_DEPEND_BEFORE_SRC:=|
-  D_DEPEND_AFTER_SRC:=
-else
-  D_DEPEND_BEFORE_SRC:=
-  D_DEPEND_AFTER_SRC:=|
-endif
+D_DEPEND_BEFORE_SRC := $(if $(NO_RECALC_DEPS),|,)
+D_DEPEND_AFTER_SRC := $(if $(NO_RECALC_DEPS),,|)
 
 ## When a rule redirects stdout of a command to the target file : cmd > $@
 ## then the target file will be created even if cmd has failed.
@@ -180,21 +210,18 @@ 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
 
-$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) 
+$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
 	cd $(dir $(LIBCOQRUN)) && \
-	$(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
+	$(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)
@@ -203,777 +230,315 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
 	sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' $< | \
 	awk -f kernel/make-opcodes $(TOTARGET)
 
-###########################################################################
-# Main targets (coqmktop, coqtop.opt, coqtop.byte)
-###########################################################################
-
-.PHONY: coqbinaries coq coqlib coqlight states
-
-coqbinaries: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE}
-
-coq: coqlib tools coqbinaries
-
-coqlib: theories plugins
-
-coqlight: theories-light tools coqbinaries
-
-states: theories/Init/Prelude.vo
+%.o: %.c
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<)
 
-miniopt: $(COQTOPEXE) pluginsopt
-minibyte: $(COQTOPBYTE) pluginsbyte
+%_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC)
+	$(SHOW)'CCDEP	$<'
+	$(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@
 
-ifeq ($(BEST),opt)
-$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
-	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -thread -o $@
-	$(STRIP) $@
-	$(CODESIGN) $@
-else
-$(COQTOPEXE): $(COQTOPBYTE)
-	cp $< $@
-endif
+%.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)
 
-$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA)
-	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@
+###########################################################################
+### Special rules (Camlp5 / Camlp4)
+###########################################################################
 
-LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) )
-CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB)
+# Special rule for the compatibility-with-camlp5 extension for camlp4
+#
+# - grammar/compat5.cmo changes 'GEXTEND' into 'EXTEND'. Safe, always loaded
+# - grammar/compat5b.cmo changes 'EXTEND' into 'EXTEND Gram'. Interact badly with
+#    syntax such that 'VERNAC EXTEND', we only load it in grammar/
 
-ifeq ($(BEST),opt)
-$(CHICKEN): checker/check.cmxa checker/main.ml
-	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ $(SYSCMXA) $^
-	$(STRIP) $@
-	$(CODESIGN) $@
+ifeq ($(CAMLP4),camlp4)
+grammar/compat5.cmo: grammar/compat5.mlp
+	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) -impl' -impl $<
+grammar/compat5b.cmo: grammar/compat5b.mlp
+	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) -impl' -impl $<
 else
-$(CHICKEN): $(CHICKENBYTE)
-	cp $< $@
+grammar/compat5.cmo: grammar/compat5.ml
+	$(OCAMLC) -c $<
 endif
 
-$(CHICKENBYTE): checker/check.cma checker/main.ml
-	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -thread -o $@ $(SYSCMA) $^
-
-# coqmktop
-$(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ)))
-	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
-
-tools/tolink.ml: Makefile.build Makefile.common
-	$(SHOW)"ECHO... >" $@
-	$(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@
-	$(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@
-	$(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: | %.mllib.d
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $^
-
-%.cmxa: | %.mllib.d
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $^
-
-# For the checker, different flags may be used
-
-checker/check.cma: | md5chk checker/check.mllib.d
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $^
-
-checker/check.cmxa: | md5chk checker/check.mllib.d
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $^
-
 ###########################################################################
-# Csdp to micromega special targets
+#  grammar/grammar.cma
 ###########################################################################
 
-plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ))  \
-		$(addsuffix $(BESTLIB), lib/clib)
-	$(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
+## In this part, we compile grammar/grammar.cma
+## without relying on .d dependency files, for bootstraping the creation
+## and inclusion of these .d files
 
-COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
+## Explicit dependencies for grammar stuff
 
-.SUFFIXES:.vo
+GRAMBASEDEPS := grammar/gramCompat.cmo grammar/q_util.cmi
+GRAMCMO := grammar/gramCompat.cmo grammar/q_util.cmo \
+ grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo
 
-IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
+grammar/q_util.cmi : grammar/gramCompat.cmo
+grammar/argextend.cmo : $(GRAMBASEDEPS)
+grammar/q_util.cmo : $(GRAMBASEDEPS)
+grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo
+grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \
+ grammar/argextend.cmo
 
-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
+## Ocaml compiler with the right options and -I for grammar
 
-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
+GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \
+ -I $(MYCAMLP4LIB) -I grammar
 
-$(COQIDEBYTE): $(LINKIDE)
-	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \
-	        lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^
+## Specific rules for grammar.cma
 
-# install targets
+grammar/grammar.cma : $(GRAMCMO)
+	$(SHOW)'Testing $@'
+	@touch grammar/test.mlp
+	$(HIDE)$(GRAMC) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test
+	@rm -f grammar/test.* grammar/test
+	$(SHOW)'OCAMLC -a $@'   
+	$(HIDE)$(GRAMC) $^ -linkall -a -o $@
 
-.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
+## Support of Camlp5 and Camlp5
 
-ifeq ($(HASCOQIDE),no)
-install-coqide: install-ide-toploop
+ifeq ($(CAMLP4),camlp4)
+ COMPATCMO:=grammar/compat5.cmo grammar/compat5b.cmo
+ GRAMP4USE:=$(COMPATCMO) -D$(CAMLVERSION)
+ GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl
 else
-install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
+ COMPATCMO:=
+ GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
+ GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl
 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
+## Rules for standard .mlp and .mli files in grammar/
 
-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
+grammar/%.cmo: grammar/%.mlp | $(COMPATCMO)
+	$(SHOW)'OCAMLC -c -pp $<'
+	$(HIDE)$(GRAMC) -c -pp '$(GRAMPP)' -impl $<
 
-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
+grammar/%.cmi: grammar/%.mli
+	$(SHOW)'OCAMLC -c $<'
+	$(HIDE)$(GRAMC) -c $<
 
-install-ide-info:
-	$(MKDIR) $(FULLDOCDIR)
-	$(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde
 
 ###########################################################################
-# CoqIde MacOS special targets
+# Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
 
-.PHONY: $(COQIDEAPP)/Contents
+.PHONY: coqbinaries
 
-$(COQIDEAPP)/Contents:
-	rm -rdf $@
-	$(MKDIR) $@
-	sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist
-	$(MKDIR) "$@/MacOS"
+coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \
+ $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE)
 
-$(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
+ifeq ($(BEST),opt)
+$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
+	$(SHOW)'COQMKTOP -o $@'	
+	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@
+	$(STRIP) $@
 	$(CODESIGN) $@
+else
+$(COQTOPEXE): $(COQTOPBYTE)
+	cp $< $@
+endif
 
-###########################################################################
-# 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: highparsing stm toplevel hightactics
-
-lib: lib/clib.cma lib/lib.cma
-kernel: kernel/kernel.cma
-byterun: $(BYTERUN)
-library: library/library.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
-hightactics: tactics/hightactics.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)
+$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA)
+	$(SHOW)'COQMKTOP -o $@'	
+	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@
 
-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
+# coqmktop
 
-###########################################################################
-# 3) plugins
-###########################################################################
+COQMKTOPCMO:=lib/clib.cma lib/cErrors.cmo tools/tolink.cmo tools/coqmktop.cmo
 
-.PHONY: plugins omega micromega setoid_ring nsatz extraction
-.PHONY: fourier funind cc rtauto btauto pluginsopt pluginsbyte
+$(COQMKTOP): $(call bestobj, $(COQMKTOPCMO))
+	$(SHOW)'OCAMLBEST -o $@'
+	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
 
-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)
+tools/tolink.ml: Makefile.build Makefile.common
+	$(SHOW)"ECHO... >" $@
+	$(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@
+	$(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@
+	$(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@
 
-###########################################################################
-# rules to make theories and plugins
-###########################################################################
+# coqc
 
-theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
-	$(SHOW)'COQC $(COQ_XML) -noinit $<'
-	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq
+COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo
 
-theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
-	$(OCAML) $< $(TOTARGET)
+$(COQC): $(call bestobj, $(COQCCMO))
+	$(SHOW)'OCAMLBEST -o $@'
+	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
 
 ###########################################################################
-# tools
+# other tools
 ###########################################################################
 
-.PHONY: printers tools
-
-printers: $(DEBUGPRINTERS)
-
-tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)
+.PHONY: tools
+tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT)
 
 # coqdep_boot : a basic version of coqdep, with almost no dependencies.
+# We state these dependencies here explicitly, since some .ml.d files
+# may still be missing or not taken in account yet by make when coqdep_boot
+# is being built.
 
-# Here it is important to mention .ml files instead of .cmo in order
-# to avoid using implicit rules and hence .ml.d files that would need
-# coqdep_boot.
+COQDEPBOOTSRC := lib/minisys.cmo \
+ tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep_boot.cmo
 
-COQDEPBOOTSRC:= \
-  tools/coqdep_lexer.mli tools/coqdep_lexer.ml \
-  tools/coqdep_common.mli tools/coqdep_common.ml \
-  tools/coqdep_boot.ml
+tools/coqdep_lexer.cmo : tools/coqdep_lexer.cmi
+tools/coqdep_lexer.cmx : tools/coqdep_lexer.cmi
+tools/coqdep_common.cmo : lib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi
+tools/coqdep_common.cmx : lib/minisys.cmx tools/coqdep_lexer.cmx tools/coqdep_common.cmi
+tools/coqdep_boot.cmo : tools/coqdep_common.cmi
+tools/coqdep_boot.cmx : tools/coqdep_common.cmx
 
-$(COQDEPBOOT): $(COQDEPBOOTSRC)
+$(COQDEPBOOT): $(call bestobj, $(COQDEPBOOTSRC))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I tools, unix)
 
-# the full coqdep
+$(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo)
+	$(SHOW)'OCAMLBEST -o $@'
+	$(HIDE)$(call bestocaml, -I tools, unix)
 
-$(COQDEP): $(patsubst %.cma,%$(BESTLIB),$(COQDEPCMO:.cmo=$(BESTOBJ)))
+# The full coqdep (unused by this build, but distributed by make install)
+
+COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.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/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
+FAKEIDECMO:= lib/clib.cma lib/cErrors.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.cmo)
 	$(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 $<
-tools/compat5b.cmo: tools/compat5b.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
-
-#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
+.PHONY: validate check test-suite $(ALLSTDLIB).v
 
-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)
+# Default rules for compiling ML code
 ###########################################################################
 
-.PHONY: source-doc mli-doc ml-doc
-
-source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
-
-$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
-	$(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
-	$(DOCMLIS) -t "Coq mlis documentation" \
-	-intro $(OCAMLDOCDIR)/docintro -o $@
-
-mli-doc: $(DOCMLIS:.mli=.cmi)
-	$(OCAMLDOC) -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)
-	$(OCAMLDOC) -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \
-	$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
+# Target for libraries .cma and .cmxa
 
-%_dep.png: %.dot
-	$(DOT) -Tpng $< -o $@
+# 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.
 
-%_types.dot: %.mli
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< 
-
-OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
-  $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
-
-%.dot: | %.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-ml-doc:
-	$(OCAMLDOC) -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 tactics/hightactics.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-%.dot: %.mli
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< 
-
-$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
-	(cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex)
-
-###########################################################################
-### Special rules
-###########################################################################
+%.cma: %.mllib
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
-dev/printers.cma: | dev/printers.mllib.d
-	$(SHOW)'Testing $@'
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $^ -o test-printer
-	@rm -f test-printer
-	$(SHOW)'OCAMLC -a $@'   
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $^ -linkall -a -o $@
+%.cmxa: %.mllib
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
-grammar/grammar.cma: | grammar/grammar.mllib.d
-	$(SHOW)'Testing $@'
-	@touch test.ml4
-	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $^ -impl test.ml4 -o test.ml
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) test.ml -o test-grammar
-	@rm -f test-grammar test.*
-	$(SHOW)'OCAMLC -a $@'   
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $^ -linkall -a -o $@
+# For plugin packs
 
-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
+# Note: both ocamlc -pack and ocamlopt -pack will create the same .cmi, and there's
+# apparently no way to avoid that (no -intf-suffix hack as below).
+# We at least ensure that these two commands won't run at the same time, by a fake
+# dependency from the packed .cmx to the packed .cmo.
 
-###########################################################################
-# Default rules
-###########################################################################
+%.cmo: %.mlpack
+	$(SHOW)'OCAMLC -pack -o $@'
+	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
 
-## Three flavor of flags: checker/* ide/* and normal files
+%.cmx: %.mlpack %.cmo
+	$(SHOW)'OCAMLOPT -pack -o $@'
+	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack %.cmo, $^)
 
 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 | %.mli.d
+%.cmi: %.mli
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
 
-%.cmo: %.ml | %.ml.d
+%.cmo: %.ml
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
 
@@ -998,125 +563,120 @@ $(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi  # for .ml with .mli this is already the
 
 $(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo
 
-%.cmx: %.ml | %.ml.d
+# NB: the *_FORPACK variables are generated in *.mlpack.d by ocamllibdep
+# The only exceptions are the sources of the csdpcert binary.
+# To avoid warnings, we set them manually here:
+plugins/micromega/sos_lib_FORPACK:=
+plugins/micromega/sos_FORPACK:=
+plugins/micromega/sos_print_FORPACK:=
+plugins/micromega/csdpcert_FORPACK:=
+
+plugins/%.cmx: plugins/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $<
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<
 
-%.cmxs: %.cmxa
-	$(SHOW)'OCAMLOPT -shared -o $@'
-ifeq ($(HASNATDYNLINK),os5fixme)
-	$(HIDE)dev/ocamlopt_shared_os5fix.sh "$(OCAMLOPT)" $@
-else
-	$(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
-endif
+%.cmx: %.ml
+	$(SHOW)'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $<
 
 %.cmxs: %.cmx
 	$(SHOW)'OCAMLOPT -shared -o $@'
 	$(HIDE)$(OCAMLOPT) -shared -o $@ $<
 
+%.cmxs: %.cmxa
+	$(SHOW)'OCAMLOPT -shared -o $@'
+	$(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
+
 %.ml: %.mll
 	$(SHOW)'OCAMLLEX  $<'
 	$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
 
-%.ml %.mli: %.mly
-	$(SHOW)'OCAMLYACC $<'
-	$(HIDE)$(OCAMLYACC) $<
-
-plugins/%_mod.ml: plugins/%.mllib
-	$(SHOW)'ECHO... > $@'
-	$(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
-	$(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@
-
-# NB: compatibility modules for camlp4: 
-# - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
-# - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
-#    syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps
-
-%.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo
+%.ml: %.ml4 | $(CAMLP4DEPS)
 	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) tools/compat5.cmo \
-	  $(call CAMLP4DEPS,$<) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
+	$(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) \
+	  $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
 
-%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
-	$(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
 ###########################################################################
 
-# .ml4.d contains the dependencies to generate the .ml from the .ml4
-# NOT to generate object code.
+# Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12)
+OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
 
-%.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
-	$(SHOW)'CAMLP4DEPS $<'
-	$(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(call CAMLP4DEPS,$<)" $(TOTARGET)
+%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES)
+	$(SHOW)'OCAMLDEP  $<'
+	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
-# Since OCaml 3.12.1, we could use again ocamldep directly, thanks to
-# the option -ml-synonym
+%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES)
+	$(SHOW)'OCAMLDEP  $<'
+	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
-OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4
+%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES)
+	$(SHOW)'OCAMLLIBDEP  $<'
+	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
-checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET)
+%.mlpack.d: $(D_DEPEND_BEFORE_SRC) %.mlpack $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES)
+	$(SHOW)'OCAMLLIBDEP  $<'
+	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
-checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET)
+###########################################################################
+# Compilation of .v files
+###########################################################################
 
-%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
+# 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
 
-%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
+coqlib: theories plugins
 
-checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
-	$(SHOW)'COQDEP  $<'
-	$(HIDE)$(COQDEPBOOT) -I checker -c "$<" $(TOTARGET)
+theories: $(THEORIESVO)
+plugins: $(PLUGINSVO)
 
-%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
-	$(SHOW)'COQDEP  $<'
-	$(HIDE)$(COQDEPBOOT) -I kernel -I tools/coqdoc -c "$<" $(TOTARGET)
+.PHONY: coqlib theories plugins
 
-%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
-	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEPBOOT) $(DEPNATDYN) "$<" $(TOTARGET)
+# One of the .v files is macro-generated
 
-%_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC)
-	$(SHOW)'CCDEP	$<'
-	$(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@
+theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
+	$(OCAML) $< $(TOTARGET)
 
-%.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)
+# The .vo files in Init are built with the -noinit option
 
-###########################################################################
-# this sets up developper supporting stuff
-###########################################################################
+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
 
-.PHONY: devel otags
-devel: $(DEBUGPRINTERS)
+# The general rule for building .vo files :
 
-otags:
-	otags $(MLIFILES) $(MLSTATICFILES) \
-	$(foreach i,$(ML4FILES),-pc -pa tools/compat5.cmo -pa op -pa g -pa m -pa rq $(patsubst %,-pa %,$(call CAMLP4DEPS,$i)) -impl $i)
+%.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 : ;
+
+# Final catch-all rule.
+# Usually, 'make' would display such an error itself.
+# But if the target has some declared dependencies (e.g. in a .d)
+# but no building rule, 'make' succeeds silently (see bug #4812).
 
+%:
+	@echo "Error: no rule to make target $@ (or missing .PHONY)" && false
 
 # For emacs: 
 # Local Variables: