Skip to content
Snippets Groups Projects
Commit 3bf85c54 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'nil-lemmas-changelog' into 'master'

Mention change to lemmas in changelog

See merge request iris/iris!469
parents 59a1ad49 7aa4ad8b
No related branches found
No related tags found
No related merge requests found
...@@ -211,6 +211,10 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -211,6 +211,10 @@ Coq development, but not every API-breaking change is listed. Changes marked
As part of this, the lemmas about the 3-mask variant were changed to be about As part of this, the lemmas about the 3-mask variant were changed to be about
the 2-mask variant instead, and `step_fupd_mask_mono` now also has a more the 2-mask variant instead, and `step_fupd_mask_mono` now also has a more
consistent argument order for its masks. consistent argument order for its masks.
* Slightly strengthen the lemmas `big_sepL_nil'`, `big_sepL2_nil'`,
`big_sepM_nil'` `big_sepM2_empty'`, `big_sepS_empty'`, and `big_sepMS_empty'`.
They now only require that the argument `P` is affine instead of the whole BI
being affine.
The following `sed` script should perform most of the renaming (FIXME: incomplete) The following `sed` script should perform most of the renaming (FIXME: incomplete)
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment