Yet another Makefile reform : a unique phase without nasty make tricks

 We're back to a unique build phase (as before e372b72), but without
 relying on the awkward include-deps-failed-lets-retry feature of make.
 Since PMP has made grammar/ self-contained, we could now build
 grammar.cma in a rather straightforward way, no need for
 a specific sub-call to $(MAKE) for that. The dependencies between
 files of grammar/ are stated explicitely, since .d files aren't
 fully available initially.

 Some Makefile simplifications, for instance remove the CAMLP4DEPS
 shell horror. Instead, we generalize the use of two different
 filename extensions :
  - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
  - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
    except coqide_main.ml4 and its specific rule

 Note that we do not generate .ml4.d anymore (thanks to the .mlp vs.
 .ml4 dichotomy)

0 files changed, 0 insertions, 0 deletions