add pred_infinite_surj

See merge request !225

rename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteq

See merge request !210

rename elem_of_equiv -> set_equiv and set_equiv_spec -> set_equiv_subseteq, and rename some instances to get out of the way

Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`

See merge request !224

Rename `Forall_Forall2` → `Forall_Forall2_diag`

See merge request !223

names for big operators in Iris.

Rename `_11` and `_12` suffixes into `_1_1` and `_1_2`

See merge request !222

Fix documentation of `select` to state that it selects the "last" hypothesis.

See merge request !221

Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}`.

See merge request !206

Robbert Krebbers authored 4 years ago and Ralf Jung committed 4 years ago

* Add lemma `map_omap_union`.
* Add lemmas `map_disjoint_fmap` and `map_disjoint_omap`.
* Add lemmas `fmap_merge` and `omap_merge`.
* Add lemma `omap_delete`.
* Generalize `omap_insert` and `omap_singleton` to cover both the `Some` and `None` case. Add `_Some` and `_None` versions of the lemmas for the specific cases.
* Generalize `map_size_insert` and `map_size_delete` in the same way.
* Add lemmas `lookup_fmap_Some`, `lookup_omap_Some`, and `lookup_omap_id_Some`.

Rename instance `finmap_lookup_total` → `map_lookup_total`.

See merge request iris/stdpp!220

add map_zip_diag and the lemmas required for that

See merge request iris/stdpp!217

remove unused find_pat tactic

Closes #93

See merge request !219

add rename-by-pattern tactic

See merge request iris/stdpp!218

Remove hint db and import of omega, since omega will be removed from Coq.

See merge request !216

fix and reject warnings on Coq 8.13

See merge request !214

add zip_with_diag and zip_diag

See merge request !215

See https://github.com/coq/coq/pull/13741#issuecomment-762761112