diff --git a/opam b/opam
index 394966d9a31d56a7e9c578f6c33dc2fcf09288e4..3fe858916b49919ac045e42858b61e2993497c5c 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.2018-02-02.0") | (= "dev") }
+  "coq-stdpp" { (= "dev.2018-02-08.0") | (= "dev") }
 ]
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 7212515e4ea4a537408931b54b3098fbed48cddb..9f042b3fab53bd5c119c59b796ce3b78e06d7974 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -638,9 +638,10 @@ Global Instance make_later_default P : MakeLater P (â–· P) | 100.
 Proof. done. Qed.
 
 Global Instance frame_later p R R' P Q Q' :
-  IntoLaterN 1 R' R → Frame p R P Q → MakeLater Q Q' → Frame p R' (▷ P) Q'.
+  NoBackTrack (IntoLaterN 1 R' R) →
+  Frame p R P Q → MakeLater Q Q' → Frame p R' (▷ P) Q'.
 Proof.
-  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
+  rewrite /Frame /MakeLater /IntoLaterN=>-[->] <- <-.
   by rewrite persistently_if_later later_sep.
 Qed.
 
@@ -651,9 +652,10 @@ Global Instance make_laterN_default P : MakeLaterN n P (â–·^n P) | 100.
 Proof. done. Qed.
 
 Global Instance frame_laterN p n R R' P Q Q' :
-  IntoLaterN n R' R → Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
+  NoBackTrack (IntoLaterN n R' R) →
+  Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
 Proof.
-  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
+  rewrite /Frame /MakeLater /IntoLaterN=>-[->] <- <-.
   by rewrite persistently_if_laterN laterN_sep.
 Qed.