diff --git a/CHANGELOG.md b/CHANGELOG.md
index 62d023ca6a1edc4eb460ab17187b0e982dd26220..dac4e1a0d516f559def5343f72e41f7e10a83274 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -27,6 +27,8 @@ Coq 8.13 is no longer supported.
     For backwards compatibility for existing developments, the tactic
     `f_contractive_fin` is provided. It uses the old definition of `dist_later`,
     now called `dist_later_fin`.
+  - If you need to deal with a `dist_later`/`dist_later_fin` in a manual proof,
+    use the tactic `dist_later_intro`/`dist_later_fin_intro` to introduce it.
   (by Michael Sammler, Lennard Gäher, and Simon Spies).
 
 **Changes in `bi`:**