aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/kernel.mllib
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-20 20:50:44 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-20 20:50:44 +0000
commitdffb6159812757ba59e02419b451e6135d1e3502 (patch)
treeab7b08e217b1e3ba24bf584220478c7c812a0d1e /kernel/kernel.mllib
parentd542a1850f52bb44a1c2d026fd5277b26aa9354c (diff)
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
Diffstat (limited to 'kernel/kernel.mllib')
-rw-r--r--kernel/kernel.mllib32
1 files changed, 32 insertions, 0 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
new file mode 100644
index 000000000..a628e5cfe
--- /dev/null
+++ b/kernel/kernel.mllib
@@ -0,0 +1,32 @@
+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
+
+Vm
+Csymtable
+Vconv \ No newline at end of file