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

Make projections of BI operational type classes `Typeclasses Opaque`.

See merge request iris/iris!914

Update prelude file to use new ssreflect file from std++.

See merge request iris/iris!917

Bump stdpp

See merge request iris/iris!915

drop support for Coq 8.14

See merge request iris/iris!908

This avoids weird unification, where `@bupd ? ? ?` is unified with `@plainly ? ? ?`.

`embed` was already opaque, but `bupd`/`fupd`/`plainly`/`internal_eq` were not.

Make `BiLaterContractive` a class instead of a notation.

See merge request iris/iris!913

This avoids unnecessary search on failed attempts. `Contractive` is notation for
`Proper`, so previously, this caused a bunch of setoid instances to be used. In
turn, this resulted in TC debug output that is hard to read.

Make `persistently_True` a bi-entailment.

See merge request iris/iris!912

Generalize `intuitionistically_intro` to general BI.

See merge request iris/iris!911