Commits · 03fc47627cfcc20bfddf9d62d6c2de1648976d67 · Iris / ReLoC

May 27, 2020
- update dependencies, fix for lifting rename · 03fc4762
  Ralf Jung authored 4 years ago
  
  03fc4762
May 26, 2020
- Bump Iris (free operation). · 44ca81fd
  Robbert Krebbers authored 4 years ago
  
  44ca81fd
May 25, 2020
- bit of cleanup · a8a8439a
  Dan Frumin authored 4 years ago
  
  a8a8439a
- simplify `tac_rel_load_r` · 9e0d651a
  Dan Frumin authored 4 years ago
  
  9e0d651a
May 24, 2020
- Bump Iris (sbi removal). · b56c7cc7
  Robbert Krebbers authored 4 years ago
  
  b56c7cc7
May 18, 2020
- update gitignore · 25eb1239
  Ralf Jung authored 4 years ago
  
  25eb1239
- update Iris · 15526ec5
  Ralf Jung authored 4 years ago
  
  15526ec5
May 13, 2020
- Use is_stack predicate for the right hand side · aeaaf8b2
  Dan Frumin authored 4 years ago
  
  aeaaf8b2
May 06, 2020
- Ticket lock refinement using HOCAP-style specs · 0e7e1e07
  Dan Frumin authored 4 years ago
  
  0e7e1e07
May 04, 2020
- a tiny clean up · 3c05b1ae
  Dan Frumin authored 4 years ago
  
  3c05b1ae
Apr 29, 2020
- better handling of rel_pure_l/r · 5c942d31
  Dan Frumin authored 4 years ago
  
  5c942d31
- Fix a warning · ac3a3e4d
  Dan Frumin authored 4 years ago
  
  ac3a3e4d
- More work on tp_ tactics · 5d15373a
  Dan Frumin authored 4 years ago
  
  - All tp_ tactics work without explicit modalities in the goal; - All tp_ tactics simplify the ghost thread pool points-to; - Proof term size improvements
  5d15373a
Apr 28, 2020
- fix the tp_ tactics · c32e111d
  Dan Frumin authored 4 years ago
  
  c32e111d
Apr 23, 2020
- Simplify `revoke_offer_l` further · 15dac0c4
  Dan Frumin authored 4 years ago
  
  15dac0c4
Apr 22, 2020
- Cleanup in the stack with helping proof · 26051162
  Dan Frumin authored 4 years ago
  
  26051162
- Make the helping stack proof abstract in the offers specs (almost?) · 753db937
  Dan Frumin authored 4 years ago
  
  753db937
- Simplify the stack with helping refinement. · 6fee530c
  Dan Frumin authored 4 years ago
  
  6fee530c
Apr 21, 2020
- Merge branch 'master' of gitlab.mpi-sws.org:iris/reloc · 64791382
  Dan Frumin authored 4 years ago
  
  64791382
- wk_incr · 15185169
  Dan Frumin authored 4 years ago
  
  15185169
Apr 18, 2020
- update dependencies · a96c4a03
  Ralf Jung authored 4 years ago
  
  a96c4a03
Apr 13, 2020
- Merge branch 'master' of gitlab.mpi-sws.org:iris/reloc · 926738e3
  Dan Frumin authored 4 years ago
  
  926738e3
- a bit of cleanup in bit.v · 900b58ae
  Dan Frumin authored 4 years ago
  
  900b58ae
Apr 09, 2020
- quickfix for _CoqProject · ae8a85e5
  Dan Frumin authored 4 years ago
  
  ae8a85e5
- Bump Iris. · 9487c4c3
  Robbert Krebbers authored 4 years ago
  
  9487c4c3
Apr 05, 2020
- Refinement proof with HOCAP specs. · bb4669b4
  Dan Frumin authored 4 years ago
  
  bb4669b4
- HOCAP specs for the counter · 48090e44
  Dan Frumin authored 4 years ago
  
  48090e44
- Merge commit 'f4619355 ' · ecd44ff2
  Dan Frumin authored 4 years ago
  
  ecd44ff2
- Add typing for values. · 8786f3ef
  Dan Frumin authored 5 years ago
  
  8786f3ef
- Ignore more. · e46427d5
  Robbert Krebbers authored 4 years ago
  
  e46427d5
- Bump Iris. · 42e0d03d
  Robbert Krebbers authored 4 years ago
  
  42e0d03d
Apr 03, 2020
- update dependencies · 232c2cac
  Ralf Jung authored 4 years ago
  
  232c2cac
Mar 16, 2020
- Bump Iris (⊢ changes). · fdb975a5
  Robbert Krebbers authored 5 years ago
  
  fdb975a5
Mar 13, 2020
- Update LICENSE. · 03c65e92
  Robbert Krebbers authored 5 years ago
  
  03c65e92
Mar 06, 2020
- Ordering induced by ⊕ conincides with contextual refinement · f4619355
  Dan Frumin authored 5 years ago
  
  f4619355
- Add FAA to the type system · d698a0c4
  Dan Frumin authored 5 years ago
  
  d698a0c4
Mar 05, 2020
- Add 'unpack' contexts for contextual refinement · cc7a5daf
  Dan Frumin authored 5 years ago
  
  cc7a5daf
- clean up the context typing a bit · 11b432e8
  Dan Frumin authored 5 years ago
  
  11b432e8
Mar 04, 2020
- Add typing for values. · 74a31dc7
  Dan Frumin authored 5 years ago
  
  74a31dc7
Mar 02, 2020
- Generalize `or_choice_1_r`. · aff91eaa
  Dan Frumin authored 5 years ago
  
  aff91eaa