From fa59d087b82eff89568d0cb33a652e2db7749736 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 7 Mar 2023 18:25:37 +0100
Subject: [PATCH] CHANGELOG.

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 62d023ca6..dac4e1a0d 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`:**
-- 
GitLab