Merge branch 'iris-later-credits' into 'master'
First Steps for Later Credits See merge request iris/iris!792
Showing
- CHANGELOG.md 38 additions, 0 deletionsCHANGELOG.md
- _CoqProject 1 addition, 0 deletions_CoqProject
- iris/base_logic/lib/fancy_updates.v 156 additions, 18 deletionsiris/base_logic/lib/fancy_updates.v
- iris/base_logic/lib/invariants.v 1 addition, 0 deletionsiris/base_logic/lib/invariants.v
- iris/base_logic/lib/later_credits.v 423 additions, 0 deletionsiris/base_logic/lib/later_credits.v
- iris/base_logic/lib/wsat.v 20 additions, 20 deletionsiris/base_logic/lib/wsat.v
- iris/bi/derived_laws.v 18 additions, 0 deletionsiris/bi/derived_laws.v
- iris/program_logic/adequacy.v 112 additions, 37 deletionsiris/program_logic/adequacy.v
- iris/program_logic/ownp.v 6 additions, 6 deletionsiris/program_logic/ownp.v
- iris/program_logic/total_adequacy.v 4 additions, 4 deletionsiris/program_logic/total_adequacy.v
- iris_heap_lang/adequacy.v 4 additions, 4 deletionsiris_heap_lang/adequacy.v
- iris_heap_lang/total_adequacy.v 2 additions, 2 deletionsiris_heap_lang/total_adequacy.v
- tests/heap_lang.v 1 addition, 1 deletiontests/heap_lang.v
- tests/one_shot.v 1 addition, 1 deletiontests/one_shot.v
- tests/one_shot_once.v 1 addition, 1 deletiontests/one_shot_once.v
- tex/extended-logic.tex 1 addition, 0 deletionstex/extended-logic.tex
- tex/iris.sty 14 additions, 1 deletiontex/iris.sty
- tex/program-logic.tex 112 additions, 8 deletionstex/program-logic.tex
Loading
Please register or sign in to comment