diff options
| author | Maxime Dénès | 2018-03-09 13:11:04 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-09 13:11:04 +0100 |
| commit | ff947d85f8b8921e401b693e47c52504c71f9c4c (patch) | |
| tree | 24c7acce3d8dcc2d5babb7182f81924bb4ae82cd /dev | |
| parent | 0c345d64d67c01c7b7a75bf23391b421f95c4fb7 (diff) | |
| parent | 925487d5450f2575b1d46a9a694c5e447c776047 (diff) | |
Merge PR #6945: Fix error with univ binders on monomorphic records.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions