diff options
| author | Emilio Jesus Gallego Arias | 2020-06-30 16:27:29 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-13 19:12:29 +0100 |
| commit | d4ce120346aaecef518c0781cf194308bad55f12 (patch) | |
| tree | c6038af6ca0d940b9832ece49791a908c8ad1a2f /kernel/type_errors.mli | |
| parent | e47d39403f9830d7a84c32bdc3e9cf360427b7e8 (diff) | |
[record] Refactor nested functions.
In preparation for better handling of the regular record / class
codepath. This will also allow to pack record data better.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions