diff --git a/CHANGELOG.md b/CHANGELOG.md index 8bba3a075517781b703b56e21fafbb9abe89823c..90c021cbc67492e6ed60673d6684b2784cd1eca7 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)