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