From 37b578f5627d4f428619158eb2906354644196e6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Aug 2024 22:29:11 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4fe7fcb46..5fab43e31 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,10 @@ lemma.
 * Change `iInduction` to always generate a magic wand instead of sometimes
   generating an implication for reverted hypotheses.
 * Add `iUnfold` tactic.
+* Improve ability to name induction hypotheses (IHs) in `iInduction`: when
+  performing `iInduction x as cpat` the names of the IHs in the Coq introduction
+  pattern `cpat` are used to name the IHs in the proof mode context. For
+  example, `iInduction n as [|n IH]` and `iInduction t as [|l IHl r IHr]`.
 
 **Changes in `base_logic`:**
 
-- 
GitLab