Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
This could lead to awkward loops, for example, when having: - As goal `own γ c` with `c` persistent, one could keep on `iSplit`ting the goal. Especially in (semi-)automated proof scripts this is annoying as it easily leads to loops. - When having a hypothesis `own γ c` with `c` persistent, one could keep on `iDestruct`ing it. To that end, this commit removes the `IntoOp` and `FromOp` instances for persistent CMRA elements. Instead, we changed the instances for pairs, so that one, for example, can still split `(a ⋅ b, c)` with `c` persistent.
Robbert Krebbers authoredThis could lead to awkward loops, for example, when having: - As goal `own γ c` with `c` persistent, one could keep on `iSplit`ting the goal. Especially in (semi-)automated proof scripts this is annoying as it easily leads to loops. - When having a hypothesis `own γ c` with `c` persistent, one could keep on `iDestruct`ing it. To that end, this commit removes the `IntoOp` and `FromOp` instances for persistent CMRA elements. Instead, we changed the instances for pairs, so that one, for example, can still split `(a ⋅ b, c)` with `c` persistent.