diff --git a/opam.pins b/opam.pins
index b4cfbbf51ecf2b5b1fa9b0b3eb5e9be59999a872..ee2d15f4df23e9a795c02d8d0eea4c6754bacab2 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 6ffa20c8f23797f81f1bb55ab27432e897de71d5
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 0ac2b4db07bdc471421c5a4c47789087b3df074c
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 8376ee688798102d13bdb1abc5a6b8a219ba3058..adf16b59dde19df928d6dbc898a54b4a1b2c4a5a 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -46,7 +46,7 @@ Section core.
   Proof.
     split.
     - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
-      iClear "∗". iAlways. by iApply HP.
+      iAlways. by iApply HP.
     - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
       iDestruct (coreP_elim with "HcQ") as "#HQ". done.
   Qed.