adapt to coq/coq#13840

See merge request iris/iris!635

rename u?frac_op/valid' to remove the final '

See merge request iris/iris!632

mostly make Iris compatible with name mangling

See merge request iris/iris!624

add "deprecated" and "staging" packages and deprecate some modules

See merge request iris/iris!602

create iris-deprecated and iris-staging packages, and deprecate some hard-to-use logic-level wrappers as well as view shift and Hoare triple notation

Fix wp_bind's error message

Closes #401

See merge request iris/iris!633

Fixes #401

Add tests for wp_load and wp_store failures

See merge request iris/iris!634

Rename monoid-related operational typeclass instances to include the suffix '_instance'

See merge request iris/iris!629

This was done using the following sed script:
sed -i -E 's/Instance ([a-zA-Z0-9_]+)( .*: (Op|P?Core|ValidN?|Unit) )/Instance \1_instance\2/' $(find iris/algebra -name "*.v")

only locally make uPred_holds a coercion

See merge request iris/iris!631

add _wand lemmas for big-ops

See merge request iris/iris!630

add big_sepM_filter

See merge request iris/iris!627

Generalize `big_opM_filter'` and `big_opS_filter'` to arbitrary monoids, and make arguments consistent.

Add [iSelect], and various tactics based on it

See merge request !625

add big_sepS_elem_of_acc_impl

See merge request iris/iris!570