Generalized CAMLP4USE for pp dependencies

Removed parsing/lexer.ml4 special case
No file depends on pa_extend_m.cmo anymore, Wierd ...


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

20 files changed, 54 insertions, 23 deletions

diff --git a/Makefile.build b/Makefile.build
index bac86b6cdd..26a77d7aba 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -79,9 +79,9 @@ DEPFLAGS=$(LOCALINCLUDES)
 
 OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS)
 OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS)
-CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo q_MLast.cmo
+CAMLP4EXTENDFLAGS=-I . #grammar dependencies are now in camlp4use statements 
 CAMLP4DEPS=sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*\*)@\1@p'
-CAMLP4USE=sed -n -e 's@^(\*.*camlp4\(deps\|use\): "\(.*\)".*\*)@\2@p'
+CAMLP4USE=sed -n -e 's@^(\*.*camlp4use: "\(.*\)".*\*)@\1@p'
 
 COQINCLUDES=          # coqtop includes itself the needed paths
 COQ_XML=	# is "-xml" when building XML library
@@ -702,11 +702,11 @@ toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml4.ml.d toplevel/mlto
 ## In other words, the Byte-only code doesn't import a new module.
 toplevel/mltop.byteml: toplevel/mltop.ml4 # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'	
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -DByte -impl $< > $@
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` -DByte -impl $< > $@
 
 toplevel/mltop.optml: toplevel/mltop.ml4 # no camlp4deps here 
 	$(SHOW)'CAMLP4O   $<'	
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -impl $< > $@
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` -impl $< > $@
 
 # files compiled with -rectypes
 
@@ -723,17 +723,6 @@ endef
 
 $(foreach f,$(RECTYPESML),$(eval $(call rectypes-rules-template,$(f))))
 
-# Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with
-# ast-based camlp4
-
-parsing/lexer.cmx: parsing/lexer.ml4 | parsing/lexer.ml4.ml.d parsing/lexer.ml4.d
-	$(SHOW)'OCAMLOPT4 $<'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -impl" -c -impl $<
-
-parsing/lexer.cmo: parsing/lexer.ml4 | parsing/lexer.ml4.ml.d parsing/lexer.ml4.d
-	$(SHOW)'OCAMLC4   $<'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -impl" -c -impl $<
-
 # pretty printing of the revision number when compiling a checked out
 # source tree
 .PHONY: revision
@@ -780,7 +769,7 @@ endif
 
 %.cmo: %.ml4 | %.ml4.ml.d %.ml4.d
 	$(SHOW)'OCAMLC4   $<'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
 
 %.cmo: %.ml | %.ml.d
 	$(SHOW)'OCAMLC    $<'
@@ -792,7 +781,7 @@ endif
 
 %.cmx: %.ml4 | %.ml4.ml.d %.ml4.d
 	$(SHOW)'OCAMLOPT4 $<'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
 
 %.cmx: %.ml | %.ml.d
 	$(SHOW)'OCAMLOPT  $<'
@@ -808,7 +797,7 @@ endif
 
 %.ml4.preprocessed: %.ml4 | %.ml4.d
 	$(SHOW)'CAMLP4O $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` $(CAMLP4COMPAT) -impl $< > $@
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@
 
 %.vo %.glob: %.v states/initial.coq $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
 	$(SHOW)'COQC      $<'
@@ -830,7 +819,7 @@ endif
 #Critical section:
 # Nobody (in a make -j) should touch the .ml file here.
 	$(SHOW)'OCAMLDEP4 $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` $(CAMLP4COMPAT) -impl $< > $*.ml
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $*.ml
 	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml > "$@"
 	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml
 #End critical section
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index f6aad378d8..72b609b24d 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -11,6 +11,7 @@
 (* $Id$ *)
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmo" i*)
 
 open Options
 open Util
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index d6040646e8..7fd08c7b05 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -6,13 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmo" i*) 
+
+
 (*
   Syntax for the subtac terms and types.
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
 
 (* $Id$ *)
 
-(*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Options
 open Util
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index ebe2b28939..7585ad4d86 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
+
 (* $Id$ *)
 
 open Genarg
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ecb2e132a8..5e68c73089 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo" i*)
+
 (* $Id$ *)
 
 open Pcoq
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index 8942b6541e..91433b8a63 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -6,8 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
 (*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
+
+(* $Id$ *)
+
 
 open Decl_expr
 open Names
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 5755aee645..3c5c88e89a 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo" i*)
+
 (* $Id$ *)
 
 open Pp
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index 1c838f238d..fe7906f63d 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo" i*)
+
 (* $Id$ *)
 
 open Pp
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 73c88540c0..d2d5ad36a1 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo" i*)
+
 (*i $Id$ i*)
 
 open Pcoq
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index e13962ce88..b564828a57 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,8 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo" i*)
+
 (* $Id$ *)
 
+
 open Pcoq
 open Pp
 open Tactic
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7ec88618da..ff23fb225c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo" i*)
+
 (* $Id$ *)
 
 open Pp
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c128ff7af2..c61dfbf63d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -6,8 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
 (*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmo" i*)
+
+(* $Id$ *)
+
 
 open Pp
 open Util
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index dea45ac11c..cd929e5af5 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo" i*)
+
 (* $Id$ *)
 
 open Pp
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 9f7e422d73..043a0c08a9 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -8,6 +8,11 @@
 
 (*i $Id$ i*)
 
+
+(*i camlp4use: "pr_o.cmo" i*) 
+(* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with
+ * ast-based camlp4 *)
+
 open Pp
 open Token
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 68659bb3e1..161a08bfa7 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo" i*)
+
 (*i $Id$ i*)
 
 open Pp
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 21c851dfbe..d8ce0a570e 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
+
 (* $Id: g_constr.ml4,v 1.58 2005/12/30 10:55:32 herbelin Exp $ *)
 
 open Rawterm
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e03d5d7c0a..f5bab5d69d 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_ifdef.cmo" i*)
+(*i camlp4use: "q_MLast.cmo pa_ifdef.cmo" i*)
 
 (* $Id$ *)
 
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index f7ea7ee468..7c684cdc15 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "q_MLast.cmo" i*)
+
 (* $Id$ *)
 
 (* This file defines standard combinators to build ml expressions *)
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 7e32879d2a..476732a3f3 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
+
 (* $Id$ *)
 
 open Genarg
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 5e8337fe97..3c8526c08c 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
+
 (* $Id$ *)
 
 open Genarg