add lemmas for 'separable' propositions

See merge request iris/iris!881

re-export std++ options

See merge request iris/iris!922

Better handling of `let` bindings in proof mode

Closes #520

See merge request iris/iris!921

This fixes the second bug in issue #520.

These should either be `simpl`ed or introduced into the Coq context.
Fixes the first bug in issue #520.

Thanks, Johannes!

make Prop-level BI connectives notation for bi_emp_valid (rather than bi_entails)

See merge request iris/iris!791

add locality annotation to all Typeclasses Opaque/Transparent

See merge request iris/iris!918

use more primitive projections in cmra.v

See merge request iris/iris!919

spygame and time-credits don't send nightly build results to the shared iris-dev; also don't run them in rev-dep checks