- Jul 28, 2021
-
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Robbert Krebbers authored
-
Hai Dang authored
-
Robbert Krebbers authored
Use `_True` and `_False` for the specific cases. Weaken premise of `map_filter_delete_not` and make it consistent with `map_filter_insert_not'`.
-
- Jul 27, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Write them all using `
` and consistently use the `_iff` suffix. -
Robbert Krebbers authored
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 26, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Rename `gmultiset_elem_of_singleton_subseteq` → `gmultiset_singleton_subseteq_l` and swap order to be consistent with Iris's `singleton_included_l`.
-
- Jul 24, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 23, 2021
-
-
Ralf Jung authored
-
- Jul 22, 2021
-
-
Ralf Jung authored
-
- Jul 21, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jul 19, 2021
-
-
Robbert Krebbers authored
This also applies to `(un)curry{3,4}`, `gmap_(un)curry`, and `h(un)curry`. This fixes issue #76. The code includes a horrible hack that should removed once support for Coq versions prior to 8.13 is dropped.
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jul 18, 2021
-
-
- Jul 17, 2021
-
-
Ralf Jung authored
-