diff --git a/CHANGELOG.md b/CHANGELOG.md index 07970642ff5ae7a69aefd5ffd9dae7fa64c68f5d..17fa7dac71a5c4b8d7d62859dfe059892feb02db 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -52,7 +52,7 @@ Coq 8.11 is no longer supported in this version of Iris. explicit coercions in a few cases, in particular `WP v {{ Φ }}` must now be written `WP (of_val v) {{ Φ }}`. * Improve `make_laterable`: - - Adjust definition such that `Laterable P` iff `P ⊢ make_laterable `. + - Adjust definition such that `Laterable P` iff `P ⊢ make_laterable P`. As a consequence, `make_laterable_elim` got weaker: elimination now requires an except-0 modality (`make_laterable P -∗ ◇ P`). - Add `iModIntro` support for `make_laterable`.