GitLab

* 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.

We do this in two ways:

- Use `notypeclasses refine` instead of `eapply`, to avoid type class
  search being called arbitrary.
- Use `typeclasses eauto` instead of `apply _`, to avoid type class
  search being called on unrelated evars.

I mainly tried this for `iSpecialize` and friends; this same remains to
be done for all other tactics.

This commit also makes partial progress w.r.t. issue #135.

Based on an earlier MR by @jung.

See the discussion in #163.