diff options
author | 2018-02-13 12:19:47 +0100 | |
---|---|---|
committer | 2018-02-13 12:22:34 +0100 | |
commit | 50c948480647af3c5aaea5f80fa9f3341471f2b0 (patch) | |
tree | 26f18a3c560197dede4932f02b4ac4d8a4acc701 /configure.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 'configure.ml')
0 files changed, 0 insertions, 0 deletions