aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-11 15:11:07 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-11 15:11:07 +0000
commit5ea279dbd47d9ef1b87351e4df469aba3310f3f0 (patch)
treec14542a358247563989a3d887a94f5a6d81782cc /config
parent2abc6e4c9b35570a44af9a246c88bb177d81373d (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 'config')
-rw-r--r--config/Makefile.template1
1 files changed, 1 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index 91b12cb4f..f406ab6fb 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -83,6 +83,7 @@ CAMLMKTOP="CAMLMKTOPEXEC"
# Caml flags
CAMLFLAGS=-rectypes CAMLANNOTATEFLAG
+TYPEREX=TYPEREXCMD
# Compilation debug flags
CAMLDEBUG=COQDEBUGFLAG