diff options
| -rw-r--r-- | _tags | 18 | ||||
| -rw-r--r-- | myocamlbuild.ml | 13 |
2 files changed, 30 insertions, 1 deletions
@@ -25,7 +25,6 @@ "toplevel/whelp.ml4": use_grammar "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 @@ -35,6 +34,23 @@ "tactics/hipattern.ml4": use_grammar, use_constr "tactics/rewrite.ml4": use_grammar +"parsing/g_constr.ml4": use_compat5 +"parsing/g_ltac.ml4": use_compat5 +"parsing/g_prim.ml4": use_compat5 +"parsing/g_proofs.ml4": use_compat5 +"parsing/g_tactic.ml4": use_compat5 +"parsing/g_vernac.ml4": use_compat5 +"parsing/g_xml.ml4": use_compat5 +"parsing/pcoq.ml4": use_compat5 +"plugins/decl_mode/g_decl_mode.ml4": use_compat5 +"plugins/funind/g_indfun.ml4": use_compat5 +"plugins/subtac/g_subtac.ml4": use_compat5 + +"parsing/argextend.ml4": use_compat5b +"parsing/q_constr.ml4": use_compat5b +"parsing/tacextend.ml4": use_compat5b +"parsing/vernacextend.ml4": use_compat5b + <plugins/**/*.ml4>: use_grammar ## sub-directory inclusion diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 5832fa813..6cf1d5214 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -287,6 +287,19 @@ let extra_rules () = begin 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_compat5"] (P "tools/compat5.cmo"); + flag_and_dep ["p4mod"; "use_compat5b"] (P "tools/compat5b.cmo"); + + let mlp_cmo s = + let src=s^".mlp" and dst=s^".cmo" in + rule (src^".cmo") ~dep:src ~prod:dst ~insert:`top + (fun env _ -> + Cmd (S [!Options.ocamlc; A"-c"; A"-pp"; + Quote (S [camlp4o;A"-impl"]); camlp4incl; A"-impl"; P src])) + in + mlp_cmo "tools/compat5"; + mlp_cmo "tools/compat5b"; + (** Special case of toplevel/mltop.ml4: - mltop.ml will be the old mltop.optml and be used to obtain mltop.cmx - we add a special mltop.ml4 --> mltop.cmo rule, before all the others |