diff options
| author | Matthieu Sozeau | 2016-07-04 15:26:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-04 15:27:59 +0200 |
| commit | 9468bcd39808f4587d3732f46773b1e339b2267c (patch) | |
| tree | 5ddb5b1b81b2d240520918e8c845a602f7b1f2d1 | |
| parent | 2b6dd2ff132a74ba247609191c344dda991e3b84 (diff) | |
Update CHANGES, the bugfixes for 4527 and 4726 are
not in pl2.
| -rw-r--r-- | CHANGES | 16 |
1 files changed, 9 insertions, 7 deletions
@@ -1,5 +1,14 @@ Changes beyond V8.5 =================== +Bugfixes + +- #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). Specification language @@ -81,13 +90,6 @@ 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 ============================ |