GitLab

After Coq PR #7825 this will create unwanted evars.

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

All those for `big_sepL` that hold.

* 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

This avoids the proofmode to be irritated by unrelated goals with a typeclass
type.

This fixes issue #187.

This follows the proof at https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem

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

This fixes issue #182.

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