Commits · 1703312614798d4f6d5fc2ee6877339804a2b736 · Pierre Roux / Iris

Dec 09, 2020
- drop support for Coq 8.10 · dda0bf71
  Ralf Jung authored 4 years ago
  
  dda0bf71
Dec 06, 2020
- CHANGELOG. · 2ec2e4d9
  Robbert Krebbers authored 4 years ago
  
  2ec2e4d9
- CHANGELOG. · 54dccc24
  Robbert Krebbers authored 4 years ago
  
  54dccc24
Dec 04, 2020
- add missing changelog entries · e138d2f8
  Ralf Jung authored 4 years ago
  
  e138d2f8
Nov 27, 2020
- forgot to add a changelog entry · f0f9f3b6
  Ralf Jung authored 4 years ago
  
  f0f9f3b6
Nov 12, 2020
- add changelog entry · b397b3ea
  Ralf Jung authored 4 years ago
  
  b397b3ea
Nov 11, 2020
- update docs, also to account for multi-package · 166d4014
  Ralf Jung authored 4 years ago
  
  166d4014
Nov 10, 2020
- Add variant of mapsto_mapsto_ne that does not require further fraction reasoning · 07b3a7db
  Ralf Jung authored 4 years ago
  
  07b3a7db
- one gen_heap_init lemma is enough · 79cd8d45
  Ralf Jung authored 4 years ago
  
  79cd8d45
- changelog, TWP test · 672f4a53
  Ralf Jung authored 4 years ago
  
  672f4a53
- add docs and changelog entry · 0e228686
  Ralf Jung authored 4 years ago
  
  0e228686
Nov 05, 2020
- Strengthen persistent_sep_dup for intuitionistic propositions · 13c5c1ad
  Paolo G. Giarrusso authored 4 years ago and Ralf Jung committed 4 years ago
  
  13c5c1ad
- base_logic and above: use Qp inequality instead of frac validity for lemma statements · 384a4c37
  Ralf Jung authored 4 years ago
  
  384a4c37
- extend changelog explanation · fe2a377e
  Ralf Jung authored 4 years ago
  
  fe2a377e
- CHANGELOG. · 68ec156b
  Robbert Krebbers authored 4 years ago
  
  68ec156b
- algebra: use Qp inequality instead of frac validity for lemma statements · d91853b5
  Ralf Jung authored 4 years ago
  
  d91853b5
Nov 04, 2020
- fix changelog section ordering · 287d6888
  Ralf Jung authored 4 years ago
  
  287d6888
- Revert "Merge branch 'duplicable-type-class' into 'master'" · e8a803c0
  Simon Friis Vindum authored 4 years ago
  
  This reverts commit 71a1fbf0, reversing changes made to ce12f3a6.
  e8a803c0
- split base_logic and bi changelog · f86c08d8
  Ralf Jung authored 4 years ago
  
  f86c08d8
Nov 03, 2020
- more informative changelog · c2f90237
  Ralf Jung authored 4 years ago
  
  c2f90237
- Make mapsto_valid_2 consistent with ghost_var_valid_2 · b41add0e
  Ralf Jung authored 4 years ago
  
  b41add0e
- changelog · 1e029b18
  Ralf Jung authored 4 years ago
  
  1e029b18
- extend changelog · b42f8f52
  Ralf Jung authored 4 years ago
  
  b42f8f52
- Add duplicable type class · 3c625746
  Simon Friis Vindum authored 4 years ago and Robbert Krebbers committed 4 years ago
  
  3c625746
Nov 02, 2020
- CHANGELOG. · 09332c37
  Robbert Krebbers authored 4 years ago
  
  09332c37
Oct 31, 2020
- Fix typos · 291d150c
  Yusuke Matsushita authored 4 years ago and Ralf Jung committed 4 years ago
  
  291d150c
Oct 27, 2020

Add mnat library for monotonic nat ghost state · 28c2e8e3

Tej Chajed authored 4 years ago and

Robbert Krebbers committed 4 years ago

Implemented as an algebra for rules about `auth max_natUR` and a
logic-level wrapper for the auth element (a nat) and fragment (a
persistent lower-bound).

Fixes #327.

28c2e8e3

Oct 20, 2020
- CHANGELOG. · 54fecc1e
  Robbert Krebbers authored 4 years ago
  
  54fecc1e
- changelog · d4441722
  Ralf Jung authored 4 years ago
  
  d4441722
Oct 13, 2020
- rename gen_heap_ctx -> gen_heap_interp, and similar for proph_map_ctx · e31517d5
  Ralf Jung authored 4 years ago
  
  e31517d5
Oct 09, 2020
- changelog entry and some more comments at the top of the file · 4e205a0e
  Ralf Jung authored 4 years ago
  
  4e205a0e
Oct 06, 2020
- CHANGELOG. · 037349bf
  Robbert Krebbers authored 4 years ago
  
  037349bf
Oct 05, 2020
- CHANGELOG. · 741c92b0
  Robbert Krebbers authored 4 years ago
  
  741c92b0
Oct 04, 2020
- CHANGELOG. · 8c7c1ba2
  Robbert Krebbers authored 4 years ago
  
  8c7c1ba2
Oct 03, 2020
- Add dfrac · 7ff11e39
  Simon Friis Vindum authored 4 years ago
  
  7ff11e39
- expand auth changelog · b059329d
  Ralf Jung authored 4 years ago
  
  b059329d
Oct 01, 2020
- CHANGELOG. · 8341b39b
  Robbert Krebbers authored 4 years ago
  
  8341b39b
- CHANGELOG. · 2c2565ac
  Robbert Krebbers authored 4 years ago
  
  2c2565ac
- make adequacy apply to multiple initial threads · 996ec297
  Michael Sammler authored 4 years ago
  
  996ec297
Sep 29, 2020
- changelog for uPred_mono change · 19ba2bc0
  Ralf Jung authored 4 years ago
  
  19ba2bc0