From 8f1ed633426beb3ace044b4515ed54c158cefd23 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Apr 2023 20:19:08 +0200
Subject: [PATCH] Tweak changelog for `persistently_True`.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7747ffdae..92bfbe9eb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -47,7 +47,8 @@ Coq 8.13 is no longer supported.
 * Add compatibility lemmas for `big_sepL <-> big_sepL2`, `big_sepM <-> big_sepM2`
   with list/maps of pairs; and `big_sepM <-> big_sepL` via `list_to_map` and
   `map_to_list`. (by Dorian Lesbre).
-- Make `persistently_True` a bi-entailment.
+- Make `persistently_True` a bi-entailment; this changes the default `rewrite`
+  direction.
 - Make `BiLaterContractive` a class instead of a notation.
 
 **Changes in `proofmode`:**
-- 
GitLab