Merge Requests · Iris

Strengthen the [LocInBounds] infrastructure.

refinedc!22 · opened Feb 01, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 11
updated Feb 02, 2021
rename u?frac_op/valid' to remove the final '

iris!632 · opened Feb 01, 2021 by Ralf Jung
- MERGED
- 7
updated Feb 10, 2021
only locally make uPred_holds a coercion

iris!631 · opened Jan 29, 2021 by Ralf Jung
- MERGED
- 5
updated Jan 29, 2021
Add several simple lemmas (mostly about list and map filter).

stdpp!226 · opened Jan 29, 2021 by Paulo Emílio de Vilhena
- MERGED
- 31
updated Feb 15, 2021
Infrastructure for [SimpleSubsumeVal].

refinedc!21 · opened Jan 29, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 0
updated Feb 01, 2021
add _wand lemmas for big-ops

iris!630 · opened Jan 29, 2021 by Ralf Jung
- MERGED
- 1
updated Jan 29, 2021
add pred_infinite_surj

stdpp!225 · opened Jan 29, 2021 by Ralf Jung
- MERGED
- 7
updated Feb 01, 2021
Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`

stdpp!224 · opened Jan 29, 2021 by Robbert Krebbers
- MERGED
- 8
updated Jan 29, 2021
Fix inversion of signedness for [uintptr_t] and [intptr_t].

refinedc!20 · opened Jan 28, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Jan 28, 2021
Rename monoid-related operational typeclass instances to include the suffix '_instance'

iris!629 · opened Jan 28, 2021 by Ralf Jung
- MERGED
- 3
updated Feb 01, 2021
Rename `Forall_Forall2` → `Forall_Forall2_diag`

stdpp!223 · opened Jan 28, 2021 by Robbert Krebbers
- MERGED
- 1
updated Jan 28, 2021
Rename `equiv_spec` → `equiv_entails` to be consistent with conventions in std++.

iris!628 · opened Jan 28, 2021 by Robbert Krebbers
- MERGED
- 5
updated Feb 12, 2021
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
add big_sepM_filter

iris!627 · opened Jan 27, 2021 by Ralf Jung
- MERGED
- 8
updated Jan 29, 2021
Performance improvements?

refinedc!19 · opened Jan 27, 2021 by Michael Sammler
- MERGED
- 0
updated Jan 27, 2021
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
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