Merge Requests · Iris

Remove `CopyDestruct` heuristic

iris!596 · opened Dec 02, 2020 by Robbert Iris 3.4
- MERGED
- 19
updated Dec 06, 2020
Rename `mnat`/`mnat_auth` into `mono_nat`.

iris!572 · opened Nov 05, 2020 by Robbert Iris 3.4
- MERGED
- 40
updated Dec 06, 2020
Add persistent points-to predicate to Iris

iris!554 · opened Oct 26, 2020 by Simon Friis Vindum Iris 3.4
- MERGED
- 118
updated Dec 18, 2020
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 Iris 3.3
- MERGED
- 5
updated May 28, 2020
Remove `Open Scope Z_scope` in HeapLang

iris!453 · opened May 27, 2020 by Robbert 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 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
Add support for pure names in intro patterns

iris!400 · opened Mar 23, 2020 by Tej Chajed Iris 3.3
- MERGED
- 3
- 90
updated Apr 17, 2020
ASCII notation

iris!396 · opened Mar 18, 2020 by Gregory Malecha Iris 3.3
- MERGED
- 154
updated Apr 08, 2020
Fix issue #260: Error message when iLöb used on non-SBI

iris!302 · opened Aug 12, 2019 by Robbert Iris 3.2
- MERGED
- 6
updated Aug 13, 2019
Fix issue #259: Error message when iRevert is used on out of scope variable

iris!301 · opened Aug 12, 2019 by Robbert Iris 3.2
- MERGED
- 7
updated Aug 13, 2019