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

changelog

parent 6ad65f26
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 0 deletions
CHANGELOG.md
+ 1
− 0
View file @ de8da74a
...@@ -33,6 +33,7 @@ Coq 8.11 is no longer supported in this version of Iris. ...@@ -33,6 +33,7 @@ Coq 8.11 is no longer supported in this version of Iris.
* Add new lemmas `big_sepM2_delete_l` and `big_sepM2_delete_r`. * Add new lemmas `big_sepM2_delete_l` and `big_sepM2_delete_r`.
* Rename `big_sepM2_lookup_1` → `big_sepM2_lookup_l` and * Rename `big_sepM2_lookup_1` → `big_sepM2_lookup_l` and
`big_sepM2_lookup_2` → `big_sepM2_lookup_r`. `big_sepM2_lookup_2` → `big_sepM2_lookup_r`.
* Add lemmas for swapping nested big-ops: `big_sep{L,M,S,MS}_sep{L,M,S,MS}`.
**Changes in `proofmode`:** **Changes in `proofmode`:**
......
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