From 74ed6cfae54594e902e07543a67491107e995e8e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 29 Mar 2025 11:06:05 +0100
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index aa7d81e2..7174279f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,6 +23,9 @@ API-breaking change is listed.
   implementation detail. `stdpp.list_numbers` is now re-exported by `stdpp.list`
   and also considered part of the list module, so existing imports should be
   updated.
+- Remove `list_remove` and `list_remove_list`. There were no lemmas about these
+  functions; they existed solely to facilitate the proofs of decidability of
+  `submseteq` and `≡ₚ`, which have been refactored.
 
 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