diff --git a/CHANGELOG.md b/CHANGELOG.md index 09cab0b53989626127684da09a02515bd6855f3e..bde91d87d7504c3c76d81607f6e93db8a1c64f97 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)