Additional lemmas about map_imap

See merge request !175

Lemmas about "filter" on maps

See merge request !172

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

by Tej

prove NoDup_fmap_2_strong

See merge request !173

Fix #70: add pattern variant of bind notation

Closes #70

See merge request iris/stdpp!169

LICENSE: Clarify which BSD license is being used

See merge request !174

Sister MR to iris!472.

Sketch docs for computation on [gmap], since they're a FAQ

See merge request !171

Also, document why [simpl never] is not enough, with a link to an alternative
design.

drop support for Coq 8.7

See merge request !170

Use that in place of the old encoding:
iris/stdpp#70 (comment 52817)

Requires dropping support for Coq 8.7.

Add solver `multiset_solver` for multisets

See merge request !167

Prove theorem about delete of gset_to_gmap

See merge request !162

Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)

See merge request !164

Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512

See merge request !166