diff --git a/CHANGELOG.md b/CHANGELOG.md
index 090c811a57df0f918cec19d51e34ab8c695ecda5..23cd9f4b3a88664500314619675d8478316c3b55 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -32,7 +32,8 @@ Changes in Coq:
     `iNext` and `iAlways`.
   - General infrastructure for deriving a logic for monotone predicates over
     an existing logic (see the paper for more details).
-  Developments instantiating the proof mode typeclasses may need significant
+
+    Developments instantiating the proof mode typeclasses may need significant
   changes.  For developments just using the proof mode tactics, porting should
   not be too much effort.  Notable things to port are:
   - All the BI laws moved from the `uPred` module to the `bi` module.  For