static (and shared) camlp4use instead of per-file declaration

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

24 files changed, 12 insertions, 71 deletions

diff --git a/Makefile.build b/Makefile.build
index 9b6452658..42b2ee456 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -97,7 +97,7 @@ $(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^
 endef
 
 CAMLP4DEPS=`sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<`
-CAMLP4USE=`sed -n -e 's/pa_macro.cmo/pa_macro.cmo -D$(CAMLVERSION)/' -e 's@^(\*.*camlp4use: "\(.*\)".*@\1@p' $<`
+CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
 
 PR_O := $(if $(READABLE_ML4),pr_o.cmo)
 
@@ -788,7 +788,7 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(HIDE)\
 	DEPS=$(CAMLP4DEPS); \
 	if ls $${DEPS} > /dev/null 2>&1; then \
-	$(CAMLP4O) $(PR_O) $(CAMLP4USE) $${DEPS} $(CAMLP4COMPAT) -impl $< $(TOTARGET); \
+	$(CAMLP4O) $(PR_O) $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< $(TOTARGET); \
 	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/_tags b/_tags
index dd82e488d..32f57c706 100644
--- a/_tags
+++ b/_tags
@@ -21,28 +21,11 @@
 
 ## tags for camlp4 files 
 
-"toplevel/mltop.ml4": is_mltop, use_macro
-
-"parsing/lexer.ml4": use_macro
-"lib/compat.ml4": use_macro
-"lib/refutpat.ml4": use_extend, use_MLast
-"parsing/g_xml.ml4": use_extend
-"parsing/q_constr.ml4": use_extend, use_MLast
-"parsing/argextend.ml4": use_extend, use_MLast
-"parsing/tacextend.ml4": use_extend, use_MLast
-"parsing/g_prim.ml4": use_extend
-"parsing/g_ltac.ml4": use_extend
-"parsing/pcoq.ml4": use_extend, use_macro
-"parsing/q_util.ml4": use_MLast
-"parsing/vernacextend.ml4": use_extend, use_MLast
-"parsing/g_constr.ml4": use_extend
-"parsing/g_tactic.ml4": use_extend
-"parsing/g_proofs.ml4": use_extend
-"parsing/q_coqast.ml4": use_MLast, use_macro
+"toplevel/mltop.ml4": is_mltop
 
 "toplevel/whelp.ml4": use_grammar
-"parsing/g_vernac.ml4": use_grammar, use_extend
-"parsing/g_decl_mode.ml4": use_grammar, use_extend, use_MLast
+"parsing/g_vernac.ml4": use_grammar
+"parsing/g_decl_mode.ml4": use_grammar
 "tactics/extraargs.ml4": use_grammar
 "tactics/extratactics.ml4": use_grammar
 "tactics/class_tactics.ml4": use_grammar
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 4ec4d915c..5ed8d7a54 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_macro.cmo" i*)
-
-(* Compatibility file depending on ocaml version *)
+(** Compatibility file depending on ocaml/camlp4 version *)
 
 IFDEF CAMLP5 THEN
 
diff --git a/lib/refutpat.ml4 b/lib/refutpat.ml4
index 7c6801a8b..ef2801941 100644
--- a/lib/refutpat.ml4
+++ b/lib/refutpat.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-
 open Pcaml
 
 (** * Non-irrefutable patterns
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index dc9e4dbfe..6f148ba73 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -270,9 +270,9 @@ let extra_rules () = begin
 	      T(tags_of_pathname ml4 ++ "p4option"); camlp4compat;
 	      A"-o"; Px ml; A"-impl"; P ml4]));
 
-  flag ["p4mod"; "use_macro"] (A"pa_macro.cmo");
-  flag ["p4mod"; "use_extend"] (A"pa_extend.cmo");
-  flag ["p4mod"; "use_MLast"] (A"q_MLast.cmo");
+  flag ["p4mod"] (A"pa_macro.cmo");
+  flag ["p4mod"] (A"pa_extend.cmo");
+  flag ["p4mod"] (A"q_MLast.cmo");
 
   flag_and_dep ["p4mod"; "use_grammar"] (P "parsing/grammar.cma");
   flag_and_dep ["p4mod"; "use_constr"] (P "parsing/q_constr.cmo");
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 3b2160af1..72b9d0a50 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-
 open Genarg
 open Q_util
 open Q_coqast
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 432903377..12ed0c4b6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo" i*)
-
 open Pp
 open Pcoq
 open Constr
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index ca9e90cd5..bfdd0773a 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo" i*)
-
 open Pp
 open Util
 open Topconstr
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 02b3df3fb..5e6e0e1ed 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo" i*)
-
 open Pcoq
 open Names
 open Libnames
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 758d4599a..dfb59a19d 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,9 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo" i*)
-
-
 open Pcoq
 open Pp
 open Tactic
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 0ef18de2f..c1400f0c4 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo" i*)
-
 open Pp
 open Pcoq
 open Util
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a5b522fea..8951cfa2f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo" i*)
 
 
 open Pp
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 8bda1e58f..901f7ff10 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo" i*)
-
 open Pp
 open Util
 open Names
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 9ca653343..1db651033 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_macro.cmo" i*)
-
 open Pp
 open Util
 open Token
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 087bfc5b7..d12388382 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
-
 open Pp
 open Util
 open Names
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 28911794f..4c86e4415 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-
 open Rawterm
 open Term
 open Names
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 914b6b8f6..6d3e8e03a 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*)
-
 open Util
 open Names
 open Libnames
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index e5851f81d..94319cc73 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "q_MLast.cmo" i*)
-
 (* This file defines standard combinators to build ml expressions *)
 
 open Util
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index f77b24eff..fb1425e0e 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-
 open Util
 open Genarg
 open Q_util
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index ff354d5e0..d8b6fba31 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-
 open Util
 open Genarg
 open Q_util
diff --git a/plugins/_tags b/plugins/_tags
index 8611ebc0c..2d1d5a760 100644
--- a/plugins/_tags
+++ b/plugins/_tags
@@ -4,9 +4,9 @@
 "setoid_ring/newring.ml4": use_grammar
 "dp/g_dp.ml4": use_grammar
 "quote/g_quote.ml4": use_grammar
-"subtac/equations.ml4": use_grammar, use_extend
+"subtac/equations.ml4": use_grammar
 "subtac/g_eterm.ml4": use_grammar
-"subtac/g_subtac.ml4": use_grammar, use_extend
+"subtac/g_subtac.ml4": use_grammar
 "rtauto/g_rtauto.ml4": use_grammar
 "xml/xmlentries.ml4": use_grammar
 "xml/dumptree.ml4": use_grammar
@@ -20,7 +20,7 @@
 "fourier/g_fourier.ml4": use_grammar
 "groebner/ideal.ml4": use_refutpat
 "groebner/groebner.ml4": use_grammar
-"decl_mode/g_decl_mode.ml4": use_grammar, use_extend, use_MLast
+"decl_mode/g_decl_mode.ml4": use_grammar
 
 "cc": include
 "extraction": include
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index d87708510..28aa93975 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
 (* arnaud: veiller à l'aspect tutorial des commentaires *)
 
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 28ded30da..9e415b635 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo" i*)
-
 
 (*
   Syntax for the subtac terms and types.
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 509ecd89d..8b0775d9f 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -6,11 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_macro.cmo" i*)
-(* WARNING
- * camlp4deps will not work for this file unless Makefile system enhanced.
- *)
-
 open Util
 open Pp
 open Flags