-
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.
10a93b0b
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.