From 518bd3c41fc08dfcd690eba99cf8bb818ddf51df Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 30 May 2023 07:42:36 +0200 Subject: [PATCH] CHANGELOG. --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index cd33b8853..e926aad99 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -74,6 +74,7 @@ Coq 8.13 is no longer supported. particular, replace `apply` by `iApply`). - Add some `apply bi.entails_wand`/`apply bi.wand_entails` to 'convert' between the old and new way of interpreting `P -∗ Q`. +* Add `auto` hint to introduce the BI version of `↔`. **Changes in `proofmode`:** -- GitLab