Commits · e17f284e1f4df9e02ee3c1cb997284cfc5e664b6 · Paolo G. Giarrusso / iris

May 03, 2023
- make Prop-level BI connectives notation for bi_emp_valid (rather than bi_entails) · 1014493f
  Ralf Jung authored 2 years ago
  
  1014493f
- add locality annotation to all Typeclasses Opaque/Transparent · 20e5effc
  Ralf Jung authored 1 year ago
  
  20e5effc
Mar 19, 2023
- Tweak new proofs. · 61b66b33
  Robbert Krebbers authored 2 years ago
  
  61b66b33
- Define order predicates on locations. · 729363f2
  Arthur Azevedo de Amorim authored 2 years ago
  
  729363f2
- Add order operations for locations in HeapLang. · 7d0662bf
  Arthur Azevedo de Amorim authored 2 years ago
  
  7d0662bf
Mar 18, 2023
- add some line breaks · d8a491f9
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  d8a491f9
- add 'wp_apply (...) as' · 6900258e
  Ralf Jung authored 2 years ago
  
  6900258e
- Remove useless scope. · ad163b18
  Robbert Krebbers authored 2 years ago
  
  ad163b18
Mar 09, 2023
- Fix uses of `[=?]`, follow up of !893. · 026c3af0
  Robbert Krebbers authored 2 years ago
  
  026c3af0
- Improve iCombine to allow a 'gives' clause for validity properties · 02a46fc6
  Ike Mulder authored 2 years ago and Robbert Krebbers committed 2 years ago
  
  02a46fc6
Feb 15, 2023
- Adapt to https://github.com/coq/coq/pull/16788 · 8fc19c9d
  Pierre Roux authored 2 years ago
  
  8fc19c9d
Feb 14, 2023
- In logatom lock: Formalize that the lock is Free before acquire. · fd02cdaa
  Robbert Krebbers authored 2 years ago
  
  fd02cdaa
Feb 13, 2023

Adam authored 3 years ago

This fixes the fixme introduced in !554.
Coq issue #13654 was fixed by coq pr #14183.

23b4b568

Feb 08, 2023
- Make module for `Loc`. · 360e1cf4
  Robbert Krebbers authored 2 years ago
  
  360e1cf4
Jan 08, 2023
- remove some spurious spaces · a34184ae
  Ralf Jung authored 2 years ago
  
  a34184ae
Dec 04, 2022
- Type annotation in potential ambigious case. · 002cb824
  Robbert Krebbers authored 2 years ago
  
  002cb824
Nov 24, 2022
- Remove tactic `iSolveTC`. · 893f1ab0
  Robbert Krebbers authored 2 years ago
  
  893f1ab0
Sep 06, 2022
- fix typo · a72eb0d7
  Ralf Jung authored 2 years ago
  
  a72eb0d7
Aug 15, 2022
- Tweaks. · 0a297ea2
  Robbert Krebbers authored 2 years ago
  
  0a297ea2
Aug 14, 2022
- add FAA to atomic_heap · 6a2cf566
  Ralf Jung authored 2 years ago
  
  6a2cf566
Aug 12, 2022
- Bump stdpp. · b6ab00a8
  Robbert Krebbers authored 2 years ago
  
  b6ab00a8
Aug 11, 2022
- remove stale reference to Laterable · d5410b27
  Ralf Jung authored 2 years ago
  
  d5410b27
Aug 09, 2022
- use term 'cost' of an instance rather than 'priority' · 2445a4ea
  Ralf Jung authored 2 years ago
  
  2445a4ea
- final tweaks · 88dcbd11
  Robbert Krebbers authored 2 years ago and Ralf Jung committed 2 years ago
  
  88dcbd11
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
- logatom_lock tweaks · fc4b08fe
  Ralf Jung authored 2 years ago
  
  fc4b08fe
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
- 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
Jul 27, 2022
- Add later credits to the WP · c5ebd34d
  Lennard Gäher authored 2 years ago and Robbert Krebbers committed 2 years ago
  
  c5ebd34d
Jul 05, 2022
- First Steps for Later Credits · 7032de0e
  Simon Spies authored 2 years ago and Ralf Jung committed 2 years ago
  
  7032de0e
May 24, 2022
- 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 18, 2022
- document HeapLang syntax and operational semantics · 6676a195
  Ralf Jung authored 2 years ago
  
  6676a195
May 13, 2022
- No longer make `envs_entails_unseal` local. · 599493de
  Robbert Krebbers authored 2 years ago
  
  599493de
- 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