diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 20:56:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-01 19:34:58 +0200 |
| commit | 0bc7e7405553dc63d9693e85c3ce1485b5e8fe23 (patch) | |
| tree | 29a75b9b4edf5e20e939ab9c5779c5516294517d /kernel/nativecode.mli | |
| parent | fa1782e05eeb6f18871d26cc43670d35ed73bf23 (diff) | |
[declare] Separate kinds from entries in constant declaration
They are clearly not at the same importance level, thus we use a named
parameter and isolate the kinds as to allow further improvements and
refactoring.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions