Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
This tweak allows us to declare pvs as an instance of FromPure (it is not an instance of IntoPure), making some tactics (like iPureIntro and done) work with pvs too.
Robbert Krebbers authoredThis tweak allows us to declare pvs as an instance of FromPure (it is not an instance of IntoPure), making some tactics (like iPureIntro and done) work with pvs too.
