diff options
| author | Gaëtan Gilbert | 2020-02-12 14:01:09 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-13 15:12:01 +0100 |
| commit | bbf05cd2baa767c46ce95c1c185b87521afc0ec7 (patch) | |
| tree | f3a8e08ce9e285141abaf59cf59a869a78f32998 /kernel/subtyping.ml | |
| parent | 3af570b60e6912d2eb906ce86a3df3b8ecca675c (diff) | |
Delete unused comment
Diffstat (limited to 'kernel/subtyping.ml')
0 files changed, 0 insertions, 0 deletions