Merge Requests · Iris

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
Add `big_sepL2_app_inv_2`.

iris!292 · opened Jul 12, 2019 by Dan Frumin Iris 3.2
- MERGED
- 9
updated Nov 24, 2020
Get rid of a superflous argument to `fresh_locs`.

iris!288 · opened Jul 09, 2019 by Dan Frumin
- MERGED
- 4
updated Nov 24, 2020
Add `head_prim_fill_reducible`.

iris!293 · opened Jul 12, 2019 by Dan Frumin Iris 3.2
- MERGED
- 4
updated Nov 24, 2020
Add simplification instance for list ≠ [], needed for quicksort

refinedc!4 · opened Nov 24, 2020 by Ike Mulder
- MERGED
- 3
updated Nov 24, 2020
move algebra.base -> prelude.prelude

iris!586 · opened Nov 12, 2020 by Ralf Jung
- MERGED
- 9
updated Nov 12, 2020
adding allocation range ghost state.

refinedc!3 · opened Nov 05, 2020 by Rodolphe Lepigre
- MERGED
- 0
updated Nov 12, 2020
Set `Hint Mode` for `pretty`.

stdpp!201 · opened Nov 12, 2020 by Robbert Krebbers
- MERGED
- 2
updated Nov 12, 2020
Add back a proofmode test for issue #288

iris!584 · opened Nov 11, 2020 by Tej Chajed
- MERGED
- 1
updated Nov 11, 2020
Use original pattern in iDestruct error messages

iris!550 · opened Oct 20, 2020 by Tej Chajed S-waiting-for-review
- MERGED
- 28
updated Nov 11, 2020
Pretty-print 0 as "0" for N, Z, and nat

stdpp!200 · opened Nov 09, 2020 by Robbert Krebbers
- MERGED
- 3
updated Nov 11, 2020
multi-package repositories

iris!514 · opened Sep 26, 2020 by Ralf Jung S-waiting-for-review
- MERGED
- 1
- 31
updated Nov 11, 2020
add big_opM_singletons

iris!567 · opened Nov 04, 2020 by Ralf Jung
- MERGED
- 10
updated Nov 11, 2020
avoid (e)apply in wp_expr_eval

iris!582 · opened Nov 11, 2020 by Ralf Jung
- MERGED
- 2
updated Nov 11, 2020
wp_pures: also handle [WP v]

iris!578 · opened Nov 09, 2020 by Ralf Jung
- MERGED
- 5
updated Nov 11, 2020
Rename mapsto_mapsto_ne and add easier-to-use variant

iris!574 · opened Nov 05, 2020 by Ralf Jung
- MERGED
- 8
updated Nov 10, 2020