Merge Requests · Iris

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
- 62
updated Mar 05, 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
Unfold instantiated evars on each liRStep.

refinedc!15 · opened Jan 12, 2021 by Rodolphe Lepigre
- MERGED
- 1
updated Jan 12, 2021
reuse PreG class in G class where possible

iris!617 · opened Jan 12, 2021 by Ralf Jung
- MERGED
- 4
updated Jan 12, 2021
Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib

stdpp!212 · opened Jan 11, 2021 by Robbert Krebbers
- MERGED
- 2
updated Jan 11, 2021
upstream some list_numbers lemmas from Perennial

stdpp!211 · opened Jan 11, 2021 by Ralf Jung
- MERGED
- 12
updated Jan 11, 2021
rename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteq

stdpp!210 · opened Jan 11, 2021 by Ralf Jung
- MERGED
- 32
updated Feb 01, 2021
prove take_0

stdpp!209 · opened Jan 11, 2021 by Ralf Jung
- MERGED
- 1
updated Jan 11, 2021