put it into a type class `BiPureForall`.

This property does not hold for embeddings of classical logic into Coq.

Preserve identifiers in binders where possible, analogous to the support
for destructing existentials in !479.

Fixes #336.

Tej Chajed authored Jul 21, 2020 and Robbert Krebbers committed Jul 21, 2020

When running `iDestruct "H" as (?) "H"`, use the name of the binder in
"H". For example, if "H" has type `∃ y, Φ y`,  we now use `y` as the
name of the variable after freshening. Previously the name was always
the equivalent of running `fresh H`.

The implementation achieves this by forwarding the desired identifier
name through the `IntoExist` typeclass. Identifiers are serialized in
Gallina by using them as the name of a function of type `ident_name :=
unit -> unit`.

This fixes some issues in GPS and RustBelt-relaxed, where the old
unification algorithm is now too weak.

This is in preparation for coq/coq#9274.

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

These instances are the same as those for e.g. the later modality.