diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-18 14:05:09 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-28 13:24:43 +0200 |
commit | a8c4dee491fdd2426c623ad458ed15310295c93b (patch) | |
tree | 932881da5d8c82de46cebda1e76f239910826ddd /kernel/cooking.ml | |
parent | 3984f3c1db51f7b788ad49eafb7647774e8d1f53 (diff) |
[env.env_rel_context.env_rel_ctx] -> [rel_context env]
It's a bit shorter and more direct.
Diffstat (limited to 'kernel/cooking.ml')
0 files changed, 0 insertions, 0 deletions