diff options
| author | Gaëtan Gilbert | 2020-07-01 09:51:44 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 09:51:44 +0200 |
| commit | 36faebc29986f7e895a7de16c6f2ea4c5b6fd074 (patch) | |
| tree | 19339dba343a00677517491facbd1968524b6d7b /kernel/type_errors.mli | |
| parent | 69e798fb97487b3a83de3486084a112413850fdf (diff) | |
Use weak ref to memoize Evarutil.is_ground_env
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions