Commits · 0da37f400b47ff58f8b57003aed398f6d4a2eb41 · Paolo G. Giarrusso / iris

Jul 24, 2024
- Merge branch 'typos' into 'master' · 0da37f40
  Ralf Jung authored 8 months ago
  
  docs: typo fixes See merge request iris/iris!1059
  0da37f40
Jul 23, 2024
- docs: typo fixes · dcaaeae1
  Sanjit Bhat authored 8 months ago
  
  Verified
  
  dcaaeae1
Jul 22, 2024
- update dependencies · d955d6af
  Ralf Jung authored 8 months ago
  
  d955d6af
Jul 19, 2024
- Merge branch 'gset_to_gmap_theory' into 'master' · 426f2d2e
  Ralf Jung authored 8 months ago
  
  Add lemmas for big_opS and gmap singletons See merge request iris/iris!1049
  426f2d2e
Jul 15, 2024
- Tweak CHANGELOG. · b9f8d4bd
  Robbert Krebbers authored 8 months ago
  
  b9f8d4bd
Jul 02, 2024
- Add CHANGELOG entry for big op gset_to_gmap lemma · 34b628e6
  Isaac van Bakel authored 8 months ago
  
  Verified
  
  34b628e6
- Merge branch 'master' into gset_to_gmap_theory · a32469f5
  Isaac van Bakel authored 8 months ago
  
  Verified
  
  a32469f5
- Merge branch 'robbert/iInduction_wand' into 'master' · 6cb68cdf
  Robbert Krebbers authored 8 months ago
  
  Always use magic wand in `iInduction` hypothesis See merge request iris/iris!1048
  6cb68cdf
- Tweak CHANGELOG. · b4f0c8ef
  Ralf Jung authored 8 months ago and Robbert Krebbers committed 8 months ago
  
  b4f0c8ef
- CHANGELOG. · acf66b74
  Robbert Krebbers authored 10 months ago
  
  acf66b74
- Tests. · f694cf77
  Robbert Krebbers authored 10 months ago
  
  f694cf77
- Similar to `IntoIH` and `IntoWand` instances, let `tac_pure_revert` use `MakeAffinely`. · 76a18ce3
  Robbert Krebbers authored 10 months ago
  
  76a18ce3
- Let `into_ih_impl` generate -∗ instead of →. · 06f67042
  Robbert Krebbers authored 10 months ago
  
  06f67042
- Merge branch 'ralf/wp_cmpxchg_fail-persist' into 'master' · 7f856b61
  Ralf Jung authored 8 months ago
  
  fix wp_cmpxchg_fail when points-to is in persistent context Closes #570 See merge request iris/iris!1057
  7f856b61
- coqdoc, changelog · b3e73b39
  Robbert Krebbers authored 8 months ago and Ralf Jung committed 8 months ago
  
  b3e73b39
- Merge branch 'yusuke/big_sepX_flip_mono' into 'master' · f8546a91
  Robbert Krebbers authored 8 months ago
  
  Add big_sep*_flip_mono' See merge request iris/iris!1053
  f8546a91
- Add big_sep*_flip_mono' · e2118410
  Yusuke Matsushita authored 8 months ago and Robbert Krebbers committed 8 months ago
  
  e2118410
- Tweak proof. · 1c0a4f4b
  Robbert Krebbers authored 8 months ago
  
  1c0a4f4b
Jul 01, 2024
- fix wp_cmpxchg_fail when points-to is in persistent context · e46e1b7d
  Ralf Jung authored 8 months ago
  
  e46e1b7d
Jun 19, 2024
- update dependencies · 3d7c7fd5
  Ralf Jung authored 9 months ago
  
  3d7c7fd5
- Merge branch 'rodolphe/dune' into 'master' · 47000dbc
  Ralf Jung authored 9 months ago
  
  Allow compiling the packages with dune. See merge request iris/iris!1056
  47000dbc
- Allow compiling the packages with dune. · f1313bda
  Rodolphe Lepigre authored 9 months ago
  
  f1313bda
- Merge branch 'robbert/iInv_error' into 'master' · 3818b339
  Ralf Jung authored 9 months ago
  
  More suggestive error message for `iInv`. See merge request iris/iris!1055
  3818b339
- CHANGELOG. · d0410021
  Robbert Krebbers authored 9 months ago
  
  d0410021
- More suggestive error message for `iInv`. · caf5ae2a
  Robbert Krebbers authored 9 months ago
  
  caf5ae2a
- Merge branch 'robbert/remove_star_spec_pattern' into 'master' · a14be4c1
  Robbert Krebbers authored 9 months ago
  
  Remove the `*` specialization pattern. See merge request iris/iris!1054
  a14be4c1
- Remove the `*` specialization pattern. This pattern has been deprecated and a... · df6ae78b
  Robbert Krebbers authored 9 months ago
  
  Remove the `*` specialization pattern. This pattern has been deprecated and a no-op since 2017. See !41.
  df6ae78b
Jun 10, 2024
- Merge branch 'robbert/issue_571' into 'master' · 84ed8993
  Ralf Jung authored 9 months ago
  
  Bump timeout to hopefully solve #571. Closes #571 See merge request iris/iris!1051
  84ed8993
Jun 09, 2024
- Bump timeout to hopefully solve !571. · a26d9ee5
  Robbert Krebbers authored 9 months ago
  
  a26d9ee5
Jun 04, 2024
- add Coq 8.21 to NOREF · 25cc104d
  Ralf Jung authored 9 months ago
  
  25cc104d
- update dependencies · 3ecd3e95
  Ralf Jung authored 9 months ago
  
  3ecd3e95
May 29, 2024
- update dependencies · 6aaddc70
  Ralf Jung authored 9 months ago
  
  6aaddc70
May 28, 2024

Add lemmas for big_opS and gmap singletons · 42b75ebf

Isaac van Bakel authored 9 months ago

This is a particular pattern that comes up in the lifetime logic which I
want to be able to rewrite, which is why I've extracted it to a general
lemma.

Verified

42b75ebf

Apr 19, 2024
- update dependencies · 5ae02407
  Ralf Jung authored 11 months ago
  
  5ae02407
- Merge branch 'fix-doc-links' into 'master' · a2e43250
  Ralf Jung authored 11 months ago
  
  Fix broken code links in docs See merge request iris/iris!1047
  a2e43250
- Fix broken code links in docs · c727bce5
  Tej Chajed authored 11 months ago
  
  Unverified
  
  c727bce5
Apr 16, 2024
- bump std++ · f2800611
  Ralf Jung authored 11 months ago
  
  f2800611
- exclude Coq 8.20 from printing tests · 8c11e613
  Ralf Jung authored 11 months ago
  
  8c11e613
Apr 15, 2024
- Merge branch 'feat-na-own-empty' into 'master' · 9dbbb15f
  Robbert Krebbers authored 11 months ago
  
  add lemmas for na_own p ∅ See merge request iris/iris!1044
  9dbbb15f
- add lemmas for na_own p ∅ · 9926920d
  Benjamin Peters authored 11 months ago
  
  9926920d