diff options
| author | Pierre-Marie Pédrot | 2017-12-25 17:23:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-12-29 14:46:32 +0100 |
| commit | 045193aedfd6a262981f06c500af1cc13df2900f (patch) | |
| tree | 6ac79fcfd27c6012f6ea7b2d8e08432749f56444 /kernel/environ.ml | |
| parent | a4c8ee5ccffd2b56acf5e6719213e9799e077601 (diff) | |
Share the rel environment between Environ.env and reduction cache.
Diffstat (limited to 'kernel/environ.ml')
0 files changed, 0 insertions, 0 deletions