diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-20 20:50:44 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-20 20:50:44 +0000 |
commit | dffb6159812757ba59e02419b451e6135d1e3502 (patch) | |
tree | ab7b08e217b1e3ba24bf584220478c7c812a0d1e /pretyping/pretyping.mllib | |
parent | d542a1850f52bb44a1c2d026fd5277b26aa9354c (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 'pretyping/pretyping.mllib')
-rw-r--r-- | pretyping/pretyping.mllib | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib new file mode 100644 index 000000000..ab0fac4a6 --- /dev/null +++ b/pretyping/pretyping.mllib @@ -0,0 +1,28 @@ +Termops +Evd +Reductionops +Vnorm +Inductiveops +Retyping +Cbv +Pretype_errors +Typing +Evarutil +Term_dnet +Recordops +Tacred +Evarconv +Typeclasses_errors +Typeclasses +Classops +Coercion +Unification +Clenv +Rawterm +Pattern +Detyping +Indrec +Cases +Pretyping +Matching + |