diff options
| author | Gaëtan Gilbert | 2020-10-22 11:24:50 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-22 11:24:50 +0200 |
| commit | f0ce03e2c4d519ee8321bed8d61c3c959e505d49 (patch) | |
| tree | d6c13ad0b2aa4a2b485b6b434efc412a1ba02c4f /kernel/type_errors.ml | |
| parent | 235c550896604b6b030a31fbd98eddb7237ece44 (diff) | |
Fix bench variables
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions