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

10 files changed, 108 insertions, 8 deletions

diff --git a/Makefile.build b/Makefile.build
index adba237537..0540b9a9ae 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -499,6 +499,20 @@ $(COQDOC): $(COQDOCCMO:.cmo=$(BESTOBJ))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,str unix)
 
+# Special rule for the compatibility-with-camlp5 extension for camlp4
+
+ifeq ($(CAMLP4),camlp4)
+tools/compat5.cmo: tools/compat5.mlp
+	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $<
+tools/compat5b.cmo: tools/compat5b.mlp
+	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $<
+else
+tools/compat5.cmo: tools/compat5.ml
+	$(OCAMLC) -c $<
+tools/compat5b.cmo: tools/compat5b.ml
+	$(OCAMLC) -c $<
+endif
+
 ###########################################################################
 # Installation
 ###########################################################################
@@ -673,11 +687,11 @@ toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml
 
 toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< $(TOTARGET)
+	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@
 
 toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< $(TOTARGET)
+	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@
 
 # pretty printing of the revision number when compiling a checked out
 # source tree
@@ -796,12 +810,17 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
 	$(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@
 
-%.ml: %.ml4 | %.ml4.d
+# NB: compatibility modules 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
+
+%.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)\
 	DEPS=$(CAMLP4DEPS); \
 	if ls $${DEPS} > /dev/null 2>&1; then \
-	$(CAMLP4O) $(PR_O) -I $(CAMLLIB) $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< $(TOTARGET); \
+	$(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \
 	else echo $< : Dependency $${DEPS} not ready yet; false; fi
 
 %.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index e156bdc266..fc1f05dad2 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4deps: "tools/compat5b.cmo" i*)
+
 open Genarg
 open Q_util
 open Egrammar
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index fb34a5aa27..43f4559246 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4deps: "tools/compat5b.cmo" i*)
+
 open Rawterm
 open Term
 open Names
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index f64c8f700c..3aac36c08a 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4deps: "tools/compat5b.cmo" i*)
+
 open Util
 open Genarg
 open Q_util
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 1fa0e7e99b..9ed89536c5 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4deps: "tools/compat5b.cmo" i*)
+
 open Util
 open Genarg
 open Q_util
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0ddb4da755..e71e6366ca 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -21,6 +21,7 @@ open Util
 open Termops
 open Evd
 open Equality
+open Compat
 
 (**********************************************************************)
 (* replace, discriminate, injection, simplify_eq                      *)
@@ -543,7 +544,7 @@ let subst_var_with_hole occ tid t =
     | RVar (_,id) as x -> 
         if id = tid 
         then (decr occref; if !occref = 0 then x
-                           else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true))))
+                           else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))))
         else x
     | c -> map_rawconstr_left_to_right substrec c in
   let t' = substrec t
@@ -556,7 +557,7 @@ let subst_hole_with_term occ tc t =
   let rec substrec = function
     | RHole (_,Evd.QuestionMark(Evd.Define true)) -> 
         decr occref; if !occref = 0 then tc
-                     else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true)))
+                     else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))
     | c -> map_rawconstr_left_to_right substrec c
   in
   substrec t
@@ -578,8 +579,8 @@ let hResolve id c occ t gl =
     try 
       Pretyping.Default.understand sigma env t_hole
     with 
-    | Ploc.Exc (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> 
-        resolve_hole (subst_hole_with_term (Ploc.line_nb loc) c_raw t_hole)
+    | Loc.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
+        resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
   in
   let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
diff --git a/tools/compat5.ml b/tools/compat5.ml
new file mode 100644
index 0000000000..6a76895cd9
--- /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 0000000000..c3c7e9995f
--- /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 0000000000..03bdb358b0
--- /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 0000000000..0aa13dd640
--- /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))