aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2016-07-26 14:08:07 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2016-07-26 14:08:07 +0200
commita40420601410c5d6f86ff40c5f0b0e723d171833 (patch)
treea85eb630187aef57daee8e9432da3bb72b9a31fc /CHANGES
parentad39b5c127e1ff3d16adc1d0264617d461616111 (diff)
Update CHANGES about critical bugfix and others
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES7
1 files changed, 7 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 5b7db5c38..97a803b82 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,13 @@
Changes from V8.5pl2 to V8.5pl3
===============================
+
+Critical bugfix
+- #4876: Guard checker incompleteness when using primitive projections
+
+Other bugfixes
+
- #4780: Induction with universe polymorphism on was creating ill-typed terms.
+- #4754: Regression in setoid_rewrite, allow postponed unification problems to remain.
Changes from V8.5pl1 to V8.5pl2
===============================