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

1 files changed, 59 insertions, 0 deletions

diff --git a/_tags b/_tags
new file mode 100644
index 0000000000..7e8db8dd61
--- /dev/null
+++ b/_tags
@@ -0,0 +1,59 @@
+
+## tags for binaries
+
+<scripts/coqmktop.{native,byte}> : 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
+