Commits · master · Iris / Iris

11 May, 2021 6 commits
- Merge branch 'ralf/wp_frame_wand' into 'master' · 98b90f13
  Ralf Jung authored May 11, 2021
```
add wp_frame_wand lemma

See merge request !672
```
  98b90f13
- add twp_frame_wand · 771b9aed
  Ralf Jung authored May 11, 2021
  
  771b9aed
- changelog · 4ffdfc18
  Ralf Jung authored May 11, 2021
  
  4ffdfc18
- use wp_frame_wand in awp_apply; get rid of _l/_r variants · 5b43a080
  Ralf Jung authored May 11, 2021
  
  5b43a080
- use wp_frame_wand where suitable · 7ee261cf
  Ralf Jung authored May 03, 2021
  
  7ee261cf
- add wp_frame_wand lemma · 09835135
  Ralf Jung authored May 02, 2021
  
  09835135
09 May, 2021 1 commit
- fix typo (thanks Paolo) · 4a59814e
  Ralf Jung authored May 09, 2021
  
  4a59814e
07 May, 2021 3 commits
- further extend comment · 141a635e
  Ralf Jung authored May 07, 2021
  
  141a635e
- extend logical atomicity comments · d7b84ad4
  Ralf Jung authored May 07, 2021
  
  d7b84ad4
- improve 'unqualified' error message · 5119ab8b
  Ralf Jung authored May 07, 2021
  
  5119ab8b
05 May, 2021 1 commit
- update dependencies · 6f18e8cd
  Ralf Jung authored May 05, 2021
  
  6f18e8cd
02 May, 2021 1 commit
- re-enable coq.dev CI · 6a1f68dc
  Ralf Jung authored May 02, 2021
  
  6a1f68dc
30 Apr, 2021 1 commit
- update std++ · 70f0dde7
  Ralf Jung authored Apr 30, 2021
  
  70f0dde7
29 Apr, 2021 3 commits
- disable Coq master test while Coq master is broken · aa13172e
  Ralf Jung authored Apr 29, 2021
  
  aa13172e
- Merge branch 'dfrumin-master-patch-71378' into 'master' · c8352453
  Ralf Jung authored Apr 29, 2021
```
Fix typo in the comments.

See merge request !670
```
  c8352453
- Fix typo in the comments. · 89c539ef
  Dan Frumin authored Apr 29, 2021
  
  89c539ef
22 Apr, 2021 4 commits
- Merge branch 'ralf/doc-mask-mismatch' into 'master' · 35e8d8d7
  Ralf Jung authored Apr 22, 2021
```
add some guidance on how to handle mask mismatches

See merge request !669
```
  35e8d8d7
- Apply 3 suggestion(s) to 1 file(s) · 2f262935
  Ralf Jung authored Apr 22, 2021
  
  2f262935
- bump Coq version we test to 8.13.2 · dea10729
  Ralf Jung authored Apr 22, 2021
  
  dea10729
- add some guidance on how to handle mask mismatches · 05f77071
  Ralf Jung authored Apr 22, 2021
  
  05f77071
20 Apr, 2021 1 commit
- Bump std++ (multiset singleton). · 7a260d80
  Robbert Krebbers authored Apr 20, 2021
  
  7a260d80
19 Apr, 2021 3 commits
- Merge branch 'gset_bij_lem' into 'master' · 823d3357
  Ralf Jung authored Apr 19, 2021
```
base_logic/lib/gset_bij: fix gset_bij_own_elem_agree; add gset_bij_own_elem_auth_agree

See merge request !663
```
  823d3357
- change name to gset_bij_elem_of · 58e8818d
  Lennard Gäher authored Apr 19, 2021
  
  58e8818d
- invariant paradox: use fupd notation and fix formatting · 9e4493f9
  Ralf Jung authored Apr 19, 2021
  
  9e4493f9
15 Apr, 2021 1 commit
- Add lemma `map_seq_ne`. · 2927fef1
  Robbert Krebbers authored Apr 15, 2021
  
  2927fef1
14 Apr, 2021 5 commits
- Merge branch 'fix-string-ident-clear' into 'master' · b3896878
  Ralf Jung authored Apr 14, 2021
```
Fix string_to_ident when ident is not fresh

See merge request !667
```
  b3896878
- Fix string_to_ident when ident is not fresh · 20d74b17
  Tej Chajed authored Apr 14, 2021
  
  20d74b17
- Merge branch 'hai/iff_sym' into 'master' · f4fbb6c0
  Robbert Krebbers authored Apr 14, 2021
```
Add more lemmas for wand_iff and iff

See merge request !666
```
  f4fbb6c0
- Add more lemmas for wand_iff and iff · eeb87782
  Hai Dang authored Apr 14, 2021
  
  eeb87782
- Merge branch 'hai/frac_agree_included' into 'master' · d2bd3117
  Robbert Krebbers authored Apr 14, 2021
```
Add included lemmas for frac_agree

See merge request !665
```
  d2bd3117
13 Apr, 2021 2 commits
- Strengthen frac_agree_included to equivalence · 47a0bd1f
  Hai Dang authored Apr 13, 2021
  
  47a0bd1f
- Add included lemmas for frac_agree · a9f6c350
  Hai Dang authored Apr 13, 2021
  
  a9f6c350
12 Apr, 2021 3 commits
- Merge branch 'ci/ralf/name-mangle-string-to-ident' into 'master' · cba13ce5
  Ralf Jung authored Apr 12, 2021
```
different approach for string_to_ident that works with name mangling

Closes #343

See merge request !660
```
  cba13ce5
- add back a version of string_to_ident · 57e813e6
  Ralf Jung authored Apr 12, 2021
  
  57e813e6
- note that things will be better in the future · 4d39284d
  Ralf Jung authored Apr 12, 2021
  
  4d39284d
11 Apr, 2021 2 commits
- Merge branch 'view-coreid' into 'master' · 01d4289b
  Ralf Jung authored Apr 11, 2021
```
Add CoreId instances for auth and view

See merge request !664
```
  01d4289b
- Add CoreId instances for auth and view · 346ca437
  Simon Friis Vindum authored Apr 11, 2021
  
  346ca437
08 Apr, 2021 3 commits
- update dependencies · 95637901
  Ralf Jung authored Apr 08, 2021
  
  95637901
- change name · 5941b28a
  Lennard Gäher authored Apr 08, 2021
  
  5941b28a
- fix bij_own_elem_agree; add bij_own_elem_auth_agree · 8ab2971e
  Lennard Gäher authored Apr 08, 2021
  
  8ab2971e