Merge Requests · Iris

make pure_exec_fill not an instance any more

iris!588 · opened Nov 13, 2020 by Ralf Jung
- MERGED
- 16
updated Nov 29, 2020
Add a good failure state for allocation failure 6 of 6 tasks completed

refinedc!5 · opened Nov 26, 2020 by Rodolphe Lepigre
- MERGED
- Approved
- 0
updated Nov 27, 2020
bupd, fupd: add idempotence lemmas

iris!592 · opened Nov 26, 2020 by Ralf Jung
- MERGED
- 0
updated Nov 26, 2020
Replace unused pattern variables with underscore

stdpp!203 · opened Nov 21, 2020 by Tej Chajed
- MERGED
- 1
- 8
updated Nov 26, 2020
Replace `C`s with `O`s since we use OFEs instead of COFEs.

iris!263 · opened Jun 11, 2019 by Robbert Iris 3.2
- MERGED
- 18
updated Nov 24, 2020
ltac_tactics.v: drop dead branch

iris!273 · opened Jun 15, 2019 by Paolo G. Giarrusso
- MERGED
- 17
updated Nov 24, 2020
Add stuck_fill lemma.

iris!276 · opened Jun 20, 2019 by Hai Dang
- MERGED
- 2
updated Nov 24, 2020
Fix parsing precedence for iEval

iris!269 · opened Jun 14, 2019 by Paolo G. Giarrusso
- MERGED
- 10
updated Nov 24, 2020
show auth_update_core_id

iris!282 · opened Jun 27, 2019 by Ralf Jung
- MERGED
- 7
updated Nov 24, 2020
comparison: treat prophecies like unit and make all closures equal

iris!270 · opened Jun 14, 2019 by Ralf Jung
- MERGED
- 1
- 17
updated Nov 24, 2020
Add clairvoyant_coin example

iris!266 · opened Jun 13, 2019 by Amin Timany
- MERGED
- 20
updated Nov 24, 2020
Fix typos in comments

iris!281 · opened Jun 24, 2019 by Paolo G. Giarrusso
- MERGED
- 1
updated Nov 24, 2020
Fix sed on mac for real

iris!277 · opened Jun 21, 2019 by Paolo G. Giarrusso
- MERGED
- 3
updated Nov 24, 2020
Cofe and cFunctor for sigT

iris!278 · opened Jun 21, 2019 by Paolo G. Giarrusso
- MERGED
- 99
updated Nov 24, 2020
Turn CAS from compare-and-set to compare-and-swap

iris!274 · opened Jun 19, 2019 by Ralf Jung
- MERGED
- 53
updated Nov 24, 2020
provide a lemma to update only the authoritative part, ignoring the fragments entirely

iris!284 · opened Jul 03, 2019 by Ralf Jung
- MERGED
- 8
updated Nov 24, 2020
show that pair construction commutes with taking the core

iris!286 · opened Jul 07, 2019 by Ralf Jung Iris 3.2
- MERGED
- 6
updated Nov 24, 2020
Prove sigT_equivI is admissible (fix #250)

iris!280 · opened Jun 24, 2019 by Paolo G. Giarrusso
- MERGED
- 12
updated Nov 24, 2020
heap_lang: Make binary "=" operator partial, to sync with CmpXchg

iris!283 · opened Jun 29, 2019 by Ralf Jung Iris 3.2 T-heap_lang
- MERGED
- 9
updated Nov 24, 2020
Mark projections for sigTO as NonExpansive and Proper

iris!285 · opened Jul 06, 2019 by Paolo G. Giarrusso Iris 3.2
- MERGED
- 15
updated Nov 24, 2020