diff --git a/coq-iris.opam b/coq-iris.opam
index 34fbd4a5e439bac62847a51d9226a522811b13c5..2a6738e3e4e9f4ef2d70bce26720c47d6049c527 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2024-09-08.0.d37b5e70") | (= "dev") }
+  "coq-stdpp" { (= "dev.2024-09-10.3.a1a12e00") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 4db325d7c1e775d6bde4b45d891b189d15ccff57..1018168a70c7198df8103c791afe6d1208637d1c 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1196,7 +1196,7 @@ Tactic Notation "iSplit" :=
 
 Tactic Notation "iSplitL" constr(Hs) :=
   iStartProof;
-  let Hs := words Hs in
+  let Hs := String.words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let Δ := iGetCtx in
   eapply tac_sep_split with Left Hs _ _; (* (js:=Hs) *)
@@ -1212,7 +1212,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
 
 Tactic Notation "iSplitR" constr(Hs) :=
   iStartProof;
-  let Hs := words Hs in
+  let Hs := String.words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let Δ := iGetCtx in
   eapply tac_sep_split with Right Hs _ _; (* (js:=Hs) *)
@@ -1481,7 +1481,7 @@ Tactic Notation "iDestructHyp" constr(H) "as"
 
 (** * Combinining hypotheses *)
 Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
-  let Hs := words Hs in
+  let Hs := String.words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let H := iFresh in
   let Δ := iGetCtx in
@@ -1502,7 +1502,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat) :=
   iCombine [H1;H2] as pat.
 
 Tactic Notation "iCombineGivesCore" constr(Hs) "gives" tactic3(tac) :=
-  let Hs := words Hs in
+  let Hs := String.words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let H := iFresh in
   let Δ := iGetCtx in
@@ -1534,7 +1534,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2)
 
 Tactic Notation "iCombineAsGivesCore" constr(Hs) "as" constr(pat1)
                                       "gives" tactic3(tac) :=
-  let Hs := words Hs in
+  let Hs := String.words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let H1 := iFresh in
   let H2 := iFresh in
diff --git a/iris/proofmode/tokens.v b/iris/proofmode/tokens.v
index a450d6c2fea4d9c4959174ab547df052370fad5b..8885c26d96de2d1d0beb2d5842baa3b7eebf9bad 100644
--- a/iris/proofmode/tokens.v
+++ b/iris/proofmode/tokens.v
@@ -37,8 +37,8 @@ Inductive state :=
 Definition cons_state (kn : state) (k : list token) : list token :=
   match kn with
   | SNone => k
-  | SName s => TName (string_rev s) :: k
-  | SPure s => TPure (if String.eqb s "" then None else Some (string_rev s)) :: k
+  | SName s => TName (String.rev s) :: k
+  | SPure s => TPure (if String.eqb s "" then None else Some (String.rev s)) :: k
   | SNat n => TNat n :: k
   end.
 
@@ -77,17 +77,17 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
   | String a s =>
      (* TODO: Complain about invalid characters, to future-proof this
      against making more characters special. *)
-     if is_space a then tokenize_go s (cons_state kn k) SNone else
+     if Ascii.is_space a then tokenize_go s (cons_state kn k) SNone else
      match kn with
      | SNone =>
-        match is_nat a with
+        match Ascii.is_nat a with
         | Some n => tokenize_go s k (SNat n)
         | None => tokenize_go s k (SName (String a ""))
         end
      | SName s' => tokenize_go s k (SName (String a s'))
      | SPure s' => tokenize_go s k (SPure (String a s'))
      | SNat n =>
-        match is_nat a with
+        match Ascii.is_nat a with
         | Some n' => tokenize_go s k (SNat (n' + 10 * n))
         | None => tokenize_go s (TNat n :: k) (SName (String a ""))
         end
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 1f33c430b902687991ed0f66a0aa802ad994ac37..5fd51ed3798e3bf4a136f7792aa51fc05f233c90 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -737,7 +737,7 @@ Tactic Notation "awp_apply" open_constr(lem) :=
   last iAuIntro.
 Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
   (* Convert "list of hypothesis" into specialization pattern. *)
-  let Hs := words Hs in
+  let Hs := String.words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   wp_apply_core lem
     ltac:(fun H =>