Merge Requests · Iris

Rename instance `finmap_lookup_total` → `map_lookup_total`.

stdpp!220 · opened Jan 20, 2021 by Robbert
- 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
Remove hint db and import of omega, since omega will be removed from Coq.

stdpp!216 · opened Jan 19, 2021 by Robbert
- 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
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
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
- 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
prove take_0

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

stdpp!208 · opened Jan 11, 2021 by Ralf Jung
- MERGED
- 11
updated Jan 11, 2021
explicit Local/Global for all Instance, Arguments, Hint

stdpp!207 · opened Jan 07, 2021 by Ralf Jung
- MERGED
- 5
updated Jan 07, 2021
Better errors when opening an invariant/mask changing update around a non-atomic WP

iris!614 · opened Jan 05, 2021 by Robbert
- MERGED
- 10
updated Jan 08, 2021