It can be infered now.

It used to be an inline pattern match.

This also restores compatibility with Coq 8.6.1.

saved predicates: use ofe_fun, not ofe_mor

See merge request FP/iris-coq!86

generalize savedProp to let the user control the position of the type-level later

See merge request FP/iris-coq!76

It does not really help since the main work of the proof is in showing that
`cFunctor_map F (iProp_fold, iProp_unfold)` is injective, but whatever.

Fix typo in definition of weakest pre in documentation.

See merge request FP/iris-coq!84

This is an old flag set by the ssr plugin, and recently unset in coq-stdpp,
see https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/issues/5.

Improved treatment of anonymous hypotheses in the proof mode

See merge request FP/iris-coq!83