diff --git a/CHANGELOG.md b/CHANGELOG.md
index c566a6ed907a7f2395be815916a092e3f9993949..9a7e7e6c0f03362798126b59909ffe30215b3547 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -144,13 +144,15 @@ Coq 8.13 is no longer supported.
   classes, their results may have become more concise.
 * Support n-ary versions of `iIntros`, `iRevert`, `iExists`, `iDestruct`, `iMod`,
   `iFrame`, `iRevertIntros`, `iPoseProof`, `iInduction`, `iLöb`, `iInv`, and
-  `iAssert`. (by Jan-Oliver Kaiser, and Rodolphe Lepigre)
+  `iAssert`. (by Jan-Oliver Kaiser and Rodolphe Lepigre)
 * Add tactics `ltac1_list_iter` and `ltac1_list_rev_iter` to iterate over
-  lists of `ident`s/`simple intropatterns`/`constr`/etc using Ltac1. To read how
+  lists of `ident`s/`simple intropatterns`/`constr`/etc using Ltac1. See
+  [iris/proofmode/base.v](proofmode/base.v) for documentation on how
   to use these tactics to convert your own fixed arity tactics to an n-ary
-  variant, see [iris/proofmode/base.v](proofmode/base.v).
-* The tactic `iIntros` will always call `iStartProof`, so even `iIntros (x)`. If
-  you do not want to start the proof mode, use ordinary `intros`.
+  variant.
+* The tactic `iIntros` will always call `iStartProof`, even when there is no Iris
+  pattern such as in `iIntros (x)`. If you do not want to start the proof mode,
+  use ordinary `intros`.
 
 **Changes in `base_logic`:**