diff options
| author | Maxime Dénès | 2017-03-21 14:29:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-21 17:15:27 +0100 |
| commit | 09c856a3bcb7369244202ed94db247f7abe84dad (patch) | |
| tree | c42d9900700d068d25d5707f5f395bd7805ca0ee /kernel/nativecode.mli | |
| parent | cd87eac3757d8925ff4ba7dee85efadb195153a3 (diff) | |
Do not typecheck twice the type of opaque constants.
I believe an unwanted shadowing was introduced by a4043608f704f0.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions