From 68352782e99387e7c0b0a87d764ce78b2de7890a Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 18 Mar 2010 19:44:12 +0000 Subject: 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 --- _tags | 2 -- myocamlbuild.ml | 16 ++++++---------- 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 -- cgit v1.2.3