diff options
| -rw-r--r-- | CHANGES | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -80,6 +80,11 @@ 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). Changes from V8.5 to V8.5pl1 ============================ |