- Nov 12, 2020
- Nov 11, 2020
-
-
Ralf Jung authored -
Robbert Krebbers authored
Add back a proofmode test for issue #288 See merge request iris/iris!584
-
Robbert Krebbers authored
Use original pattern in iDestruct error messages See merge request iris/iris!550
-
Tej Chajed authored
This test is incompatible with Coq 8.8 and Coq 8.9, but Iris no longer supports those versions.
-
Tej Chajed authored
-
Ralf Jung authored
multi-package repositories See merge request iris/iris!514
-
Tej Chajed authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
add big_opM_singletons See merge request iris/iris!567
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
avoid (e)apply in wp_expr_eval See merge request iris/iris!582
-
Ralf Jung authored
-
- Nov 10, 2020
-
-
Ralf Jung authored
Rename mapsto_mapsto_ne and add easier-to-use variant See merge request iris/iris!574
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
provide _big variant of gen_heap_init Closes #361 See merge request iris/iris!580
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Documentation on Iris equalities (take 2) See merge request iris/iris!575
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
split RA docs into separate file, and general doc updates See merge request iris/iris!576
-
Ralf Jung authored
-
Ralf Jung authored
Seal ghost_var and mnat_own See merge request iris/iris!571
-
Ralf Jung authored
-
Ralf Jung authored
fix wp_bind with empty context See merge request iris/iris!579
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
wp_pures: also handle [WP v] See merge request iris/iris!578
-
Ralf Jung authored
-
Robbert Krebbers authored
-
