Commits · 89c539efe305e0f109b4c612abcbda9daa7bbeea · Paolo G. Giarrusso / iris

Apr 29, 2021
- Fix typo in the comments. · 89c539ef
  Dan Frumin authored 3 years ago
  
  89c539ef
Apr 22, 2021
- Merge branch 'ralf/doc-mask-mismatch' into 'master' · 35e8d8d7
  Ralf Jung authored 3 years ago
  
  add some guidance on how to handle mask mismatches See merge request iris/iris!669
  35e8d8d7
- Apply 3 suggestion(s) to 1 file(s) · 2f262935
  Ralf Jung authored 3 years ago
  
  2f262935
- bump Coq version we test to 8.13.2 · dea10729
  Ralf Jung authored 3 years ago
  
  dea10729
- add some guidance on how to handle mask mismatches · 05f77071
  Ralf Jung authored 3 years ago
  
  05f77071
Apr 20, 2021
- Bump std++ (multiset singleton). · 7a260d80
  Robbert Krebbers authored 3 years ago
  
  7a260d80
Apr 19, 2021
- Merge branch 'gset_bij_lem' into 'master' · 823d3357
  Ralf Jung authored 3 years ago
  
  base_logic/lib/gset_bij: fix gset_bij_own_elem_agree; add gset_bij_own_elem_auth_agree See merge request iris/iris!663
  823d3357
- change name to gset_bij_elem_of · 58e8818d
  Lennard Gäher authored 3 years ago
  
  58e8818d
- invariant paradox: use fupd notation and fix formatting · 9e4493f9
  Ralf Jung authored 3 years ago
  
  9e4493f9
Apr 15, 2021
- Add lemma `map_seq_ne`. · 2927fef1
  Robbert Krebbers authored 3 years ago
  
  2927fef1
Apr 14, 2021
- Merge branch 'fix-string-ident-clear' into 'master' · b3896878
  Ralf Jung authored 3 years ago
  
  Fix string_to_ident when ident is not fresh See merge request iris/iris!667
  b3896878
- Fix string_to_ident when ident is not fresh · 20d74b17
  Tej Chajed authored 3 years ago and Ralf Jung committed 3 years ago
  
  20d74b17
- Merge branch 'hai/iff_sym' into 'master' · f4fbb6c0
  Robbert Krebbers authored 3 years ago
  
  Add more lemmas for wand_iff and iff See merge request iris/iris!666
  f4fbb6c0
- Add more lemmas for wand_iff and iff · eeb87782
  Hai Dang authored 3 years ago and Robbert Krebbers committed 3 years ago
  
  eeb87782
- Merge branch 'hai/frac_agree_included' into 'master' · d2bd3117
  Robbert Krebbers authored 3 years ago
  
  Add included lemmas for frac_agree See merge request iris/iris!665
  d2bd3117
Apr 13, 2021
- Strengthen frac_agree_included to equivalence · 47a0bd1f
  Hai Dang authored 3 years ago
  
  47a0bd1f
- Add included lemmas for frac_agree · a9f6c350
  Hai Dang authored 3 years ago
  
  a9f6c350
Apr 12, 2021
- Merge branch 'ci/ralf/name-mangle-string-to-ident' into 'master' · cba13ce5
  Ralf Jung authored 3 years ago
  
  different approach for string_to_ident that works with name mangling Closes #343 See merge request iris/iris!660
  cba13ce5
- add back a version of string_to_ident · 57e813e6
  Ralf Jung authored 3 years ago
  
  57e813e6
- note that things will be better in the future · 4d39284d
  Ralf Jung authored 3 years ago
  
  4d39284d
Apr 11, 2021
- Merge branch 'view-coreid' into 'master' · 01d4289b
  Ralf Jung authored 3 years ago
  
  Add CoreId instances for auth and view See merge request iris/iris!664
  01d4289b
- Add CoreId instances for auth and view · 346ca437
  Simon Friis Vindum authored 3 years ago
  
  346ca437
Apr 08, 2021
- update dependencies · 95637901
  Ralf Jung authored 3 years ago
  
  95637901
- change name · 5941b28a
  Lennard Gäher authored 3 years ago
  
  5941b28a
- fix bij_own_elem_agree; add bij_own_elem_auth_agree · 8ab2971e
  Lennard Gäher authored 3 years ago
  
  8ab2971e
Mar 27, 2021
- Merge branch 'ralf/coq-8.11' into 'master' · f1484b2b
  Ralf Jung authored 4 years ago
  
  drop support for Coq 8.11 See merge request iris/iris!657
  f1484b2b
- remove now stale .ref files · 6415d82a
  Ralf Jung authored 4 years ago
  
  6415d82a
- drop support for Coq 8.11 · a092506c
  Ralf Jung authored 4 years ago
  
  a092506c
Mar 25, 2021
- add test for dependent nested exist · 0e7930c6
  Ralf Jung authored 4 years ago
  
  0e7930c6
Mar 24, 2021
- Merge branch 'ralf/into-and-sep' into 'master' · 7ccdfe0d
  Robbert Krebbers authored 4 years ago
  
  fix IntoAnd/IntoSep docs See merge request iris/iris!659
  7ccdfe0d
- fix IntoAnd/IntoSep docs · 473087eb
  Ralf Jung authored 4 years ago
  
  473087eb
- different approach for string_to_ident that works with name mangling · 2eb8bde0
  Ralf Jung authored 4 years ago
  
  2eb8bde0
- disable name mangling test for now, it is incompatible with using the string_ident feature · 5e5446b0
  Ralf Jung authored 4 years ago
  
  5e5446b0
- use the new pattern features in a few places to shorten proofs a bit · fe2b525c
  Ralf Jung authored 4 years ago
  
  fe2b525c
- Merge branch 'ci/ralf/exists-intro-pattern' into 'master' · 93ae382f
  Ralf Jung authored 4 years ago
  
  Support destructing exists with intro patterns Closes #310 See merge request iris/iris!658
  93ae382f
- improve comments · b861419a
  Ralf Jung authored 4 years ago
  
  b861419a
- Move old note in proof mode docs. · bb9201b5
  Robbert Krebbers authored 4 years ago
  
  This note is obsolete due to iris/iris!640
  bb9201b5
- generalize into_and_sep_affine so that generalizing just the conjunction... · f531cc9d
  Ralf Jung authored 4 years ago
  
  generalize into_and_sep_affine so that generalizing just the conjunction instance for IntoExist is sufficient
  f531cc9d
- add more tests · 7da8952e
  Ralf Jung authored 4 years ago
  
  7da8952e
- extend proof_mode.md · 260e0593
  Ralf Jung authored 4 years ago
  
  260e0593