From 21bc4cba55b4485cf06e8b8474a3e805de4642d6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 22 Apr 2023 19:55:58 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 76e52259..b48144f3 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`).
-- 
GitLab