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

4 files changed, 72 insertions, 0 deletions

diff --git a/tools/compat5.ml b/tools/compat5.ml
new file mode 100644
index 000000000..6a76895cd
--- /dev/null
+++ b/tools/compat5.ml
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This file is meant for camlp5, for which there is nothing to
+   add to gain camlp5 compatibility :-).
+
+   See [compat5.mlp] for the [camlp4] counterpart
+*)
diff --git a/tools/compat5.mlp b/tools/compat5.mlp
new file mode 100644
index 000000000..c3c7e9995
--- /dev/null
+++ b/tools/compat5.mlp
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
+    - GEXTEND ... becomes EXTEND ...
+*)
+
+open Camlp4.PreCast
+
+let rec my_token_filter = parser
+  | [< '(KEYWORD "GEXTEND", loc); s >] ->
+    [< '(KEYWORD "EXTEND", loc); my_token_filter s >]
+  | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
+  | [< >] -> [< >]
+
+let _ =
+  Token.Filter.define_filter (Gram.get_filter())
+    (fun prev strm -> prev (my_token_filter strm))
diff --git a/tools/compat5b.ml b/tools/compat5b.ml
new file mode 100644
index 000000000..03bdb358b
--- /dev/null
+++ b/tools/compat5b.ml
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This file is meant for camlp5, for which there is nothing to
+   add to gain camlp5 compatibility :-).
+
+   See [compat5b.mlp] for the [camlp4] counterpart
+*)
diff --git a/tools/compat5b.mlp b/tools/compat5b.mlp
new file mode 100644
index 000000000..0aa13dd64
--- /dev/null
+++ b/tools/compat5b.mlp
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
+    - EXTEND ... becomes EXTEND Gram ...
+*)
+
+open Camlp4.PreCast
+
+let rec my_token_filter = parser
+  | [< '(KEYWORD "EXTEND",_ as t); s >] ->
+    [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >]
+  | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
+  | [< >] -> [< >]
+
+let _ =
+  Token.Filter.define_filter (Gram.get_filter())
+    (fun prev strm -> prev (my_token_filter strm))