diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-28 22:43:39 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-28 22:43:39 +0200 |
| commit | 8eea39501acffa5f7a4ea046ff3862e391d0655c (patch) | |
| tree | 38ece0503c1609d4c57d32f4e43ec5fa89e746f5 /kernel/typeops.ml | |
| parent | b9740771e8113cb9e607793887be7a12587d0326 (diff) | |
Remove trivial TODO comment (constants can't be template poly now).
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions