diff options
author | 2016-08-04 19:18:48 +0200 | |
---|---|---|
committer | 2016-08-05 11:54:26 +0200 | |
commit | 26e5194bc252e4ac71c74f8ac73a0e2cbe82edf6 (patch) | |
tree | b0f46e42fd417037fd5f9fda61726d48edb66474 /Makefile.dev | |
parent | 118572b57a6f15ad4342e8a75ca0836e7896d465 (diff) |
Using the extended contexts in pretyping.
In addition to sharing, we also delay the computation of the environment in
a by-need fashion.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions