From 4f30083074dbe4e923d9c4f2c13632664122ba8d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 22 Nov 2019 23:07:46 +0100
Subject: [PATCH] Tweak changelog.

---
 CHANGELOG.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c59f48658..aa35700db 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,7 +33,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   This has two consequences:
   1. Coq's "new" unification algorithm (the one in `refine`, not the "old" one
      in `apply`) is used more often by the proof mode tactics.
-  2. TC constraints are solved eagerly, see https://github.com/coq/coq/issues/6583.
+  2. Due to the use of `notypeclasses refine`, TC constraints are solved less
+     eagerly, see https://github.com/coq/coq/issues/6583.
   In order to port your development, it is often needed to instantiate evars
   explicitly (since TC search is performed less eagerly), and in few cases it is
   needed to unfold definitions explicitly (due to new unification algorithm
-- 
GitLab