diff options
| author | Tej Chajed | 2018-10-23 10:28:48 -0400 |
|---|---|---|
| committer | Tej Chajed | 2018-10-26 09:55:17 -0400 |
| commit | fcde9195f8e63ff427c03af6373f344c991fb099 (patch) | |
| tree | bbc1b8fdec678ef21bc87b3af1107701e155656d /kernel/type_errors.mli | |
| parent | 3059b9fa7c2f0e8d0d7eadabfdb5d833f294a904 (diff) | |
Add record names to multiple records error message
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions