diff options
| author | Pierre-Marie Pédrot | 2016-08-04 19:18:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-05 11:54:26 +0200 |
| commit | 26e5194bc252e4ac71c74f8ac73a0e2cbe82edf6 (patch) | |
| tree | b0f46e42fd417037fd5f9fda61726d48edb66474 /dev/include | |
| 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 'dev/include')
0 files changed, 0 insertions, 0 deletions