Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
It is no longer triggered when posing [P ⊢ Q] with [P] an evar. This, for example, makes sure that iApply pvs_intro works, which failed before.
Robbert Krebbers authoredIt is no longer triggered when posing [P ⊢ Q] with [P] an evar. This, for example, makes sure that iApply pvs_intro works, which failed before.
