Merge Requests · Iris

Rename `_11` and `_12` suffixes into `_1_1` and `_1_2`

stdpp!222 · opened Jan 27, 2021 by Robbert Krebbers
- MERGED
- 1
updated Jan 28, 2021
Fix documentation of `select` to state that it selects the "last" hypothesis.

stdpp!221 · opened Jan 25, 2021 by Robbert Krebbers
- MERGED
- 6
updated Jan 27, 2021
Add [iSelect], and various tactics based on it

iris!625 · opened Jan 22, 2021 by Rodolphe Lepigre
- MERGED
- 72
updated Jan 27, 2021
Performance improvements?

refinedc!19 · opened Jan 27, 2021 by Michael Sammler
- MERGED
- 0
updated Jan 27, 2021
Make `wp_apply` perform `wp_pure` in small steps until the lemma matches the goal.

iris!587 · opened Nov 12, 2020 by Robbert Krebbers Iris 3.4
- MERGED
- 20
updated Jan 27, 2021
Make caesium an ectxi language

refinedc!18 · opened Jan 26, 2021 by Michael Sammler
- MERGED
- 0
updated Jan 26, 2021
add big_sepS_elem_of_acc_impl

iris!570 · opened Nov 04, 2020 by Ralf Jung Iris 3.4
- MERGED
- 25
updated Jan 26, 2021
some big_sepL lemmas

iris!620 · opened Jan 12, 2021 by Ralf Jung
- MERGED
- 36
updated Jan 26, 2021
Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`.

iris!623 · opened Jan 19, 2021 by Robbert Krebbers
- MERGED
- 12
updated Jan 25, 2021
add mono_nat_auth_lb

iris!605 · opened Dec 18, 2020 by Ralf Jung
- MERGED
- 7
updated Jan 25, 2021
Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}`.

stdpp!206 · opened Jan 04, 2021 by Robbert Krebbers
- MERGED
- 24
updated Jan 23, 2021
Rename instance `finmap_lookup_total` → `map_lookup_total`.

stdpp!220 · opened Jan 20, 2021 by Robbert Krebbers
- MERGED
- 2
updated Jan 20, 2021
add map_zip_diag and the lemmas required for that

stdpp!217 · opened Jan 20, 2021 by Ralf Jung
- MERGED
- 25
updated Jan 20, 2021
remove unused find_pat tactic

stdpp!219 · opened Jan 20, 2021 by Ralf Jung
- MERGED
- 1
updated Jan 20, 2021
add rename-by-pattern tactic

stdpp!218 · opened Jan 20, 2021 by Ralf Jung
- MERGED
- 5
updated Jan 20, 2021
Added select and select_revert tactics 2 of 2 tasks completed

stdpp!142 · opened Apr 09, 2020 by Michael Sammler
- MERGED
- 48
updated Jan 20, 2021
Remove hint db and import of omega, since omega will be removed from Coq.

stdpp!216 · opened Jan 19, 2021 by Robbert Krebbers
- MERGED
- 0
updated Jan 19, 2021
fix and reject warnings on Coq 8.13

stdpp!214 · opened Jan 19, 2021 by Ralf Jung
- MERGED
- 1
updated Jan 19, 2021
add zip_with_diag and zip_diag

stdpp!215 · opened Jan 19, 2021 by Ralf Jung
- MERGED
- 1
updated Jan 19, 2021
Alternative definition of contextual refinement

reloc!5 · opened Dec 12, 2020 by Dan Frumin
- MERGED
- 5
updated Jan 17, 2021