diff --git a/opam.pins b/opam.pins
index b685c00b81bfb08a29c11823c6c1d399b8b9e98c..d5fd7ce49259c072f6e22e9d8058afe88458eb55 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp fa6ff9d18aefb29e839e815aa170262d330bd108
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 2d27f42b9c4d9e5c0810122779a93873050fb756
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 821092226a318e953c1a97e217590cd01b35016a..775d5655818cc39353fdfe74a402c935e22a3000 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -493,7 +493,7 @@ Qed.
 
 (** * Implication and wand *)
 Lemma tac_impl_intro Δ Δ' i P Q :
-  (if env_spatial_is_nil Δ then Unit else PersistentP P) →
+  (if env_spatial_is_nil Δ then TCTrue else PersistentP P) →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.