pm_reduce just reduces away proof mode terms using cbv; pm_prettify just prettifies user-visible connectors using cbn.
Most uses of pm_default are converted to default to keep the desired reduction behavior.

make pm_maybe_wand a BI connective; reduce BI connectives and option combinators in the proofmode with cbn

* move PROP-envs definitions to environments.v so that we can control them without pulling in coq_tactics
* use reduction-controlled `pm_default` for proofmode accessors

It now turns the goal into `P` and `<pers> Q`, which is dual to
`iDestruct`, which turns `P ∧ <pers> Q` into `P` and `□ Q`.

If the accessor introduces a binder, the first Coq-level intro pattern of `iInv`
is used for that binder unless the type of the binder is unit, in which case
`iInv` removes it completely.  Binders on the closing view shift are not (yet)
supported as they are harder to smoothly eliminate in the unit case.

New IntoAcc typeclass to decouple creating and elliminating accessors; ElimInv supports both with and without Hclose

Extend ElimModal with Boolean flags to specify whether it operates on the persistent/spatial context.

Split [FromAssumption] into three, depending on wheter the parameters are evars. This is to avoid loops in TC search.

sed -i 's/absolute/objective/g; s/relative/subjective/g; s/Absolute/Objective/g; s/Relative/Subjective/g' $(find ./ -name \*.v)

Based on an earlier MR by @jung.

This requires changing the Hint Mode of the [Frame] type class because it should not fail if its parameter is an evar, but instantiate it instead. In order to prevent all the other instances of [Frame] to intantiate this evar themselves, we create a new type class [KnwonFrame], which corresponds to the old behavior.

See the discussion in #163.