Commits · fa7af0140689110589ad78c84c9d5dadc95f146c · Pierre Roux / Iris

Aug 09, 2022
- CHANGELOG. · fa7af014
  Robbert Krebbers authored 2 years ago
  
  fa7af014
- Rename `laterN_plus` into `laterN_add`. · e5905932
  Robbert Krebbers authored 2 years ago
  
  e5905932
- Merge branch 'cost' into 'master' · 55e78d6f
  Robbert Krebbers authored 2 years ago
  
  use term 'cost' of an instance rather than 'priority' See merge request iris/iris!833
  55e78d6f
- use term 'cost' of an instance rather than 'priority' · 2445a4ea
  Ralf Jung authored 2 years ago
  
  2445a4ea
- Merge branch 'lc-heaplang' into 'master' · 4e9a1ec7
  Ralf Jung authored 2 years ago
  
  Basic later credits implementation for HeapLang See merge request iris/iris!823
  4e9a1ec7
- final tweaks · 88dcbd11
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  88dcbd11
Aug 08, 2022
- Merge branch 'view-both-core' into 'master' · c069ee33
  Ralf Jung authored 2 years ago
  
  add lemmas for core of auth⋅frag in view and auth See merge request iris/iris!832
  c069ee33
- use notation · 70c2e721
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  70c2e721
- Merge branch 'mono' into 'master' · 7330d7e4
  Ralf Jung authored 2 years ago
  
  add some missing IsOp instances and remove accidental instance for mono_nat and mono_list See merge request iris/iris!828
  7330d7e4
- Avoid really long line · 4058f67d
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  4058f67d
- more space · f1cefaac
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  f1cefaac
Aug 05, 2022
- Merge branch 'mono_list_auth_core_id' into 'master' · f20bc050
  Ralf Jung authored 2 years ago
  
  add mono_list_auth_core_id, mono_nat_auth_core_id See merge request iris/iris!827
  f20bc050
- fix some leftover uses of 'staging' · 2d565928
  Ralf Jung authored 2 years ago
  
  2d565928
- add lemmas for core of auth⋅frag in view and auth · c93f40ad
  Ralf Jung authored 2 years ago
  
  c93f40ad
- add mono_list_auth_core_id, mono_nat_auth_core_id · 3c7353c7
  Ralf Jung authored 2 years ago
  
  3c7353c7
- Merge branch 'msammler/update-stdpp' into 'master' · f89a452d
  Michael Sammler authored 2 years ago
  
  update std++ See merge request iris/iris!831
  f89a452d
- update stdpp · 6478a4ae
  Michael Sammler authored 2 years ago
  
  6478a4ae
Aug 04, 2022
- update documentation and make it match reality · 01abd043
  Ralf Jung authored 2 years ago
  
  01abd043
- for now, only prodice a simple one-credit-per-step tactic · 574bc789
  Ralf Jung authored 2 years ago
  
  574bc789
- fix: make tactic work for steps_lb in intuit context · 7e4c7a3e
  Lennard Gäher authored 2 years ago and Ralf Jung committed 2 years ago
  
  7e4c7a3e
- tactics · c4e7da60
  Lennard Gäher authored 2 years ago and Ralf Jung committed 2 years ago
  
  c4e7da60
- basic heaplang implementation · 2b1b2c89
  Lennard Gäher authored 2 years ago and Ralf Jung committed 2 years ago
  
  2b1b2c89
- Merge branch 'unstable' into 'master' · 9a491ba6
  Ralf Jung authored 2 years ago
  
  rename staging to unstable See merge request !826
  9a491ba6
- add some missing IsOp instances and remove accidental instance for mono_nat and mono_list · 77d3a42e
  Ralf Jung authored 2 years ago
  
  77d3a42e
- Merge branch 'logatom_lock' into 'master' · 51da9c32
  Ralf Jung authored 2 years ago
  
  logatom_lock tweaks See merge request !829
  51da9c32
- logatom_lock tweaks · fc4b08fe
  Ralf Jung authored 2 years ago
  
  fc4b08fe
- rename staging to unstable · d9360cde
  Ralf Jung authored 2 years ago
  
  d9360cde
Aug 03, 2022
- make tada_lock_state exclusive · 75c9df64
  Ralf Jung authored 2 years ago
  
  75c9df64
- add proof that TaDA-style lock can be derived from standard CAP-style lock · c9169b9d
  Ralf Jung authored 2 years ago
  
  c9169b9d
- Merge branch 'has-lc' into 'master' · 949ab7bc
  Ralf Jung authored 2 years ago
  
  track has_lc directly in invGS/irisGS/heapGS rather than via separate typeclass See merge request !816
  949ab7bc
- changelog · 3c16b4eb
  Ralf Jung authored 2 years ago
  
  3c16b4eb
- make some more heap_lang libs lc-generic; tweak atomic_heap handling · c194161b
  Ralf Jung authored 2 years ago
  
  c194161b
Aug 02, 2022
- track has_lc directly in invGS/irisGS/heapGS rather than via separate typeclass · 4f0e06eb
  Ralf Jung authored 2 years ago
  
  4f0e06eb
Aug 01, 2022
- Merge branch 'NiklasM-master-patch-11610' into 'master' · 537d052b
  Ralf Jung authored 2 years ago
  
  [Docs] Add "Fira Code Retina" instructions for Linux See merge request iris/iris!824
  537d052b
Jul 30, 2022
- Add "Fira Code Retina" instructions for Linux · 07de39c9
  Niklas Mück authored 2 years ago
  
  see https://github.com/tonsky/FiraCode/wiki/VS-Code-Instructions
  07de39c9
Jul 27, 2022
- Merge branch 'fix-proof-coq-master' into 'master' · 753562b6
  Robbert Krebbers authored 2 years ago
  
  Fix a proof broken on Coq master See merge request !822
  753562b6
- Fix a proof broken on Coq master · b357a22c
  Tej Chajed authored 2 years ago
  
  Unverified
  
  b357a22c
- Put space after £ to ease parsing. · 7211cd79
  Robbert Krebbers authored 2 years ago
  
  7211cd79
- Bump std++. · d01b4bc8
  Robbert Krebbers authored 2 years ago
  
  d01b4bc8
- Merge branch 'lc-weakestpre' into 'master' · 52a4e096
  Robbert Krebbers authored 2 years ago
  
  Add later credits to the WP See merge request !808
  52a4e096