diff options
| author | Hugo Herbelin | 2019-12-22 20:28:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-20 09:54:45 +0100 |
| commit | 4b429f64ee9a36a7151575b914b3af56a300b28b (patch) | |
| tree | 78da4a1219afcfeafe4bb05be1fda1b7feaf12af /kernel/nativelambda.mli | |
| parent | 9d427ac1c3fcb3c50623d7a95d97bb578fd381fa (diff) | |
Fixing #11114 (anomaly with Extraction Implicit on records).
This was due to an inconsistency in handling implicit arguments in
the fields and in the constructor of a record.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions