From a40420601410c5d6f86ff40c5f0b0e723d171833 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 26 Jul 2016 14:08:07 +0200
Subject: Update CHANGES about critical bugfix and others

---
 CHANGES | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 5b7db5c383..97a803b820 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
 ===============================
-- 
cgit v1.2.3


From 25ef9dda0311213bb2f6e2b9cd0b87be2128599b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 25 Jul 2016 15:44:53 +0200
Subject: Fix #4769, univ poly and elim schemes in sections

---
 CHANGES | 1 +
 1 file changed, 1 insertion(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 97a803b820..12413f495a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,7 @@ Other bugfixes
 
 - #4780: Induction with universe polymorphism on was creating ill-typed terms.
 - #4754: Regression in setoid_rewrite, allow postponed unification problems to remain.
+- #4769: Anomaly with universe polymorphic schemes defined inside sections.
 
 Changes from V8.5pl1 to V8.5pl2
 ===============================
-- 
cgit v1.2.3


From 639eecd27e42c7dd646afdcb67b5a4e51a4541c1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 29 Jul 2016 19:36:59 +0200
Subject: Update CHANGES about #3886 bugfix

---
 CHANGES | 1 +
 1 file changed, 1 insertion(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 12413f495a..863c27e477 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,7 @@ Other bugfixes
 - #4780: Induction with universe polymorphism on was creating ill-typed terms.
 - #4754: Regression in setoid_rewrite, allow postponed unification problems to remain.
 - #4769: Anomaly with universe polymorphic schemes defined inside sections.
+- #3886: Program: duplicate obligations of mutual fixpoints
 
 Changes from V8.5pl1 to V8.5pl2
 ===============================
-- 
cgit v1.2.3


From ba5c882c6c174170d18fe01f36863ca592065671 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 25 Jul 2016 13:40:41 +0200
Subject: Fix bug #4673: regression in setoid_rewrite.

Modulo delta for types should be fully transparent.
---
 CHANGES | 1 +
 1 file changed, 1 insertion(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 863c27e477..e6b5b3206e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,7 @@ Critical bugfix
 Other bugfixes
 
 - #4780: Induction with universe polymorphism on was creating ill-typed terms.
+- #4673: regression in setoid_rewrite, unfolding let-ins for type unification.
 - #4754: Regression in setoid_rewrite, allow postponed unification problems to remain.
 - #4769: Anomaly with universe polymorphic schemes defined inside sections.
 - #3886: Program: duplicate obligations of mutual fixpoints
-- 
cgit v1.2.3


From 2f26c2fd368a10b89273712e3de64bbd83aedc59 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 7 Aug 2016 23:56:32 +0200
Subject: Fix #5000: Document the native compiler soundness bug due to Unicode
 mangling.

---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index e6b5b3206e..c74aa7234c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,6 +17,8 @@ Changes from V8.5pl1 to V8.5pl2
 
 Critical bugfix
 - Checksums of .vo files dependencies were not correctly checked.
+- Unicode-to-ASCII translation was not injective, leading in a soundness bug in
+  the native compiler.
 
 Other bugfixes
 
-- 
cgit v1.2.3