Forked from
Iris / Iris
Source project has a limited visibility.
-
Jacques-Henri Jourdan authored
When using [iAssert ... with ">[]"], we should not use [tac_assert_persistent], and eliminate the modality instead. This patch is still not ideal, because some modalities (e.g., later) preserve persistence.
Jacques-Henri Jourdan authoredWhen using [iAssert ... with ">[]"], we should not use [tac_assert_persistent], and eliminate the modality instead. This patch is still not ideal, because some modalities (e.g., later) preserve persistence.