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

17 files changed, 41 insertions, 3 deletions

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