Merge Requests · Iris

Make caesium an ectxi language

refinedc!18 · opened Jan 26, 2021 by Michael Sammler
- MERGED
- 0
updated Jan 26, 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
Fix cast insertion in the front end.

refinedc!17 · opened Jan 23, 2021 by Rodolphe Lepigre
- CLOSED
- 2
updated Jan 28, 2021
Add [iSelect], and various tactics based on it

iris!625 · opened Jan 22, 2021 by Rodolphe Lepigre
- MERGED
- 72
updated Jan 27, 2021
Rename instance `finmap_lookup_total` → `map_lookup_total`.

stdpp!220 · opened Jan 20, 2021 by Robbert Krebbers
- MERGED
- 2
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
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
mostly make Iris compatible with name mangling

iris!624 · opened Jan 19, 2021 by Ralf Jung
- MERGED
- 27
updated Feb 05, 2021
Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`.

iris!623 · opened Jan 19, 2021 by Robbert Krebbers
- MERGED
- 12
updated Jan 25, 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
add zip_with_diag and zip_diag

stdpp!215 · opened Jan 19, 2021 by Ralf Jung
- MERGED
- 1
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
Generalize frac to dfrac in auth and view camera 1 of 1 task completed

iris!622 · opened Jan 16, 2021 by Simon Friis Vindum
- MERGED
- 61
updated Mar 03, 2021
add Cinl_valid, Cinr_valid

iris!621 · opened Jan 14, 2021 by Ralf Jung
- MERGED
- 1
updated Jan 14, 2021
Sugar in the front end + Coq pretty printing

refinedc!16 · opened Jan 13, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 17
updated Jan 15, 2021
some big_sepL lemmas

iris!620 · opened Jan 12, 2021 by Ralf Jung
- MERGED
- 36
updated Jan 26, 2021
add some big_opS lemmas

iris!619 · opened Jan 12, 2021 by Ralf Jung
- MERGED
- 23
updated Jan 15, 2021
add set_map_union, set_map_singleton

stdpp!213 · opened Jan 12, 2021 by Ralf Jung
- MERGED
- 5
updated Jan 15, 2021
strengthen cmra_op_discrete

iris!618 · opened Jan 12, 2021 by Ralf Jung
- MERGED
- 3
updated Jan 15, 2021