diff options
| author | aspiwack | 2012-05-11 15:11:07 +0000 |
|---|---|---|
| committer | aspiwack | 2012-05-11 15:11:07 +0000 |
| commit | 5ea279dbd47d9ef1b87351e4df469aba3310f3f0 (patch) | |
| tree | c14542a358247563989a3d887a94f5a6d81782cc /.typerex | |
| parent | 2abc6e4c9b35570a44af9a246c88bb177d81373d (diff) | |
Tentative and very experminental support for typerex. Enabled with
./configure -typerex .
It causes (non-fatal) errors when compiling files without a .mli (the problem
seems to have something to do with the flag -intf-suffix .cmi).
In practice, most typerex functionalities don't work well because typerex
fails its lookup into files compiled with -rectypes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15302 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to '.typerex')
| -rw-r--r-- | .typerex | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/.typerex b/.typerex new file mode 100644 index 0000000000..9ccd4e7efc --- /dev/null +++ b/.typerex @@ -0,0 +1,18 @@ +parsing +ide +ide/utils +interp +kernel +kernel/byterun +lib +library +plugins +pretyping +proofs +scripts +states +tactics +theories +tools +tools/coqdoc +toplevel
\ No newline at end of file |