From e9e006988baba7c57d670bfc84ba1dbde49b47b7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 5 Feb 2020 17:44:45 +0100
Subject: [PATCH] CHANGELOG entry for the `-# pat` intro pattern.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 09cab0b53..bde91d87d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -65,6 +65,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   lemmas is through `iInv`, and that does not change.)
 * Added a construction `bi_rtc` to create reflexive transitive closures of
   PROP-level binary relations.
+* Add new introduction pattern `-# pat` that moves a hypothesis from the
+  intuitionistic context to the spatial context.
 
 ## Iris 3.2.0 (released 2019-08-29)
 
-- 
GitLab