Makefile: the initial build of grammar.cma is now directory-driven

 In last commit, we used grep to decide whether a .ml4 could be
 compiled during the initial phase of not. Instead, we now rely on
 a simpler directory dichotomy:

 - config lib kernel library pretyping interp parsing grammar
   are considered initial (and shouldn't contain grammar-dependent .ml4),
   see $(GRAMSRCDIRS) in Makefile.common

 - the grammar-dependent .ml4 could be in any other directories
   Currently, they are in: tactics toplevel plugins/*

3 files changed, 22 insertions, 19 deletions

diff --git a/Makefile b/Makefile
index 5f5397fa7..109196bea 100644
--- a/Makefile
+++ b/Makefile
@@ -59,20 +59,11 @@ define find
  $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||')
 endef
 
-define findx
- $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||')
-endef
-
-# We now discriminate .ml4 files according to their need of grammar.cma
-# or q_constr.cmo
-USEGRAMMAR := '(\*.*camlp4deps.*grammar'
-
 ## Files in the source tree
 
 YACCFILES:=$(call find, '*.mly')
 LEXFILES := $(call find, '*.mll')
 export MLLIBFILES := $(call find, '*.mllib')
-export ML4BASEFILES := $(call findx, '*.ml4', grep -L -e $(USEGRAMMAR))
 export ML4FILES := $(call find, '*.ml4')
 export CFILES := $(call find, '*.c')
 
diff --git a/Makefile.build b/Makefile.build
index 760a4db72..f8895b2ed 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -25,13 +25,20 @@ world: revision coq coqide documentation
 include Makefile.common
 include Makefile.doc
 
-# In a first phase, we restrict to the basic .ml4 (the ones without grammar.cma)
+MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
+
+# In a first phase (when BUILDGRAMMAR=1), we restrict the considered
+# files to some specific directories (up to grammar/), not considering
+# the grammar-dependent .ml4 (which are in tactics/ toplevel/ plugins/)
+
+GRAMONLY := $(addsuffix /%,$(GRAMSRCDIRS))
 
 ifdef BUILDGRAMMAR
- MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4BASEFILES:.ml4=.ml)
- CURFILES := $(MLFILES) $(MLIFILES) $(ML4BASEFILES) grammar/grammar.mllib
+ CURSRCDIRS := $(GRAMSRCDIRS)
+ CURFILES := \
+  $(filter $(GRAMONLY), $(MLFILES) $(MLIFILES) $(ML4FILES)) grammar/grammar.mllib
 else
- MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
+ CURSRCDIRS := $(SRCDIRS)
  CURFILES := $(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(CFILES) $(VFILES)
 endif
 
@@ -91,7 +98,7 @@ BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 SHOW := $(if $(VERBOSE),@true "",@echo "")
 HIDE := $(if $(VERBOSE),,@)
 
-LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
+LOCALINCLUDES := $(addprefix -I , $(CURSRCDIRS) )
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
 OCAMLC := $(OCAMLC) $(CAMLFLAGS)
diff --git a/Makefile.common b/Makefile.common
index 966829d5a..ceafbf474 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -59,16 +59,21 @@ COQBINARIES:= $(COQMKTOP) $(COQC) \
 
 CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 
-CORESRCDIRS:=\
-  config 	lib		kernel		kernel/byterun	library \
-  proofs 	tactics 	pretyping	interp		toplevel \
-  parsing	printing	grammar	        intf
+# Minimal set of source directories for building grammar.cma
+# Invariant: the .ml4 there shouldn't use grammar.cma
+# (the grammar-dependent .ml4 are in tactics, toplevel, plugins)
+GRAMSRCDIRS:=\
+  config     lib     intf    kernel   kernel/byterun  library \
+  pretyping  interp  proofs  parsing  grammar
+
+CORESRCDIRS:= $(GRAMSRCDIRS)  printing  tactics  toplevel
 
 PLUGINS:=\
   omega		romega 		micromega 	quote \
   setoid_ring 	xml 		extraction 	fourier \
   cc 		funind 		firstorder 	Derive \
-  rtauto 	nsatz           syntax          decl_mode	btauto
+  rtauto 	nsatz           syntax          decl_mode \
+  btauto
 
 SRCDIRS:=\
   $(CORESRCDIRS)  \