From 4de7d7fb63a68b766126ae467be1e9bc00b92948 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 9 Jun 2016 19:10:55 +0200
Subject: Reporting about a few bug fixes (to be continued).

---
 CHANGES | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 6a1f8f0e49..dada2ed975 100644
--- a/CHANGES
+++ b/CHANGES
@@ -3,8 +3,12 @@ Changes from V8.5pl1 to V8.5pl2
 
 Bugfixes
 
-- #4677: fix alpha-conversion in notations needing eta-expansion
+- #4677: fix alpha-conversion in notations needing eta-expansion.
 - Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode.
+- #4644: a regression in unification.
+- #4777: printing inefficiency with implicit arguments
+- #4752: CoqIDE crash on files not ended by ".v".
+- #4398: type_scope used consistently in "match goal".
 
 Changes from V8.5 to V8.5pl1
 ============================
-- 
cgit v1.2.3