diff --git a/coq-iris.opam b/coq-iris.opam
index 39b99c3cb79f77978b4f4f64674be54778ba7670..c7b397154240bbbaeae855f47f936b8b8304ef95 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2022-08-11.0.66a28855") | (= "dev") }
+  "coq-stdpp" { (= "dev.2022-08-11.3.67890e47") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 07f48e154177334ffe7254c96efdd575ba844546..039c2d751380c91c0a549e76341821d14c2f0b50 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -158,11 +158,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_equiv_ext=>y. apply oFunctor_map_id.
+  apply list_fmap_equiv_ext=>???. apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_equiv_ext=>y; apply oFunctor_map_compose.
+  apply list_fmap_equiv_ext=>???; apply oFunctor_map_compose.
 Qed.
 
 Global Instance listOF_contractive F :
diff --git a/iris_unstable/algebra/list.v b/iris_unstable/algebra/list.v
index 0afcf8c308ddecdf3cded03ba6671197ab37022d..ee55e1a16b95ea7f91b2c2206e63f93d36017b2e 100644
--- a/iris_unstable/algebra/list.v
+++ b/iris_unstable/algebra/list.v
@@ -526,7 +526,7 @@ Proof.
   - intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
     by apply (cmra_morphism_validN (fmap f : option A → option B)).
   - intros l. apply Some_proper. rewrite -!list_fmap_compose.
-    apply list_fmap_equiv_ext, cmra_morphism_core, _.
+    apply list_fmap_equiv_ext=>???. apply cmra_morphism_core, _.
   - intros l1 l2. apply list_equiv_lookup=>i.
     by rewrite list_lookup_op !list_lookup_fmap list_lookup_op cmra_morphism_op.
 Qed.
@@ -540,11 +540,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_equiv_ext=>y. apply urFunctor_map_id.
+  apply list_fmap_equiv_ext=>???. apply urFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_equiv_ext=>y; apply urFunctor_map_compose.
+  apply list_fmap_equiv_ext=>???; apply urFunctor_map_compose.
 Qed.
 
 Global Instance listURF_contractive F :