From cde5ccd91a2c46ada7b772f260926988351fab3a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 27 Sep 2021 15:47:06 -0400
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 527ad612..be362899 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -165,6 +165,11 @@ API-breaking change is listed.
 - 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>`.
+- Optimize `f_equiv` by doing more syntactic checking before handing off to
+  unification. This can make some uses 50x faster, but also makes the tactic
+  slightly weaker in case the left-hand side and right-hand side of the relation
+  call a function with arguments that are convertible but not syntactically
+  equal.
 
 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