Use `NoBackTrack` type class for framing with ▷

Closes #153

See merge request FP/iris-coq!112

Various improvements to iFrame

Closes #145

See merge request FP/iris-coq!110

We already supported framing under wands.

For example, framing `P` in `(P ∨ Q) ∗ R` now succeeds and turns the goal into `R`.

Make invariants closed under weakening.

See merge request FP/iris-coq!85

This partially solves #112.

Consistently name `wp_value_inv`

See merge request FP/iris-coq!108

`iEval  ... in ...` for performing a tactic in an invidual proofmode hypothesis

Closes #116

See merge request FP/iris-coq!105

This is to make sure that e.g. `//` in `iEval (rewrite .. // ..)` does
not immediately close the goal by reflexivity.

This should fix iris-examples.

We already used the following naming convention: `wp_value'` is stated in
terms of `of_val` and `wp_value` is stated in terms of `IntoVal`. This
commit applies this convention to `wp_value_inv` as well.