diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-06-09 15:40:28 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-29 11:52:52 +0200 |
| commit | 23ab6c84b3d04cc2218bf1ad935fa87396999ccd (patch) | |
| tree | 65962a930516d74cd3b3ef419473877107185d5a | |
| parent | 4c90b4243c49b46152eede195a086bc8dc8a86ec (diff) | |
CHANGES: document fix for #4726 too.
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -85,6 +85,8 @@ Bugfixes typechecked using only those universes (after minimization of the other, flexible universes), or raise an error (fixed scripts can be made forward compatible). +- #4726: treat user-provided sorts of universe polymorphic records as rigid + (i.e. non-minimizable). Changes from V8.5 to V8.5pl1 ============================ |