diff options
| author | Emilio Jesus Gallego Arias | 2020-03-15 00:13:55 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-13 19:12:29 +0100 |
| commit | e47d39403f9830d7a84c32bdc3e9cf360427b7e8 (patch) | |
| tree | 1deac8ab3ce7b26c9a61f71eee2164156bb2b383 /kernel/nativecode.ml | |
| parent | b341b58104ff14f10a5e170d4bfbc7a02f12755f (diff) | |
[record] Cleanup of data structure and functions [2/2]
In preparation for reworking the record declaration path to use the
common infrastructure, we perform some refactoring.
The current choices are far from definitive, as we will consolidate
the data types more as we move along with the work here.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions