- Jan 15, 2021
-
-
Ralf Jung authored
-
- Jan 11, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
prove map_size_delete, map_size_insert_Some, map_to_list_delete See merge request iris/stdpp!208
-
Robbert Krebbers authored
Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib See merge request iris/stdpp!212
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
upstream some list_numbers lemmas from Perennial See merge request iris/stdpp!211
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Proofs by Tej
-
Robbert Krebbers authored
prove take_0 See merge request iris/stdpp!209
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jan 08, 2021
-
-
Ralf Jung authored
-
- Jan 07, 2021
-
-
Robbert Krebbers authored
explicit Local/Global for all Instance, Arguments, Hint See merge request !207
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename... See merge request iris/stdpp!205
-
- Jan 04, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
-
- Dec 24, 2020
-
-
Robbert Krebbers authored
-
- Dec 11, 2020
-
-
Ralf Jung authored
-
- Dec 10, 2020
-
-
Ralf Jung authored
-
- Dec 09, 2020
-
-
Ralf Jung authored
-
- Dec 04, 2020
-
-
Robbert Krebbers authored
add insert_subseteq_l See merge request iris/stdpp!204
-
Ralf Jung authored
-
Ralf Jung authored
-
- Nov 26, 2020
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Replace unused pattern variables with underscore See merge request iris/stdpp!203
-
- Nov 23, 2020
-
-
Tej Chajed authored
Addresses new unused-pattern-matching-variable warning on Coq master.
-
Robbert Krebbers authored
Add explicit Global to hints at top level See merge request iris/stdpp!202
-
- Nov 20, 2020
-
-
Tej Chajed authored
Fixes new Coq master warning deprecated-hint-without-locality.
-
- Nov 15, 2020
-
-
Ralf Jung authored
-
