From 45b9c079cba99dcad694daf6205943066d9d6cf8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 09:59:35 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 420d3949f..a8934aa4b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -81,6 +81,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context.
 * Add notion `ofe_iso A B` that states that OFEs `A` and `B` are isomorphic.
 * Make use of `ofe_iso` in the COFE solver.
+* The functions `{o,r,ur}Functor_diag` are no longer coercions, and renamed into
+  `{o,r,ur}Functor_apply` to better match their intent.
 
 **Changes in heap_lang:**
 
-- 
GitLab