Makes it possible to use several logical steps for one logical steps, in a way which can be controlled by ghost state.

create iris-deprecated and iris-staging packages, and deprecate some hard-to-use logic-level wrappers as well as view shift and Hoare triple notation

Done with a script by Tej; see
iris/iris!609 for details.

This makes sure that when trying to open an invariant or to eliminate a mask-changing
update around a non-atomic WP that it doesn't fail with "cannot eliminate modality",
but instead gives an side-condition `Atomic ...` informing the user what's going on.

Unlike the class `ElimModal` and `ElimInv`, the class `ElimAcc` was not yet equipped
with a Coq side-condition. This commit adds such a side-condition.