From dffb6159812757ba59e02419b451e6135d1e3502 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 20 Mar 2009 20:50:44 +0000 Subject: Many changes in the Makefile infrastructure + a beginning of ocamlbuild * generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7 --- _tags | 59 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 _tags (limited to '_tags') diff --git a/_tags b/_tags new file mode 100644 index 0000000000..7e8db8dd61 --- /dev/null +++ b/_tags @@ -0,0 +1,59 @@ + +## tags for binaries + + : use_str, use_unix, use_gramlib + +## tags for camlp4 files + +<**/*.ml4>: is_ml4 + +"toplevel/mltop.ml4": is_mltop, use_macro + +"lib/compat.ml4": use_macro +"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/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 +"tactics/eauto.ml4": use_grammar +"tactics/tauto.ml4": use_grammar +"tactics/eqdecide.ml4": use_grammar +"tactics/hipattern.ml4": use_grammar, use_constr + + +## sub-directory inclusion + +"config": include +"parsing": include +"ide": include +"interp": include +"kernel": include +"kernel/byterun": include +"lib": include +"library": include +"parsing": include +"plugins": include +"pretyping": include +"proofs": include +"scripts": include +"states": include +"tactics": include +"theories": include +"tools": include +"toplevel": include + -- cgit v1.2.3