diff options
| author | Maxime Dénès | 2016-06-16 14:09:25 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-16 14:09:25 +0200 |
| commit | f9a619753644ba8e0f0ca1218396c8efee52b544 (patch) | |
| tree | de3c578430f5760ba862cc2d57a16fbcabc3c9f6 /kernel/typeops.ml | |
| parent | da92254c786a62d05a66f12b4e8e01171e171e3c (diff) | |
Remove inappropriate comment.
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions