diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 7 |
1 files changed, 7 insertions, 0 deletions
@@ -80,6 +80,13 @@ Bugfixes - #4777: printing inefficiency with implicit arguments - #4752: CoqIDE crash on files not ended by ".v". - #4398: type_scope used consistently in "match goal". +- #4527: when typechecking the statement of a lemma using universe polymorphic + definitions with explicit universe binders, check that the type can indeed be + 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 ============================ |