diff options
| author | Hugo Herbelin | 2020-04-09 12:31:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-21 19:10:49 +0200 |
| commit | 6908a9da72bc534d53493816d9b552c85d447f49 (patch) | |
| tree | 9bcff0224cbdb3ba85434466e28aee375eda7fd4 /kernel/nativelambda.mli | |
| parent | 047bfb20201776255df926fdab4d96fc0c0a82d1 (diff) | |
Constrintern: another reworking of the interning of records.
This allows to have the "No local fields allowed in a record
construction" error applicable to all fields and not only the first
one. Formerly, this was wrongly raising an error "This record contains
fields of both T and T".
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions