• Robbert Krebbers's avatar
    No longer allow ownership of persistent elements to be split. · 383fee40
    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.
    383fee40
class_instances.v 31.7 KB