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

3 files changed, 102 insertions, 0 deletions

diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
new file mode 100644
index 0000000000..128ca94456
--- /dev/null
+++ b/parsing/grammar.mllib
@@ -0,0 +1,78 @@
+Coq_config
+
+Pp_control 
+Pp
+Compat
+Flags
+Util
+Bigint
+Dyn
+Hashcons
+Predicate
+Rtree
+Option
+
+Names
+Univ
+Esubst
+Term
+Mod_subst
+Sign
+Cbytecodes
+Copcodes
+Cemitcodes
+Declarations
+Retroknowledge
+Pre_env
+Cbytegen
+Environ
+Conv_oracle
+Closure
+Reduction
+Type_errors
+Entries
+Modops
+Inductive
+Typeops
+Indtypes
+Cooking
+Term_typing
+Subtyping
+Mod_typing
+Safe_typing
+
+Nameops
+Libnames
+Summary
+Nametab
+Libobject
+Lib
+Goptions
+Decl_kinds 
+Global
+Termops
+Evd
+Reductionops
+Inductiveops
+Rawterm
+Detyping
+Pattern
+Topconstr
+Genarg
+Ppextend
+Tacexpr
+Lexer
+Extend
+Vernacexpr
+Pcoq
+Q_util
+Q_coqast 
+
+Argextend
+Tacextend
+Vernacextend
+
+G_prim
+G_tactic
+G_ltac
+G_constr
\ No newline at end of file
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
new file mode 100644
index 0000000000..03fb9c6295
--- /dev/null
+++ b/parsing/highparsing.mllib
@@ -0,0 +1,13 @@
+G_constr
+G_vernac
+G_prim
+G_proofs
+G_tactic
+G_ltac
+G_natsyntax
+G_zsyntax
+G_rsyntax
+G_ascii_syntax
+G_string_syntax
+G_decl_mode
+G_intsyntax
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
new file mode 100644
index 0000000000..c705e45cd9
--- /dev/null
+++ b/parsing/parsing.mllib
@@ -0,0 +1,11 @@
+Extend
+Pcoq
+Egrammar
+G_xml
+Ppconstr
+Printer
+Pptactic
+Ppdecl_proof
+Tactic_printer
+Printmod
+Prettyp