diff options
| author | Emilio Jesus Gallego Arias | 2020-10-16 15:50:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-13 19:12:29 +0100 |
| commit | 94048f8960910cee604946d1b950b21bcc662ff8 (patch) | |
| tree | c45dd4bb0781b35fe5b3cd8c3f628a968dfd577f /kernel/type_errors.mli | |
| parent | 593e99514abc1b43a011f4ae64f40443714b0a68 (diff) | |
[record] Some documentation + minor refactoring
Co-authored-by: <Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions