From d03e27800ec51538701b606fb7be196e4693780a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Nov 2016 15:14:44 +0100
Subject: CHANGES for this branch.

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

diff --git a/CHANGES b/CHANGES
index 1b74e783dd..7f171ebc40 100644
--- a/CHANGES
+++ b/CHANGES
@@ -82,6 +82,16 @@ Hints
 - Hint Mode now accepts "!" which means that the mode matches only if the
   argument's head is not an evar (it goes under applications, casts, and
   scrutinees of matches and projections).
+- Hints can now take an optional user-given pattern, used only by
+  [typeclasses eauto] with the [Filtered Unification] option on.
+
+Typeclasses
+
+- Many new options and new engine based on the proof monad. The
+  [typeclasses eauto] tactic is now a multi-goal, multi-success tactic.
+  See reference manual for more information. It is planned to
+  replace auto and eauto in the following version. The 8.5 resolution
+  engine is still available to help solve compatibility issues.
 
 Program
 
-- 
cgit v1.2.3