diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-08 14:04:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-08 16:24:49 +0100 |
| commit | 925487d5450f2575b1d46a9a694c5e447c776047 (patch) | |
| tree | d3b77829a0dc31d89b208a2430c0b31362b00412 /toplevel | |
| parent | 563199757c5756fb5858da1b684162566a73fa3e (diff) | |
Fix error with univ binders on monomorphic records.
Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were
declared twice for all records.
Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an
observable error for monomorphic records.
Diffstat (limited to 'toplevel')
0 files changed, 0 insertions, 0 deletions