diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7ec06e5f684e85d0195f78fff274351e9358288d..74d202bc9dc2a0d8a3fdf51abb2428b02e16914d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,9 @@ API-breaking change is listed.
 
 ## std++ 1.1.0 (unfinished)
 
+Coq 8.5 is no longer supported by this release of std++.  Use std++ 1.0 if you
+have to use Coq 8.5.
+
 New features:
 
 - Many new lemmas about lists, vectors, sets, maps.
@@ -20,6 +23,8 @@ New features:
 Changes:
 
 - Get rid of `Automatic Coercions Import`, it is deprecated.
+  Also get rid of `Set Asymmetric Patterns`.
+- Various changes and improvements to `f_equiv` and `solve_proper`.
 - `Hint Mode` is now set for all operational type classes to make instance
   search less likely to diverge.
 - New type class `RelDecision` for decidable relations, and `EqDecision` is