Skip to content
Snippets Groups Projects
Commit 4760ad33 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'changelog_upd' into 'master'

Mentioned big_sepL2/sepM2 in the changelog.

See merge request iris/iris!232
parents 58ae11ed b12759c2
No related branches found
No related tags found
No related merge requests found
...@@ -100,6 +100,10 @@ Changes in Coq: ...@@ -100,6 +100,10 @@ Changes in Coq:
steps that would require unlocking subterms. Every impure wp_ tactic executes steps that would require unlocking subterms. Every impure wp_ tactic executes
this tactic before doing anything else. this tactic before doing anything else.
* Add `big_sepM_insert_acc`. * Add `big_sepM_insert_acc`.
* Add big separating conjunctions that operate on pairs of lists (`big_sepL2`)
and on pairs of maps (`big_sepM2`). In the former case the lists are required
to have the same length, and in the latter case the maps are required to
have the same domains.
* The `_strong` lemmas (e.g. `own_alloc_strong`) work for all infinite * The `_strong` lemmas (e.g. `own_alloc_strong`) work for all infinite
sets, instead of just for cofinite sets. The versions with cofinite sets, instead of just for cofinite sets. The versions with cofinite
sets have been renamed to use the `_cofinite` suffix. sets have been renamed to use the `_cofinite` suffix.
......
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