From a76fec7a0356f7555299a04f9c65db658caddb77 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 20 Jun 2021 13:07:48 +0200
Subject: [PATCH] tweak changelog

---
 CHANGELOG.md | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c97830f99..d7c576cc6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,13 +33,9 @@ Coq 8.11 is no longer supported in this version of Iris.
   algorithm.
 * Set `Hint Mode` for the classes `OfeDiscrete`, `Dist`, `Unit`, `CmraMorphism`,
   `rFunctorContractive`, `urFunctorContractive`.
-* Also set `Hint Mode` for the stdpp class `Equiv`.
-  This might require few spurious type annotations until
-  https://github.com/coq/coq/issues/14441 is fixed.
-  This `Hint Mode` is not in stdpp due to Coq bugs
-  https://github.com/coq/coq/issues/5735 and
-  https://github.com/coq/coq/issues/9058, only fixed in Coq >= 8.12, which stdpp
-  supports and Iris does not.
+* Set `Hint Mode` for the stdpp class `Equiv`. This might require few spurious
+  type annotations until
+  [Coq bug #14441](https://github.com/coq/coq/issues/14441) is fixed.
 * Add `max_prefix_list` RA on lists whose composition is only defined when one
   operand is a prefix of the other. The result is the longer list.
 
-- 
GitLab