GitLab

As reported by @jjourdan: framing now no longer back tracks on whether
to strip laters or not. When framing below a later, we now only make it
strip laters of the head of the frame.

The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

Revert "Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type."

This reverts commit fa897ff5.

The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

Fixed by stdpp 93b4ec70e13a573a9055a5bf1269f5885e18e843.

We now use the `Maybe` prefix as also used for `Frame`: it indicates
whether progress has been made by stripping of a later or not.

We already supported framing under wands.

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

This partially solves #112.

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.

This used to be done by using `ElimModal` in backwards direction. Having
a separate type class for this gets rid of some hacks:

- Both `Hint Mode`s in forward and backwards direction for `ElimModal`.
- Weird type class precedence hacks to make sure the right instance is picked.
  These were needed because using `ElimModal` in backwards direction caused
  ambiguity.