GitLab

That way, we do not have useless type annotations of the form
"v : language.val heap_lang" cluttering about any goal.

Note, that we could decide to eta expand everywhere (as we do for ∀
and ∃), and use the notation "WP e {{ Q }}" for "wp e ⊤ (λ _, Q)".

and show that this is an instance of evaluation contexts

This required a new ectx axiom: Positivity of evaluation contexts. This axiom was
also present in the old Iris 1.1 development, back when it still derived lifting
axioms for ectx languages.

Thanks to Amin Timany for the suggestion.

Add both non-expansive and contractive functors, and bundle them for the general Iris instance as well as the global functor construction

This allows us to move the \later in the user-defined functor to any place we want.
In particular, we can now have "\later (iProp -> iProp)" in the ghost CMRA.

get rid of substitution in Case (use lambdas); introduce Match as derived form that involves binders

We no longer abuse empty strings for anonymous binders. Instead, we
now have a data type for binders: a binder is either named or
anonymous.

This cleans up some ad-hoc stuff and prepares for a generalization
of saved propositions.

It is based on type classes and can it be tuned by providing
instances, for example, instances can be provided to mark that
certain expressions are closed.

This avoids ambiguity with P and Q that we were using before for both
uPreds/iProps and indexed uPreds/iProps.

Also, make our redefinition of done more robust under different
orders of Importing modules.

The rationale is that, just like the always lemmas about uPred and the frame-preserving updates for maps and iprdos, the versions with the ' are the "more specific" versions, hard-coding more assumptions in the shape of their conclusion.

Also do some minor clean up.