Myocamlbuild: slight simplification of code for .ml4

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

2 files changed, 6 insertions, 12 deletions

diff --git a/_tags b/_tags
index 6f83b4ef3a..dd82e488d9 100644
--- a/_tags
+++ b/_tags
@@ -21,8 +21,6 @@
 
 ## tags for camlp4 files 
 
-<**/*.ml4>: is_ml4
-
 "toplevel/mltop.ml4": is_mltop, use_macro
 
 "parsing/lexer.ml4": use_macro
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index f062b50bbb..dc9e4dbfe3 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -123,10 +123,6 @@ let copcodes = "kernel/copcodes.ml"
 
 let libcoqrun = "kernel/byterun/libcoqrun.a"
 
-let grammar = "parsing/grammar.cma"
-let qconstr = "parsing/q_constr.cmo"
-let refutpat = "lib/refutpat.cmo"
-
 let initialcoq = "states/initial.coq"
 let init_vo = ["theories/Init/Prelude.vo";"theories/Init/Logic_Type.vo"]
 let makeinitial = "states/MakeInitial.v"
@@ -274,13 +270,13 @@ let extra_rules () = begin
 	      T(tags_of_pathname ml4 ++ "p4option"); camlp4compat;
 	      A"-o"; Px ml; A"-impl"; P ml4]));
 
-  flag ["is_ml4"; "p4mod"; "use_macro"] (A"pa_macro.cmo");
-  flag ["is_ml4"; "p4mod"; "use_extend"] (A"pa_extend.cmo");
-  flag ["is_ml4"; "p4mod"; "use_MLast"] (A"q_MLast.cmo");
+  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_and_dep ["is_ml4"; "p4mod"; "use_grammar"] (P grammar);
-  flag_and_dep ["is_ml4"; "p4mod"; "use_constr"] (P qconstr);
-  flag_and_dep ["is_ml4"; "p4mod"; "use_refutpat"] (P refutpat);
+  flag_and_dep ["p4mod"; "use_grammar"] (P "parsing/grammar.cma");
+  flag_and_dep ["p4mod"; "use_constr"] (P "parsing/q_constr.cmo");
+  flag_and_dep ["p4mod"; "use_refutpat"] (P "lib/refutpat.cmo");
 
 (** Special case of toplevel/mltop.ml4:
     - mltop.ml will be the old mltop.optml and be used to obtain mltop.cmx