Commits · 2f26293564a91c832ea766fb8582a3ada42c6f3f · William Mansky / Iris

Mar 24, 2021
- use the new pattern features in a few places to shorten proofs a bit · fe2b525c
  Ralf Jung authored 4 years ago
  
  fe2b525c
Jan 17, 2021
- Change `wp_apply` so it no longer performs `wp_pures`, and add new tactic `wp_smart_apply` · a361b173
  Robbert Krebbers authored 4 years ago
  
  that performs `wp_pure` in small steps until the lemma matches the goal.
  a361b173
Jan 07, 2021
- also add Local/Global to Arguments · 79a11082
  Ralf Jung authored 4 years ago
  
  79a11082
- Qualify all instances with Local or Global · 143d0af3
  Ralf Jung authored 4 years ago
  
  Done with a script by Tej; see iris/iris!609 for details.
  143d0af3
Dec 18, 2020
- Add some FIXMES. · c74d8afd
  Robbert Krebbers authored 4 years ago
  
  c74d8afd
- Inline dfrac notations to work around https://github.com/coq/coq/issues/13654 · f6df2576
  Robbert Krebbers authored 4 years ago
  
  f6df2576
Dec 16, 2020
- Add `mapsto_persist` to `atomic_heap`. · 7499c0fa
  Robbert Krebbers authored 4 years ago
  
  7499c0fa
- Apply 3 suggestion(s) to 3 file(s) · 5d81fe7a
  Simon Friis Vindum authored 4 years ago
  
  5d81fe7a
- Fix various things · faba7343
  Simon Friis Vindum authored 4 years ago
  
  faba7343
- Generalize lemmas, use custom scope · 17033126
  Simon Friis Vindum authored 4 years ago
  
  17033126
- Add persistent points-to predicate · b57aac09
  Simon Friis Vindum authored 4 years ago
  
  b57aac09
Nov 26, 2020
- wp_fupd is now unnecessary in these proofs · 9120035b
  Ralf Jung authored 4 years ago
  
  9120035b
- wp_finish: avoid making a goal unprovable · 7b19365c
  Ralf Jung authored 4 years ago
  
  7b19365c
Nov 11, 2020
- multi-package repositories · 2ab9e4a2
  Ralf Jung authored 4 years ago
  
  2ab9e4a2