-
Robbert Krebbers authored
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.
146d90b0