aboutsummaryrefslogtreecommitdiff
path: root/_tags
diff options
context:
space:
mode:
authorpboutill2012-04-12 20:49:01 +0000
committerpboutill2012-04-12 20:49:01 +0000
commit59c9403ceb09a35ed219b522e9f5abdb50615d76 (patch)
treef7d3e521f6a948defdce70e00c718c6bdc7b696e /_tags
parent1b9428c4e4ce6f2dbe98d0f753b062ae8634a954 (diff)
lib directory is cut in 2 cma.
- Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to '_tags')
-rw-r--r--_tags6
1 files changed, 3 insertions, 3 deletions
diff --git a/_tags b/_tags
index 6c69011b82..b714aa93d3 100644
--- a/_tags
+++ b/_tags
@@ -2,9 +2,9 @@
## tags for binaries
<scripts/coqmktop.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
-<scripts/coqc.{native,byte}> : use_unix, use_dynlink, use_camlpX
+<scripts/coqc.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
<tools/coqdep_boot.{native,byte}> : use_unix
-<tools/coqdep.{native,byte}> : use_unix, use_dynlink, use_camlpX
+<tools/coqdep.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
<tools/coq_tex.{native,byte}> : use_str
<tools/coq_makefile.{native,byte}> : use_str, use_unix
<tools/coqdoc/main.{native,byte}> : use_str
@@ -27,6 +27,7 @@
"toplevel/mltop.ml4": is_mltop
"toplevel/whelp.ml4": use_grammar
+"toplevel/g_obligations.ml4": use_grammar
"tactics/extraargs.ml4": use_grammar
"tactics/extratactics.ml4": use_grammar
"tactics/class_tactics.ml4": use_grammar
@@ -46,7 +47,6 @@
"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