From b203a304af261967ef91a8faee8b62496bfb3d60 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 2 Feb 2022 12:45:19 +0100
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 55208174e..a6dd68403 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,8 @@ lemma.
    to occur when the conclusion contains variables that are not in scope of the
    evar, thus blocking the default behavior of instantiating the premise with
    the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
+* `iInduction` now supports induction schemes that involve `Forall` and
+  `Forall2` (for example, for trees with finite branching).
 
 ## Iris 3.6.0 (2022-01-22)
 
-- 
GitLab