diff --git a/opam b/opam
index a5cc0c9b4e64af82eb361f98dbe1d27f98144125..1b8a693e280b2d46925b3d0a815a7ae4d255a569 100644
--- a/opam
+++ b/opam
@@ -11,7 +11,7 @@ synopsis: "This is the Coq development of the Iris Project"
 
 depends: [
   "coq" { (>= "8.9.1" & < "8.12~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2020-03-10.1.20ef8941") | (= "dev") }
+  "coq-stdpp" { (= "dev.2020-03-10.2.8db97649") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 93876587b5f7e4c67ede34e2a0e93094ebef2653..eaf0b0b936e3f914bfbd8d388b5ff1549e678923 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -227,6 +227,9 @@ Proof.
   done.
 Qed.
 
+Lemma test_iSpecialize_evar P : (∀ R, R -∗ R) -∗ P -∗ P.
+Proof. iIntros "H HP". iApply ("H" with "[HP]"). done. Qed.
+
 Lemma test_iPure_intro_emp R `{!Affine R} :
   R -∗ emp.
 Proof. iIntros "HR". by iPureIntro. Qed.