From aa6ecfbb66ed26b9fd91714a028287627f1add6c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Jul 2018 07:57:30 +0200
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8bba3a075..90c021cbc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,6 +36,8 @@ Changes in Coq:
 * The `iInv` tactic can now be used without the second argument (the name for
   the closing update).  It will then instead add the obligation to close the
   invariant to the goal.
+* Added support for defining derived connectives involving n-ary binders using
+  telescopes.
 * Improved pretty-printing of Iris connectives (in particular WP and fancy
   updates) when Coq has to line-wrap the output.
 * Rename `timelessP` -> `timeless` (projection of the `Timeless` class)
-- 
GitLab