diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-25 17:23:50 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 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