diff --git a/opam b/opam
index 96a1b6ce42198be82ba61ded5fd5f1c51aada1aa..4b5cf369a16801b7ec3c64ce3ff50fbe7b7e211a 100644
--- a/opam
+++ b/opam
@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.6.1" & < "8.8~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2017-11-29.1") | (= "dev") }
+  "coq-stdpp" { (= "dev.2017-12-04.1") | (= "dev") }
 ]
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index aa371d768dbdbcd06f56fec424dcbee524cf040c..89aea2a78eb24aea1cdd701062b751d09bfeffdd 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -58,7 +58,7 @@ Lemma ht_mono s E P P' Φ Φ' e :
   (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ s; E {{ Φ' }} ⊢ {{ P }} e @ s; E {{ Φ }}.
 Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
 Lemma ht_stuck_mono s1 s2 E P Φ e :
-  stuckness_le s1 s2 → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}.
+  s1 ⊑ s2 → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}.
 Proof. by intros; apply persistently_mono, wand_mono, wp_stuck_mono. Qed.
 Global Instance ht_mono' s E :
   Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E).
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 42a7d97ef01881b28332e5014b2c34f3c3150fca..0525de9e6db84c18308b86dc11d05173eabf165b 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -22,6 +22,7 @@ Instance: PreOrder stuckness_le.
 Proof.
   split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
 Qed.
+Instance: SqSubsetEq stuckness := stuckness_le.
 
 Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
   if s is maybe_stuck then strongly_atomic else weakly_atomic.
@@ -315,7 +316,7 @@ Proof.
   iIntros "{$H}" (v) "?". by iApply HΦ.
 Qed.
 Lemma wp_stuck_mono s1 s2 E e Φ :
-  stuckness_le s1 s2 → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
+  s1 ⊑ s2 → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
 Proof. case: s1; case: s2 => // _. exact: wp_stuck_weaken. Qed.
 Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
 Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. Qed.