From 2e873a3a254653a47117ed8bf074703483c8f9c7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 28 Oct 2017 11:09:20 +0200
Subject: [PATCH] Add note about iIntros/iAlways to CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9a1bebc64..210aef4fa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -65,6 +65,12 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
     mode.
   - Many missing type class instances for distributing connectives have been
     defined.
+  - The tactics `iIntros (?)` and `iIntros "!#"` (i.e. `iAlways`) are now
+    implemented using type classes. That way, they are more generic, e.g.
+    `iIntros (?)` also works when the universal quantifier is below a modality,
+    and `iAlways` also works for the plainness modality. A breaking change,
+    however, is that these tactics now no longer work when the universal
+    quantifier or modality is behind a type class opaque definition.
 * The generic `fill` operation of the `ectxi_language` construct has been
   defined in terms of a left fold instead of a right fold. This gives rise to
   more definitional equalities.
-- 
GitLab