From 1b72a945c383afac268df40039dfa4d0147b871d Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 26 May 2021 13:04:10 +0200 Subject: [PATCH] add mask mismatch errors to changelog --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2e30d10d3..a06fb856e 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`:** -- GitLab