Merge branch 'robbert/open_scope_Z' into 'master'
Remove `Open Scope Z_scope` in HeapLang See merge request iris/iris!453
No related branches found
No related tags found
Showing
- CHANGELOG.md 2 additions, 0 deletionsCHANGELOG.md
- tests/heap_lang.ref 1 addition, 1 deletiontests/heap_lang.ref
- tests/heap_lang.v 11 additions, 9 deletionstests/heap_lang.v
- tests/ipm_paper.v 4 additions, 4 deletionstests/ipm_paper.v
- tests/tree_sum.v 1 addition, 1 deletiontests/tree_sum.v
- theories/heap_lang/derived_laws.v 5 additions, 5 deletionstheories/heap_lang/derived_laws.v
- theories/heap_lang/lang.v 8 additions, 9 deletionstheories/heap_lang/lang.v
- theories/heap_lang/lib/array.v 2 additions, 2 deletionstheories/heap_lang/lib/array.v
- theories/heap_lang/lib/counter.v 5 additions, 5 deletionstheories/heap_lang/lib/counter.v
- theories/heap_lang/lib/ticket_lock.v 2 additions, 2 deletionstheories/heap_lang/lib/ticket_lock.v
- theories/heap_lang/metatheory.v 2 additions, 2 deletionstheories/heap_lang/metatheory.v
- theories/heap_lang/primitive_laws.v 2 additions, 2 deletionstheories/heap_lang/primitive_laws.v
- theories/heap_lang/proofmode.v 4 additions, 4 deletionstheories/heap_lang/proofmode.v
- theories/heap_lang/proph_erasure.v 6 additions, 6 deletionstheories/heap_lang/proph_erasure.v
Loading
Please register or sign in to comment