Add explicit Local/Global to hints at top level

See merge request iris/iris!594

Fixes new Coq master warning deprecated-hint-without-locality
(https://github.com/coq/coq/pull/13188).

link to pinned-package-versions page

See merge request iris/iris!590

This reverts merge request !591

Make iDestruct consume wands when it's supposed to

See merge request !591

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

`iDestruct ("H" with "HP")` where "H" is persistent is supposed to
consume "H" if it isn't a forall. Due to a bug in the tactic, this
behavior was never triggered and "H" was always left alone.

make pure_exec_fill not an instance any more

See merge request iris/iris!588

bupd, fupd: add idempotence lemmas

See merge request iris/iris!592

Add back a proofmode test for issue #288

See merge request iris/iris!584

Use original pattern in iDestruct error messages

See merge request iris/iris!550

This test is incompatible with Coq 8.8 and Coq 8.9, but Iris no longer
supports those versions.

multi-package repositories

See merge request iris/iris!514

add big_opM_singletons

See merge request iris/iris!567

avoid (e)apply in wp_expr_eval

See merge request iris/iris!582

Rename mapsto_mapsto_ne and add easier-to-use variant

See merge request iris/iris!574