Merge Requests · Iris

finalize changelog for Iris 3.4 release

iris!639 · opened Feb 15, 2021 by Ralf Jung Iris 3.4
- MERGED
- 8
updated Feb 16, 2021
add better lemmas for working with mask-changing fupd, and rearrange names a bit

iris!637 · opened Feb 13, 2021 by Ralf Jung Iris 3.4
- MERGED
- 15
updated Mar 03, 2021
Remove `CopyDestruct` heuristic

iris!596 · opened Dec 02, 2020 by Robbert Krebbers Iris 3.4
- MERGED
- 19
updated Dec 06, 2020
Make `wp_apply` perform `wp_pure` in small steps until the lemma matches the goal.

iris!587 · opened Nov 12, 2020 by Robbert Krebbers Iris 3.4
- MERGED
- 20
updated Jan 27, 2021
Rename `mnat`/`mnat_auth` into `mono_nat`.

iris!572 · opened Nov 05, 2020 by Robbert Krebbers Iris 3.4
- MERGED
- 40
updated Dec 06, 2020
add big_sepS_elem_of_acc_impl

iris!570 · opened Nov 04, 2020 by Ralf Jung Iris 3.4
- MERGED
- 25
updated Jan 26, 2021
Add persistent points-to predicate to Iris

iris!554 · opened Oct 26, 2020 by Simon Friis Vindum Iris 3.4
- MERGED
- 118
updated Feb 01, 2021
Iris 3.3 changelog summary

iris!478 · opened Jul 14, 2020 by Ralf Jung Iris 3.3
- MERGED
- 9
updated Jul 15, 2020
Remove dec_agree and cofeT and use Coq #[deprecated] attribute for iAlways

iris!477 · opened Jul 14, 2020 by Ralf Jung Iris 3.3
- MERGED
- 8
updated Jul 15, 2020
All list "map singleton" lemmas consistently use `singletonM` in their name

iris!476 · opened Jul 14, 2020 by Ralf Jung Iris 3.3
- MERGED
- 6
updated Jul 15, 2020
mention that the ASCII syntax exists (but we recommend unicode)

iris!470 · opened Jul 04, 2020 by Ralf Jung Iris 3.3
- MERGED
- 3
updated Jul 15, 2020
adjust notation for step-taking updates

iris!462 · opened Jun 15, 2020 by Ralf Jung Iris 3.3
- MERGED
- 24
updated Dec 10, 2020
Fix scopes for `plainly` following !456.

iris!458 · opened May 28, 2020 by Paolo G. Giarrusso Iris 3.3
- MERGED
- 1
updated May 28, 2020
Remove redundant `%I` scopes in definitions.

iris!457 · opened May 28, 2020 by Robbert Krebbers Iris 3.3
- MERGED
- 5
updated May 28, 2020
Remove `Open Scope Z_scope` in HeapLang

iris!453 · opened May 27, 2020 by Robbert Krebbers Iris 3.3
- MERGED
- 10
updated May 28, 2020
Merge BI and SBI canonical structures 4 of 4 tasks completed

iris!441 · opened May 11, 2020 by Robbert Krebbers Iris 3.3
- MERGED
- 1
- 87
updated May 25, 2020
heap_lang: support deallocation

iris!439 · opened May 07, 2020 by Ralf Jung Iris 3.3 S-waiting-for-review T-heap_lang
- MERGED
- 62
updated May 25, 2020
Change ascii turnstile

iris!435 · opened Apr 23, 2020 by Gregory Malecha Iris 3.3
- MERGED
- 17
updated May 29, 2020
Fix `forall` parsing.

iris!432 · opened Apr 22, 2020 by Gregory Malecha Iris 3.3
- MERGED
- 27
updated May 28, 2020
heap_lang lifting: instantiate inv_heapG and inv_heap_inv

iris!429 · opened Apr 18, 2020 by Ralf Jung Iris 3.3 T-heap_lang
- MERGED
- 22
updated May 18, 2020