Skip to content
  • Robbert Krebbers's avatar
    Thread `Atomic` side-condition through `ElimModal`, `ElimAcc` and `ElimInv`. · 146d90b0
    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