[Iris-Club] Final breaking changes before Iris 3.0

[Ralf Jung]

Hi again,

> ## Handling of physical state in WP
> 
> WP is now parameterized over a predicate on physical state, instead of
> using the construction that reflect the entire physical state as one
> exclusive piece of ghost state.  This makes the overall infrastructure
> simpler for simple languages (in particular, heap_ctx is gone!).  More
> complex languages may still have to use the old construction, which is
> provided by program_logic.ownp.  Since we don't use that compatibility
> layer ourselves, we would appreciate feedback about inconveniences or
> missing features.  (Merge requests are the best form of feedback ;)

As an example for how to port a language to the compatibility layer, see
the changes in theories/lang/ made by
<https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/741c78cf94dc4a510d945e02119ed59328756ee1>.

Kind regards,
Ralf