Merge branch 'ike/better-combine' into 'master'
Improve iCombine to allow a 'gives' clause for validity properties Closes #460 See merge request iris/iris!872
Showing
- CHANGELOG.md 13 additions, 0 deletionsCHANGELOG.md
- docs/proof_mode.md 8 additions, 1 deletiondocs/proof_mode.md
- iris/base_logic/lib/gen_heap.v 21 additions, 6 deletionsiris/base_logic/lib/gen_heap.v
- iris/base_logic/lib/gen_inv_heap.v 3 additions, 3 deletionsiris/base_logic/lib/gen_inv_heap.v
- iris/base_logic/lib/ghost_map.v 34 additions, 4 deletionsiris/base_logic/lib/ghost_map.v
- iris/base_logic/lib/ghost_var.v 22 additions, 2 deletionsiris/base_logic/lib/ghost_var.v
- iris/base_logic/lib/gset_bij.v 3 additions, 3 deletionsiris/base_logic/lib/gset_bij.v
- iris/base_logic/lib/later_credits.v 14 additions, 1 deletioniris/base_logic/lib/later_credits.v
- iris/base_logic/lib/mono_nat.v 2 additions, 2 deletionsiris/base_logic/lib/mono_nat.v
- iris/base_logic/lib/na_invariants.v 1 addition, 1 deletioniris/base_logic/lib/na_invariants.v
- iris/base_logic/lib/own.v 13 additions, 0 deletionsiris/base_logic/lib/own.v
- iris/base_logic/lib/proph_map.v 1 addition, 1 deletioniris/base_logic/lib/proph_map.v
- iris/base_logic/lib/saved_prop.v 23 additions, 4 deletionsiris/base_logic/lib/saved_prop.v
- iris/base_logic/proofmode.v 14 additions, 0 deletionsiris/base_logic/proofmode.v
- iris/bi/lib/fractional.v 11 additions, 5 deletionsiris/bi/lib/fractional.v
- iris/program_logic/ownp.v 4 additions, 4 deletionsiris/program_logic/ownp.v
- iris/proofmode/class_instances.v 47 additions, 0 deletionsiris/proofmode/class_instances.v
- iris/proofmode/class_instances_embedding.v 10 additions, 0 deletionsiris/proofmode/class_instances_embedding.v
- iris/proofmode/class_instances_later.v 30 additions, 0 deletionsiris/proofmode/class_instances_later.v
- iris/proofmode/classes.v 66 additions, 2 deletionsiris/proofmode/classes.v
Loading
Please register or sign in to comment