diff --git a/CHANGELOG.md b/CHANGELOG.md
index db976b985f3fd3744a95dc612a5a8edb3247abf0..d9019babc26e4932e519a3ac468771d64bf9b575 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`:**