Merge branch 'ralf/fupd-mask' into 'master'
add better lemmas for working with mask-changing fupd, and rearrange names a bit See merge request iris/iris!637
No related branches found
No related tags found
Showing
- CHANGELOG.md 14 additions, 0 deletionsCHANGELOG.md
- iris/base_logic/lib/fancy_updates.v 4 additions, 4 deletionsiris/base_logic/lib/fancy_updates.v
- iris/base_logic/lib/invariants.v 2 additions, 2 deletionsiris/base_logic/lib/invariants.v
- iris/bi/lib/atomic.v 3 additions, 3 deletionsiris/bi/lib/atomic.v
- iris/bi/monpred.v 1 addition, 1 deletioniris/bi/monpred.v
- iris/bi/updates.v 64 additions, 28 deletionsiris/bi/updates.v
- iris/program_logic/adequacy.v 3 additions, 4 deletionsiris/program_logic/adequacy.v
- iris/program_logic/ectx_lifting.v 1 addition, 2 deletionsiris/program_logic/ectx_lifting.v
- iris/program_logic/lifting.v 5 additions, 5 deletionsiris/program_logic/lifting.v
- iris/program_logic/ownp.v 4 additions, 4 deletionsiris/program_logic/ownp.v
- iris/program_logic/total_lifting.v 3 additions, 3 deletionsiris/program_logic/total_lifting.v
- iris/program_logic/total_weakestpre.v 2 additions, 1 deletioniris/program_logic/total_weakestpre.v
- iris/program_logic/weakestpre.v 2 additions, 1 deletioniris/program_logic/weakestpre.v
- tests/proofmode_monpred.v 4 additions, 4 deletionstests/proofmode_monpred.v
Loading
Please register or sign in to comment