Commits · master · Jonas Kastberg / iris

Jan 11, 2024
- remove some long-dead files · 838322ad
  Ralf Jung authored 1 year ago
  
  838322ad
Dec 26, 2023
- allow testing with Coq 8.20 · 031cb7cb
  Ralf Jung authored 1 year ago
  
  031cb7cb
- iris-bot: support testing against different Coq versions · 0e93d3f3
  Ralf Jung authored 1 year ago
  
  0e93d3f3
Dec 21, 2023
- Merge branch 'later-laws' into 'master' · 5deb8753
  Ralf Jung authored 1 year ago
  
  Refactor proofs of {impl,wand}_timeless See merge request iris/iris!1023
  5deb8753
Dec 18, 2023
- Add comments explaining intricate later shenanigans · 676054d8
  Johannes Hostert authored 1 year ago
  
  676054d8
Dec 15, 2023
- remove trailing space · 658cfd04
  Ralf Jung authored 1 year ago
  
  658cfd04
- Merge branch 'ralf/gmap_view_cmra' into 'master' · 5fbf777b
  Ralf Jung authored 1 year ago
  
  generalize gmap_view for an arbitrary CMRA as values See merge request iris/iris!959
  5fbf777b
Dec 12, 2023
- Merge branch 'master' into 'master' · 87669a66
  Ralf Jung authored 1 year ago
  
  update emacs section in editor.md See merge request iris/iris!1025
  87669a66
- update emacs section in editor.md · d4b7a92d
  Yixuan Chen authored 1 year ago and Ralf Jung committed 1 year ago
  
  d4b7a92d
Dec 10, 2023
- changelog · 0309b526
  Ralf Jung authored 1 year ago
  
  0309b526
- Make gmap_view internal and external lemmas consistent. · 79e3dfc8
  Robbert Krebbers authored 1 year ago and Ralf Jung committed 1 year ago
  
  79e3dfc8
- add gmap_view_both_dfrac_validN_total and use it for gmap_view_both_validI_total · 3fd0224c
  Ralf Jung authored 1 year ago
  
  3fd0224c
- explain why gmap_view_both_dfrac_valid_discrete_total is unidirectional · 2fa22353
  Ralf Jung authored 1 year ago
  
  2fa22353
- clarify gmap_view_rel explanation · e2e7baaa
  Ralf Jung authored 1 year ago
  
  e2e7baaa
- Tweaks. · 48a75b16
  Robbert Krebbers authored 1 year ago and Ralf Jung committed 1 year ago
  
  48a75b16
- port the rest of Iris to the new gmap_view · 4351312a
  Ralf Jung authored 1 year ago
  
  4351312a
- generalize gmap_view for an arbitrary CMRA as values · 4a9e4307
  Ralf Jung authored 1 year ago
  
  4a9e4307
- Merge branch 'ralf/base_redex' into 'master' · 170e430e
  Ralf Jung authored 1 year ago
  
  fix forgotten rename: head_redex -> base_redex See merge request iris/iris!1024
  170e430e
Dec 09, 2023
- changelog · 8ca7b735
  Ralf Jung authored 1 year ago
  
  8ca7b735
- fix forgotten renames: head_redex -> base_redex, head_atomic -> base_atomic · 25dc2bc8
  Ralf Jung authored 1 year ago
  
  25dc2bc8
Dec 02, 2023
- Refactor proofs of {impl,wand}_timeless · 7af01091
  Johannes Hostert authored 1 year ago
  
  7af01091
- Space. · 6a0d62a5
  Robbert Krebbers authored 1 year ago
  
  6a0d62a5
Nov 20, 2023
- also exclude Coq 8.20 from testing · 7d72ccb5
  Ralf Jung authored 1 year ago
  
  7d72ccb5
- Merge branch 'steps-lb-init' into 'master' · 0e4bd033
  Ralf Jung authored 1 year ago
  
  Generalize wp_lb_init to steps_lb_0. See merge request iris/iris!1022
  0e4bd033
- Generalize wp_lb_init to steps_lb_0. · c5a6de6a
  tlsomers authored 1 year ago and Ralf Jung committed 1 year ago
  
  c5a6de6a
Nov 17, 2023
- update dependencies · e29d4cf8
  Ralf Jung authored 1 year ago
  
  e29d4cf8
Nov 14, 2023
- Merge branch 'egrep' into 'master' · 781fc232
  Ralf Jung authored 1 year ago
  
  egrep -> grep -E See merge request iris/iris!1019
  781fc232
- egrep -> grep -E · b9bcdb90
  Johannes Hostert authored 1 year ago
  
  b9bcdb90
Nov 11, 2023
- Merge branch 'undiscard-laws' into 'master' · f72d3ac9
  Ralf Jung authored 1 year ago
  
  Add laws to allow "undiscarding" points-tos See merge request iris/iris!960
  f72d3ac9
- Merge branch 'robbert/total_adequacy_later' into 'master' · 25593372
  Ralf Jung authored 1 year ago
  
  Remove needless later in total adequacy. See merge request iris/iris!1018
  25593372
- Remove needless later in total adequacy. · 4d1b044f
  Robbert Krebbers authored 1 year ago
  
  4d1b044f
Nov 10, 2023
- Add CHANGELOG for un-persisting laws · 8922f16f
  Johannes Hostert authored 1 year ago
  
  8922f16f
- Make dyn_reservation_map follow style for updateP · e40374b8
  Johannes Hostert authored 1 year ago
  
  e40374b8
- Add separation logic unpersist update laws · 0a7d4889
  Johannes Hostert authored 1 year ago
  
  0a7d4889
- Add unpersist law for gmap_view fragments · 7f663519
  Johannes Hostert authored 1 year ago
  
  7f663519
- Add unpersist laws for authorative parts of frag · 3bc1e3cc
  Johannes Hostert authored 1 year ago
  
  3bc1e3cc
- Add general/missing lemmas about updateP · 443cd600
  Johannes Hostert authored 1 year ago
  
  443cd600
- Add law for undiscarding dfracs · 14029845
  Johannes Hostert authored 1 year ago
  
  14029845
Nov 06, 2023
- fix typo in changelog · 35f38b59
  Ralf Jung authored 1 year ago
  
  35f38b59
- Merge branch 'ralf/base_step' into 'master' · 4cfd3db8
  Ralf Jung authored 1 year ago
  
  rename head_step → base_step See merge request !1012
  4cfd3db8