diff options
| author | Hugo Herbelin | 2018-02-13 12:19:47 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-13 12:22:34 +0100 |
| commit | 50c948480647af3c5aaea5f80fa9f3341471f2b0 (patch) | |
| tree | 26f18a3c560197dede4932f02b4ac4d8a4acc701 /dev/header.ml | |
| parent | d2fb531761e1f4fa02d0c7e7b5b51febe48e357e (diff) | |
Fixing an anomaly in the presence of "let-in" in the type of a record.
Was raised by Jason on Gitter.
Diffstat (limited to 'dev/header.ml')
0 files changed, 0 insertions, 0 deletions