diff --git a/CHANGELOG.md b/CHANGELOG.md
index 76e52259f4a6bd8c20c056964477e7493f848157..b48144f3abf8641bc735abf426770b7d8de83a31 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -37,6 +37,7 @@ Coq 8.12 and 8.13 are no longer supported by this release.
   Lesbre)
 - Add proof that `vec` is `Finite`. (by Herman Bergwerf.)
 - Add `min` and `max` infix notations for `positive`.
+- Set `simpl never` for `Pos` and `N` operations (similar to `Z`).
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).