From b3911c16a9bf535cee5879e554eaf767a363cd40 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 8 Jun 2021 13:32:44 +0200
Subject: [PATCH] Changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0c19f8792..607fdf3d9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -31,6 +31,8 @@ Coq 8.11 is no longer supported in this version of Iris.
   `Dist`, `Op`, `Valid`, `ValidN`, `Unit`, `PCore` now use an `Hint Extern`
   based on `refine` instead of `apply`, in order to use Coq's newer unification
   algorithm.
+* Set `Hint Mode` for the classes `OfeDiscrete`, `Unit`, `CmraMorphism`,
+  `rFunctorContractive`, `urFunctorContractive`.
 
 **Changes in `bi`:**
 
-- 
GitLab