From c00c740b69f3c295e1e40c4b858c3f9d13dc8994 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 27 Sep 2021 09:08:59 -0400
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 83f4cb9b..527ad612 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -162,6 +162,9 @@ API-breaking change is listed.
 - Make `Forall2_nil`, `Forall2_cons` bidirectional lemmas with `Forall2_nil_2`,
   `Forall2_cons_2` being the original one-directional versions (matching
   `Forall_nil` and `Forall_cons`). Rename `Forall2_cons_inv` to `Forall2_cons_1`.
+- Enable `f_equiv` (and by extension `solve_proper`) to handle goals of the form
+  `f x ≡ g x` when `f ≡ g` is in scope, where `f` has a type like Iris's `-d>`
+  and `-n>`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
-- 
GitLab