|
|
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
|
Pierre Letouzey
Maxime Dénès
herbelin
letouzey