Commits · 50cb1b9dca459760875b85367a951d6a422e70e9 · Yixuan Chen / Iris

Jun 07, 2022
- Merge branch 'functors' into 'master' · 50cb1b9d
  Ralf Jung authored 2 years ago
  
  Add some missing functors in algebra/lib See merge request iris/iris!803
  50cb1b9d
- Add some missing functors in algebra/lib · 4563868c
  Lennard Gäher authored 2 years ago and Ralf Jung committed 2 years ago
  
  4563868c
Jun 03, 2022
- Merge branch 'ralf/tex-heaplang' into 'master' · 7ad5d72c
  Ralf Jung authored 2 years ago
  
  document HeapLang syntax and operational semantics See merge request iris/iris!800
  7ad5d72c
May 25, 2022

Merge branch 'ralf/triples' into 'master' · d46e4472

Ralf Jung authored 2 years ago

fix triple issues with revert, and add logatom triples

See merge request iris/iris!801

d46e4472

May 24, 2022
- Merge branch 'atomic-flip' into 'master' · 5a3fc21a
  Ralf Jung authored 2 years ago
  
  Flip atomic updates quantifiers compared to atomic triples See merge request iris/iris!750
  5a3fc21a
- changelog · 08d1fac0
  Ralf Jung authored 2 years ago
  
  08d1fac0
- Flip quantifiers for atomic updates, and double them up · 5c1b38c5
  Paolo G. Giarrusso authored 3 years ago and Ralf Jung committed 2 years ago
  
  5c1b38c5
May 23, 2022
- add logically atomic triples · f8710e19
  Ralf Jung authored 2 years ago
  
  f8710e19
- Revert "Merge branch 'iris_style_improvements' into 'master'" · b60fbd73
  Ralf Jung authored 2 years ago
  
  This reverts commit bfb57e8b, reversing changes made to 56e9d264. Fixes the problem reported at <iris/iris!797 (comment 81110)>
  b60fbd73
- add a test document for our macros · 3e0fecca
  Ralf Jung authored 2 years ago
  
  3e0fecca
May 21, 2022
- (maybe) better symbol for Ptradd · f9181595
  Ralf Jung authored 2 years ago
  
  f9181595
- remove MatchCore macro, and add sugar for match with binders · 8dc969d0
  Ralf Jung authored 2 years ago
  
  8dc969d0
- add short-circuiting boolean operations · ee8476c4
  Ralf Jung authored 2 years ago
  
  ee8476c4
May 18, 2022
- document HeapLang syntax and operational semantics · 6676a195
  Ralf Jung authored 2 years ago
  
  6676a195
- Merge branch 'iris_style_improvements' into 'master' · bfb57e8b
  Ralf Jung authored 2 years ago
  
  Make Hoare triple tex macro compatible with e.g. array environment See merge request iris/iris!797
  bfb57e8b
May 17, 2022
- cleanup imports · 56e9d264
  Ralf Jung authored 2 years ago
  
  56e9d264
- Merge branch 'paolo/fix-461' into 'master' · 9dd4d1ea
  Ralf Jung authored 2 years ago
  
  Add testcase for #461 See merge request iris/iris!798
  9dd4d1ea
May 16, 2022
- bump std++ properly · 2ce5597c
  Ralf Jung authored 2 years ago
  
  2ce5597c
- bump std++ · 15e60f74
  Ralf Jung authored 2 years ago
  
  15e60f74
- Add testcase for #461 · 9851ef8d
  Paolo G. Giarrusso authored 2 years ago
  
  9851ef8d
- Bump stdpp for universe fix · e60de03f
  Paolo G. Giarrusso authored 2 years ago
  
  e60de03f
- use tc_opaque for a complicated definition · 1b5e1bc6
  Ralf Jung authored 2 years ago
  
  1b5e1bc6
- updates preserve being Absorbing · 15fd682e
  Ralf Jung authored 2 years ago
  
  15fd682e
- Renamed internal macro · c4857c8a
  Jonas Kastberg authored 2 years ago
  
  c4857c8a
- Removed unused angle bracket macro · 006ab914
  Jonas Kastberg authored 2 years ago
  
  006ab914
- use Coq 8.15.1, and enable flambda · ff2b1d90
  Ralf Jung authored 2 years ago
  
  ff2b1d90
May 13, 2022
- update dependencies · de41b20f
  Ralf Jung authored 2 years ago
  
  de41b20f
- Made hoare triple macro compatible with e.g. array environment · 5a0f0a4c
  Jonas Kastberg authored 2 years ago
  
  5a0f0a4c
- Add some line breaks to very long lines. · ab92f91e
  Robbert Krebbers authored 2 years ago
  
  ab92f91e
- Merge branch 'ralf/bi-lemmas' into 'master' · 89f57821
  Robbert Krebbers authored 2 years ago
  
  make affinely_True_emp more useful, and make absorbingly lemmas consistent See merge request iris/iris!796
  89f57821
- changelog · 552a6315
  Ralf Jung authored 2 years ago
  
  552a6315
- make affinely_True_emp more useful, and make absorbingly lemmas consistent · c82fbe0b
  Ralf Jung authored 2 years ago
  
  c82fbe0b
- Merge branch 'robbert/seal' into 'master' · 49f9097f
  Ralf Jung authored 2 years ago
  
  Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`. See merge request iris/iris!793
  49f9097f
- CHANGELOG. · a3534b51
  Robbert Krebbers authored 2 years ago
  
  a3534b51
- No longer make `envs_entails_unseal` local. · 599493de
  Robbert Krebbers authored 2 years ago
  
  599493de
- Make unseal collections `Local`. · 419e96d8
  Robbert Krebbers authored 2 years ago
  
  419e96d8
- Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`. · 088999ea
  Robbert Krebbers authored 2 years ago
  
  Also fix some places where we break the seal.
  088999ea
- Bump std++. · a44ffc04
  Robbert Krebbers authored 2 years ago
  
  a44ffc04
- bring back the verbatim · d080eb82
  Ralf Jung authored 2 years ago
  
  d080eb82
- fix some coqdoc warnings · e706afbf
  Ralf Jung authored 2 years ago
  
  e706afbf