change IntoVal so that it is easier to use in specs

See merge request FP/iris-coq!159

Improve and test more proof mode error messages

See merge request FP/iris-coq!160

Separating big operator over two lists.

See merge request FP/iris-coq!158

All those for `big_sepL` that hold.

We already do the same for the goal, this avoids some scope
delimiters being displayed.

move the reduction control of the proofmode to its own file and tweak it

See merge request FP/iris-coq!150

Typeclass to overload WP notation.

See merge request FP/iris-coq!146

* 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

Shorten proofmode error messages and test them

See merge request FP/iris-coq!156

different approach to monPred framing

See merge request FP/iris-coq!157