diff --git a/opam.pins b/opam.pins
index 45f895921f89077f43c738a2d0b8f7c1399bc669..64a42bfc68bc01ead7b24b50da388591541a08ed 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 613168bf8af3af0fe31873efd89038a89800792e
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 3103b7bf52d0275f2938d9af44ab2d0db89a6251
diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index a1b7774ce999e618848b1170fac892525de3ec52..d1f987623085f212d1b396cc27119b8a60452021 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -95,4 +95,8 @@ Hint Extern 1 (_ ⊆ _) => apply nclose_subseteq' : ndisj.
 Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
 Hint Resolve ndisj_difference_l : ndisj.
 
-Ltac solve_ndisj := solve [eauto with ndisj].
+Ltac solve_ndisj :=
+  repeat match goal with
+  | H : _ ∪ _ ⊆ _ |- _ => apply union_subseteq in H as [??]
+  end;
+  solve [eauto with ndisj].