diff options
| author |  mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-22 14:18:38 +0000 |
|---|---|---|
| committer | mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-22 14:18:38 +0000 |
| commit | 62ce65dadb0afb8815b26069246832662846c7ec (patch) | |
| tree | 12d463433d64263510f3875b116f7b8cf16d43bc /kernel/nativelibrary.ml | |
| parent | e88df65bbc64b18da34a4233f680829025ca76d9 (diff) | |
Revert "remove -rectypes except for term.ml"
Preparing landing of the native compiler, which requires -rectypes flag.
This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/nativelibrary.ml')
0 files changed, 0 insertions, 0 deletions