diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /_tags | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to '_tags')
-rw-r--r-- | _tags | 53 |
1 files changed, 25 insertions, 28 deletions
@@ -1,16 +1,18 @@ ## tags for binaries -<scripts/coqmktop.{native,byte}> : use_str, use_unix, use_gramlib -<scripts/coqc.{native,byte}> : use_unix, use_gramlib +<scripts/coqmktop.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX +<scripts/coqc.{native,byte}> : use_unix, use_dynlink, use_camlpX <tools/coqdep_boot.{native,byte}> : use_unix -<tools/coqdep.{native,byte}> : use_unix, use_gramlib +<tools/coqdep.{native,byte}> : use_unix, use_dynlink, use_camlpX <tools/coq_tex.{native,byte}> : use_str -<tools/coq_makefile.{native,byte}> : use_str +<tools/coq_makefile.{native,byte}> : use_str, use_unix <tools/coqdoc/main.{native,byte}> : use_str -<checker/main.{native,byte}> : use_str, use_unix, use_gramlib +<ide/coqide_main.{native,byte}> : use_str, use_unix, thread, ide +<checker/main.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX <plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix <tools/mkwinapp.{native,byte}> : use_unix +<tools/fake_ide.{native,byte}> : use_unix ## tags for ide @@ -22,30 +24,9 @@ ## tags for camlp4 files -<**/*.ml4>: is_ml4 - -"toplevel/mltop.ml4": is_mltop, use_macro - -"parsing/lexer.ml4": use_macro -"lib/compat.ml4": use_macro -"lib/refutpat.ml4": use_extend, use_MLast -"parsing/g_xml.ml4": use_extend -"parsing/q_constr.ml4": use_extend, use_MLast -"parsing/argextend.ml4": use_extend, use_MLast -"parsing/tacextend.ml4": use_extend, use_MLast -"parsing/g_prim.ml4": use_extend -"parsing/g_ltac.ml4": use_extend -"parsing/pcoq.ml4": use_extend, use_macro -"parsing/q_util.ml4": use_MLast -"parsing/vernacextend.ml4": use_extend, use_MLast -"parsing/g_constr.ml4": use_extend -"parsing/g_tactic.ml4": use_extend -"parsing/g_proofs.ml4": use_extend -"parsing/q_coqast.ml4": use_MLast, use_macro +"toplevel/mltop.ml4": is_mltop "toplevel/whelp.ml4": use_grammar -"parsing/g_vernac.ml4": use_grammar, use_extend -"parsing/g_decl_mode.ml4": use_grammar, use_extend, use_MLast "tactics/extraargs.ml4": use_grammar "tactics/extratactics.ml4": use_grammar "tactics/class_tactics.ml4": use_grammar @@ -55,8 +36,24 @@ "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 -"plugins/subtac/g_subtac.ml4": use_extend ## sub-directory inclusion |