summaryrefslogtreecommitdiff
path: root/_tags
diff options
context:
space:
mode:
Diffstat (limited to '_tags')
-rw-r--r--_tags48
1 files changed, 21 insertions, 27 deletions
diff --git a/_tags b/_tags
index a8b4ff1a..8cb8b1f9 100644
--- a/_tags
+++ b/_tags
@@ -1,40 +1,30 @@
## 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
+<tools/coqmktop.{native,byte}> : use_str, use_unix
+<tools/coqc.{native,byte}> : use_str, use_unix
<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
<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, use_camlpX
-<checker/main.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
+<ide/coqide_main.{native,byte}> : use_str, use_unix, ide
+<checker/main.{native,byte}> : use_str, use_unix, thread
<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix
<tools/mkwinapp.{native,byte}> : use_unix
-<tools/fake_ide.{native,byte}> : use_unix, use_camlpX
+<tools/fake_ide.{native,byte}> : use_unix, use_str
## tags for ide
-<ide/**/*.{ml,mli}>: thread, ide
+<ide/**/*.{ml,mli}>: ide
## tags for grammar.cm*
-<parsing/grammar.{cma,cmxa}> : use_unix
+<grammar/grammar.{cma,cmxa}> : use_unix
## tags for camlp4 files
-"toplevel/mltop.ml4": is_mltop
-
"toplevel/whelp.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
@@ -44,16 +34,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
-"plugins/subtac/g_subtac.ml4": use_compat5
+"parsing/g_obligations.ml4": use_grammar
-"parsing/argextend.ml4": use_compat5b
-"parsing/q_constr.ml4": use_compat5b
-"parsing/tacextend.ml4": use_compat5b
-"parsing/vernacextend.ml4": use_compat5b
+"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
@@ -64,6 +57,8 @@
"ide": include
"ide/utils": include
"interp": include
+"intf": include
+"grammar": include
"kernel": include
"kernel/byterun": include
"lib": include
@@ -71,9 +66,8 @@
"parsing": include
"plugins": include
"pretyping": include
+"printing": include
"proofs": include
-"scripts": include
-"states": include
"tactics": include
"theories": include
"tools": include