aboutsummaryrefslogtreecommitdiff
path: root/myocamlbuild.ml
diff options
context:
space:
mode:
Diffstat (limited to 'myocamlbuild.ml')
-rw-r--r--myocamlbuild.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 5f838571d8..0ed2053509 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -299,9 +299,6 @@ let extra_rules () = begin
mlp_cmo "tools/compat5b";
end;
- ocaml_lib ~extern:true ~dir:Coq_config.camlp4lib ~tag_name:"use_camlpX"
- ~byte:true ~native:true (if use_camlp5 then "gramlib" else "camlp4lib");
-
(** 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