From cbbb2896881bf60203c2c510c0d01b891dd6e73e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 22 Nov 2019 21:18:10 +0100
Subject: [PATCH] edit changelog

---
 CHANGELOG.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1a2e928df..c59f48658 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -31,8 +31,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Make use of `notypeclasses refine` in the implementation of `iPoseProof` and
   `iAssumption`, see https://gitlab.mpi-sws.org/iris/iris/merge_requests/329
   This has two consequences:
-  1. Coq's new unification algorithm is used more often by the proof mode
-     tactics
+  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.
   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
-- 
GitLab