diff --git a/CHANGELOG.md b/CHANGELOG.md
index 185bb7e8953b6a8bdeb8148a395c98973562fcdc..43ed2e39382c0fb3845c6e34476a8f636bdd31b5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,7 +36,7 @@ Coq 8.13 is no longer supported.
 * Use `binder` in notations for big ops. This means one can write things such
   as `[∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝`.
 * Add constructions `bi_tc`/`bi_nsteps` to create the transitive/`n`-step
-  closure of a PROP-level binary relation. (by  Simcha van Collem).
+  closure of a PROP-level binary relation. (by Simcha van Collem).
 * Make the `unseal` tactic of `monPred` more consistent with `uPred`:
   + Rename `MonPred.unseal` → `monPred.unseal`
   + No longer unfold derived BI connectives `<affine>`, `<absorb>` and `◇`.