Merge branch 'undiscard-laws' into 'master'
Add laws to allow "undiscarding" points-tos See merge request iris/iris!960
Showing
- CHANGELOG.md 16 additions, 0 deletionsCHANGELOG.md
- iris/algebra/auth.v 4 additions, 0 deletionsiris/algebra/auth.v
- iris/algebra/dfrac.v 17 additions, 0 deletionsiris/algebra/dfrac.v
- iris/algebra/dyn_reservation_map.v 1 addition, 1 deletioniris/algebra/dyn_reservation_map.v
- iris/algebra/lib/dfrac_agree.v 8 additions, 0 deletionsiris/algebra/lib/dfrac_agree.v
- iris/algebra/lib/gmap_view.v 39 additions, 20 deletionsiris/algebra/lib/gmap_view.v
- iris/algebra/lib/mono_Z.v 3 additions, 0 deletionsiris/algebra/lib/mono_Z.v
- iris/algebra/lib/mono_list.v 3 additions, 0 deletionsiris/algebra/lib/mono_list.v
- iris/algebra/lib/mono_nat.v 3 additions, 0 deletionsiris/algebra/lib/mono_nat.v
- iris/algebra/updates.v 21 additions, 0 deletionsiris/algebra/updates.v
- iris/algebra/view.v 58 additions, 7 deletionsiris/algebra/view.v
- iris/base_logic/lib/gen_heap.v 5 additions, 0 deletionsiris/base_logic/lib/gen_heap.v
- iris/base_logic/lib/ghost_map.v 11 additions, 0 deletionsiris/base_logic/lib/ghost_map.v
- iris/base_logic/lib/saved_prop.v 21 additions, 0 deletionsiris/base_logic/lib/saved_prop.v
- iris_heap_lang/primitive_laws.v 2 additions, 0 deletionsiris_heap_lang/primitive_laws.v
Loading
Please register or sign in to comment