wp_apply instantiates evars too far
Lemma wp_apply_evar e :
(∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof.
iIntros "H". wp_apply "H".
The goal is now
============================
--------------------------------------∗
WP ?e @ ?s; ?E {{ v, ?Φ v }}
but it should be
============================
--------------------------------------∗
?Q
This is in the generalized proofmode branch.