diff --git a/CHANGELOG.md b/CHANGELOG.md index 2e30d10d353453c07d955ac36ae6ae7ccff366ca..a06fb856e5333516dd361c63fa7bdffe399fdfde 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -42,6 +42,8 @@ Coq 8.11 is no longer supported in this version of Iris. https://gitlab.mpi-sws.org/iris/string-ident. (by Tej Chajed) * Add support for destructing existentials with the intro pattern `[%x ...]`. (by Tej Chajed) +* `iMod`/`iModIntro` show proper error messages when they fail due to mask + mismatches. **Changes in `bi`:**