aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-06 10:08:56 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-06 10:08:56 +0000
commit37febc09f2f5e8b64fd321bf54e91e6381b4fa33 (patch)
treeb5fdc7e7af10d3a9bd4c7a9c12b13dc6b8701c94
parent48b3abb2373a1bd4655f2de44f42245be4d773ac (diff)
ocamlbuild simplifications
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15878 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--_tags25
-rw-r--r--myocamlbuild.ml3
2 files changed, 10 insertions, 18 deletions
diff --git a/_tags b/_tags
index 767b6ebe2..3097447c3 100644
--- a/_tags
+++ b/_tags
@@ -1,15 +1,15 @@
## tags for binaries
-<scripts/coqmktop.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
-<scripts/coqc.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
+<scripts/coqmktop.{native,byte}> : use_str, use_unix
+<scripts/coqc.{native,byte}> : use_str, use_unix
<tools/coqdep_boot.{native,byte}> : use_unix
-<tools/coqdep.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
+<tools/coqdep.{native,byte}> : use_str, use_unix
<tools/coq_tex.{native,byte}> : use_str
<tools/coq_makefile.{native,byte}> : use_str, use_unix
<tools/coqdoc/main.{native,byte}> : use_str
<ide/coqide_main.{native,byte}> : use_str, use_unix, thread, ide
-<checker/main.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
+<checker/main.{native,byte}> : use_str, use_unix
<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix
<tools/mkwinapp.{native,byte}> : use_unix
<tools/fake_ide.{native,byte}> : use_unix
@@ -31,15 +31,6 @@
"toplevel/mltop.ml4": is_mltop
"toplevel/whelp.ml4": use_grammar
-"parsing/g_obligations.ml4": use_grammar
-"tactics/extraargs.ml4": use_grammar
-"tactics/extratactics.ml4": use_grammar
-"tactics/class_tactics.ml4": use_grammar
-"tactics/eauto.ml4": use_grammar
-"tactics/tauto.ml4": use_grammar
-"tactics/eqdecide.ml4": use_grammar
-"tactics/hipattern.ml4": use_grammar, use_constr
-"tactics/rewrite.ml4": use_grammar
"parsing/g_constr.ml4": use_compat5
"parsing/g_ltac.ml4": use_compat5
@@ -49,15 +40,19 @@
"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
+"parsing/g_obligations.ml4": use_grammar
"grammar/argextend.ml4": use_compat5b
"grammar/q_constr.ml4": use_compat5b
"grammar/tacextend.ml4": use_compat5b
"grammar/vernacextend.ml4": use_compat5b
+<tactics/*.ml4>: use_grammar
+"tactics/hipattern.ml4": use_constr
+
<plugins/**/*.ml4>: use_grammar
+"plugins/decl_mode/g_decl_mode.ml4": use_compat5
+"plugins/funind/g_indfun.ml4": use_compat5
## sub-directory inclusion
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 5f838571d..0ed205350 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