Commit 2877be8a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

CHANGELOG.

parent a932b194
......@@ -45,6 +45,9 @@ With this release, we dropped support for Coq 8.9.
if the result after framing is `True` or `emp`. In particular, it no longer
removes `<affine>` if the result after framing is affine, and it no longer
removes `□` if the result after framing is intuitionistic.
* Allow framing below an `<affine>` modality if the hypothesis that is framed is
affine. (Previously, framing below `<affine>` was only possible if the
hypothesis that is framed resides in the intuitionistic context.)
**Changes in `base_logic`:**
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment