Merge branch 'ci/ralf/dealloc' into 'master'
heap_lang: support deallocation Closes #313 See merge request iris/iris!439
Showing
- CHANGELOG.md 2 additions, 1 deletionCHANGELOG.md
- _CoqProject 1 addition, 1 deletion_CoqProject
- tests/heap_lang.ref 9 additions, 0 deletionstests/heap_lang.ref
- tests/heap_lang.v 22 additions, 2 deletionstests/heap_lang.v
- theories/base_logic/lib/gen_inv_heap.v 4 additions, 5 deletionstheories/base_logic/lib/gen_inv_heap.v
- theories/heap_lang/adequacy.v 4 additions, 4 deletionstheories/heap_lang/adequacy.v
- theories/heap_lang/lang.v 62 additions, 39 deletionstheories/heap_lang/lang.v
- theories/heap_lang/lib/array.v 35 additions, 7 deletionstheories/heap_lang/lib/array.v
- theories/heap_lang/lib/atomic_heap.v 13 additions, 1 deletiontheories/heap_lang/lib/atomic_heap.v
- theories/heap_lang/lifting.v 121 additions, 13 deletionstheories/heap_lang/lifting.v
- theories/heap_lang/metatheory.v 10 additions, 7 deletionstheories/heap_lang/metatheory.v
- theories/heap_lang/proofmode.v 50 additions, 0 deletionstheories/heap_lang/proofmode.v
- theories/heap_lang/proph_erasure.v 58 additions, 32 deletionstheories/heap_lang/proph_erasure.v
- theories/heap_lang/tactics.v 1 addition, 0 deletionstheories/heap_lang/tactics.v
- theories/heap_lang/total_adequacy.v 1 addition, 1 deletiontheories/heap_lang/total_adequacy.v
Loading
Please register or sign in to comment