CHANGES for this branch.

1 files changed, 10 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 1b74e783d..7f171ebc4 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