From 826e140ea22aa20d29f67f7a78d7b7596d9ea672 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 21 Jul 2023 12:59:57 +0000
Subject: [PATCH] Improve CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index db976b985..d9019babc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -94,7 +94,8 @@ Coq 8.13 is no longer supported.
     `iDestruct`/`iCombine`/`iSplitL`/`iSplitR` should be used instead.
 * Add missing transitivity, symmetry and reflexivity lemmas about the `↔`, `→`,
   `-∗` and `∗-∗` connectives. (by Ike Mulder)
-* Add `∗-∗` as notation in `stdpp_scope` similar to `-∗`.
+* Add `∗-∗` as notation in `stdpp_scope` similar to `-∗`. This means `P ∗-∗ Q`
+  can be directly used as lemma statement, and is syntactic sugar for `⊢ P ∗-∗ Q`
 
 **Changes in `proofmode`:**
 
-- 
GitLab