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.