Makefile: minor improvements

 * no need anymore for special rules for -rectypes: we use it everywhere
 * $(REVISIONCMO) is obsolete
 * avoid triple references to almost all files of kernel/

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

2 files changed, 14 insertions, 41 deletions

diff --git a/Makefile.build b/Makefile.build
index ea2fad128..5d5ff8533 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -768,21 +768,6 @@ toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
 	  $(NATDYNLINKDEF) -impl $< > $@ \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
-# files compiled with -rectypes
-
-define rectypes-rules-template
-$(1:.ml=.cmo): $(1) | $(1).d
-	$(SHOW)'OCAMLC   -rectypes $$<' 
-	$(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $$<
-
-$(1:.ml=.cmx): $(1) | $(1).d
-	$(SHOW)'OCAMLOPT -rectypes $$<'
-	$(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $$<
-
-endef
-
-$(foreach f,$(RECTYPESML),$(eval $(call rectypes-rules-template,$(f))))
-
 # pretty printing of the revision number when compiling a checked out
 # source tree
 .PHONY: revision
diff --git a/Makefile.common b/Makefile.common
index 5a981ae12..ce1fad6b2 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -153,16 +153,20 @@ LIBREP:=$(addprefix lib/, \
 BYTERUN:=$(addprefix kernel/byterun/, \
   coq_fix_code.o coq_memory.o coq_values.o coq_interp.o )
 
-KERNEL:=$(addprefix kernel/, \
+KERNEL0:=$(addprefix kernel/, \
   names.cmo 		univ.cmo 	esubst.cmo 	term.cmo \
   mod_subst.cmo		sign.cmo	cbytecodes.cmo	copcodes.cmo \
-  cemitcodes.cmo	vm.cmo		declarations.cmo \
+  cemitcodes.cmo	declarations.cmo \
   retroknowledge.cmo	pre_env.cmo	cbytegen.cmo 	environ.cmo \
-  csymtable.cmo 	conv_oracle.cmo	closure.cmo	reduction.cmo \
+  conv_oracle.cmo	closure.cmo	reduction.cmo \
   type_errors.cmo	entries.cmo	modops.cmo	inductive.cmo \
-  vconv.cmo		typeops.cmo 	indtypes.cmo	cooking.cmo \
+  typeops.cmo 		indtypes.cmo	cooking.cmo \
   term_typing.cmo	subtyping.cmo	mod_typing.cmo	safe_typing.cmo )
 
+KERNEL1:=$(addprefix kernel/, vm.cmo csymtable.cmo vconv.cmo )
+
+KERNEL:=$(KERNEL0) $(KERNEL1)
+
 LIBRARY:=$(addprefix library/, \
   nameops.cmo		libnames.cmo	libobject.cmo 	summary.cmo \
   nametab.cmo		global.cmo	lib.cmo		declaremods.cmo	\
@@ -223,7 +227,7 @@ TOPLEVEL:=\
   toplevel/vernacinterp.cmo toplevel/mltop.cmo \
   toplevel/vernacentries.cmo toplevel/whelp.cmo toplevel/vernac.cmo \
   toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \
-  toplevel/toplevel.cmo $(REVISIONCMO) toplevel/usage.cmo \
+  toplevel/toplevel.cmo toplevel/usage.cmo \
   toplevel/coqinit.cmo toplevel/coqtop.cmo
 
 HIGHTACTICS:=$(addprefix tactics/, \
@@ -311,7 +315,7 @@ COQENVCMO:=$(CONFIG) \
 COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo 
 COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx)
 
-COQCCMO:=$(COQENVCMO) $(REVISIONCMO) toplevel/usage.cmo scripts/coqc.cmo
+COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo
 COQCCMX:=$(COQCCMO:.cmo=.cmx)
 
 ## Pcoq tools : coq-interface, coq-parser
@@ -380,13 +384,7 @@ GRAMMARNEEDEDCMO:=\
   $(addprefix lib/, \
     pp_control.cmo pp.cmo compat.cmo flags.cmo util.cmo \
     bigint.cmo dyn.cmo hashcons.cmo predicate.cmo rtree.cmo option.cmo ) \
-  $(addprefix kernel/, \
-    names.cmo univ.cmo esubst.cmo term.cmo mod_subst.cmo sign.cmo \
-    cbytecodes.cmo copcodes.cmo cemitcodes.cmo declarations.cmo \
-    retroknowledge.cmo pre_env.cmo cbytegen.cmo conv_oracle.cmo \
-    environ.cmo closure.cmo reduction.cmo type_errors.cmo entries.cmo \
-    modops.cmo inductive.cmo typeops.cmo indtypes.cmo cooking.cmo \
-    term_typing.cmo subtyping.cmo mod_typing.cmo safe_typing.cmo ) \
+  $(KERNEL0) \
   $(addprefix library/, \
     nameops.cmo libnames.cmo summary.cmo nametab.cmo libobject.cmo \
     lib.cmo goptions.cmo decl_kinds.cmo global.cmo ) \
@@ -405,7 +403,7 @@ CAMLP4EXTENSIONSCMO:=\
 GRAMMARSCMO:=$(addprefix parsing/, \
   g_prim.cmo g_tactic.cmo g_ltac.cmo g_constr.cmo )
 
-GRAMMARCMO:=config/coq_config.cmo $(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO)
+GRAMMARCMO:=$(CONFIG) $(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO)
 
 GRAMMARCMA:=parsing/grammar.cma
 
@@ -420,14 +418,8 @@ STAGE1_CMO:=$(GRAMMARCMO) parsing/q_constr.cmo
 STAGE1:=parsing/grammar.cma parsing/q_constr.cmo
 
 PRINTERSCMO:=\
-  config/coq_config.cmo lib/lib.cma \
-  $(addprefix kernel/, \
-    names.cmo univ.cmo esubst.cmo term.cmo mod_subst.cmo sign.cmo \
-    cbytecodes.cmo copcodes.cmo cemitcodes.cmo declarations.cmo \
-    retroknowledge.cmo pre_env.cmo cbytegen.cmo conv_oracle.cmo \
-    environ.cmo closure.cmo reduction.cmo type_errors.cmo entries.cmo \
-    modops.cmo inductive.cmo typeops.cmo indtypes.cmo cooking.cmo \
-    term_typing.cmo subtyping.cmo mod_typing.cmo safe_typing.cmo ) \
+  $(CONFIG) lib/lib.cma \
+  $(KERNEL0) \
   $(addprefix library/, \
     summary.cmo global.cmo nameops.cmo libnames.cmo nametab.cmo \
     libobject.cmo lib.cmo goptions.cmo decls.cmo heads.cmo ) \
@@ -777,10 +769,6 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 
 PCOQMANPAGES:=man/coq-interface.1 man/coq-parser.1
 
-RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \
-  parsing/pptactic.ml 
-
-
 #########################################################
 # .mli files by directory (used for dependencies graphs #
 #########################################################