Merge Requests · Iris

reuse PreG class in G class where possible

iris!617 · opened Jan 12, 2021 by Ralf Jung
- MERGED
- 4
updated Jan 12, 2021
Unfold instantiated evars on each liRStep.

refinedc!15 · opened Jan 12, 2021 by Rodolphe Lepigre
- MERGED
- 1
updated Jan 12, 2021
Encode the constrained type into own_constrained.

refinedc!14 · opened Dec 18, 2020 by Rodolphe Lepigre
- MERGED
- 3
updated Jan 14, 2021
add Cinl_valid, Cinr_valid

iris!621 · opened Jan 14, 2021 by Ralf Jung
- MERGED
- 1
updated Jan 14, 2021
strengthen cmra_op_discrete

iris!618 · opened Jan 12, 2021 by Ralf Jung
- MERGED
- 3
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
add some big_opS lemmas

iris!619 · opened Jan 12, 2021 by Ralf Jung
- MERGED
- 23
updated Jan 15, 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
Alternative definition of contextual refinement

reloc!5 · opened Dec 12, 2020 by Dan Frumin
- MERGED
- 5
updated Jan 17, 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
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
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
add rename-by-pattern tactic

stdpp!218 · opened Jan 20, 2021 by Ralf Jung
- MERGED
- 5
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 map_zip_diag and the lemmas required for that

stdpp!217 · opened Jan 20, 2021 by Ralf Jung
- MERGED
- 25
updated Jan 20, 2021
Rename instance `finmap_lookup_total` → `map_lookup_total`.

stdpp!220 · opened Jan 20, 2021 by Robbert Krebbers
- MERGED
- 2
updated Jan 20, 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
add mono_nat_auth_lb

iris!605 · opened Dec 18, 2020 by Ralf Jung
- MERGED
- 7
updated Jan 25, 2021
Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`.

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