Merge branch 'has-lc' into 'master'
track has_lc directly in invGS/irisGS/heapGS rather than via separate typeclass See merge request iris/iris!816
Showing
- CHANGELOG.md 28 additions, 25 deletionsCHANGELOG.md
- iris/base_logic/lib/boxes.v 2 additions, 2 deletionsiris/base_logic/lib/boxes.v
- iris/base_logic/lib/cancelable_invariants.v 2 additions, 2 deletionsiris/base_logic/lib/cancelable_invariants.v
- iris/base_logic/lib/fancy_updates.v 37 additions, 46 deletionsiris/base_logic/lib/fancy_updates.v
- iris/base_logic/lib/gen_inv_heap.v 4 additions, 4 deletionsiris/base_logic/lib/gen_inv_heap.v
- iris/base_logic/lib/invariants.v 3 additions, 3 deletionsiris/base_logic/lib/invariants.v
- iris/base_logic/lib/na_invariants.v 2 additions, 2 deletionsiris/base_logic/lib/na_invariants.v
- iris/program_logic/adequacy.v 38 additions, 49 deletionsiris/program_logic/adequacy.v
- iris/program_logic/atomic.v 2 additions, 2 deletionsiris/program_logic/atomic.v
- iris/program_logic/ectx_lifting.v 1 addition, 1 deletioniris/program_logic/ectx_lifting.v
- iris/program_logic/lifting.v 1 addition, 1 deletioniris/program_logic/lifting.v
- iris/program_logic/ownp.v 6 additions, 6 deletionsiris/program_logic/ownp.v
- iris/program_logic/total_adequacy.v 9 additions, 9 deletionsiris/program_logic/total_adequacy.v
- iris/program_logic/total_ectx_lifting.v 1 addition, 1 deletioniris/program_logic/total_ectx_lifting.v
- iris/program_logic/total_lifting.v 1 addition, 1 deletioniris/program_logic/total_lifting.v
- iris/program_logic/total_weakestpre.v 9 additions, 9 deletionsiris/program_logic/total_weakestpre.v
- iris/program_logic/weakestpre.v 12 additions, 9 deletionsiris/program_logic/weakestpre.v
- iris_heap_lang/adequacy.v 4 additions, 4 deletionsiris_heap_lang/adequacy.v
- iris_heap_lang/derived_laws.v 2 additions, 2 deletionsiris_heap_lang/derived_laws.v
- iris_heap_lang/lib/array.v 1 addition, 1 deletioniris_heap_lang/lib/array.v
Loading
Please register or sign in to comment