diff --git a/opam b/opam
index 1b8a693e280b2d46925b3d0a815a7ae4d255a569..ba44b0eae8ac8dee96c7b917dfd96f6d8713eab5 100644
--- a/opam
+++ b/opam
@@ -11,7 +11,7 @@ synopsis: "This is the Coq development of the Iris Project"
 
 depends: [
   "coq" { (>= "8.9.1" & < "8.12~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2020-03-10.2.8db97649") | (= "dev") }
+  "coq-stdpp" { (= "dev.2020-03-17.3.ad2e80d6") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index 611f5623ba4476a6bc2de649eb8378fb1d236455..3a3990a955f6f11d10e9fecce115f54a40da93dd 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -91,7 +91,7 @@ Lemma mapsto_seq_array l q v n :
 Proof.
   rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
   { done. }
-  iIntros "[$ Hl]". rewrite -fmap_seq big_sepL_fmap.
+  iIntros "[$ Hl]". rewrite -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
   setoid_rewrite <-loc_add_assoc. iApply "IH". done.
 Qed.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 9f403fd1a81c6296a7484b44cef8045725870fe6..8619893ad3e64c090ddd95139311b3af35b2043f 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -249,7 +249,7 @@ Proof.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
     intros (j&?&Hjl&_)%heap_array_lookup.
     rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
-  rewrite loc_add_0 -fmap_seq big_sepL_fmap.
+  rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
   setoid_rewrite <-loc_add_assoc.
   rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
@@ -265,7 +265,7 @@ Proof.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
     intros (j&?&Hjl&_)%heap_array_lookup.
     rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
-  rewrite loc_add_0 -fmap_seq big_sepL_fmap.
+  rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
   setoid_rewrite <-loc_add_assoc.
   rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".