From 5f73bf42c53d5ca23890709be2bb1add966c9acb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 Apr 2022 23:36:24 +0200
Subject: [PATCH] CHANGELOG.
---
CHANGELOG.md | 1 +
1 file changed, 1 insertion(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 518d58d5d..ac6566191 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,6 +21,7 @@ lemma.
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).
+* `iRevert` of a pure hypothesis generates a wand instead of an implication.
**Changes in `base_logic`:**
--
GitLab