Finish adding out-of-the-box support for camlp4

 If you want to try, it should be now as simple as:

 make clean && ./configure -local -usecamlp4 && make

 For the moment, the default stays camlp5, hence
 ./configure -usecamlp5 and ./configure are equivalent.

 Thanks to a suggestion by N. Pouillard, the remaining
 incompatibilities are now handled via some token filtering in
 camlp4. See compat5*.mlp. Morally, these files should be named .ml4,
 but I prefer having them not in $(...ML4) variables, it might confuse
 the Makefile... The empty compat5*.ml are used to build empty .cmo
 for making camlp5 happy. 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

 TODO: check that my quick adaptation of camlp5-specific code in
 tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur
 is hiding information in the locations ?!

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

0 files changed, 0 insertions, 0 deletions