diff options
| author | Gaëtan Gilbert | 2021-04-14 14:09:07 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-04-14 14:09:07 +0200 |
| commit | ad380aca8cad3329c9a3db4b65b933b1179ed6a2 (patch) | |
| tree | a52999ba8e54b12c4458f80716fb94afb05610f2 /kernel/type_errors.ml | |
| parent | ea62d1e19f2ba565ea3a18ba3709a06af5c845ac (diff) | |
Cleanup useless environment manipulation in Class declaration
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions