Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
It now turns the goal into `P` and `<pers> Q`, which is dual to `iDestruct`, which turns `P ∧ <pers> Q` into `P` and `□ Q`.
Robbert Krebbers authoredIt now turns the goal into `P` and `<pers> Q`, which is dual to `iDestruct`, which turns `P ∧ <pers> Q` into `P` and `□ Q`.
