diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8df954bc5712d8e07e707d645e553faedd6958c5..cd33b885352b49fd6cd69575593aa2b1d33623f3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -94,13 +94,15 @@ Coq 8.13 is no longer supported.
   `CombineSepGives` typeclass. The 'gives' clause is still experimental;
   in future versions of Iris it will combine `own` connectives based on the
   validity rules for cameras.
-- Make sure that `iStartProof` fails with a proper error message on goals with
+* Make sure that `iStartProof` fails with a proper error message on goals with
   `let`. These `let`s should either be `simpl`ed or introduced into the Coq
   context using `intros x`, `iIntros (x)`, or `iIntros "%x"`.
   This can break some proofs that did `iIntros "?"` on a goal of the shape
   `let ... in P ⊢ Q`.
-- Make `iApply`/`iPoseProof`/`iDestruct` more reliable for lemmas whose
+* Make `iApply`/`iPoseProof`/`iDestruct` more reliable for lemmas whose
   statement involves `let`.
+* Remove `string_to_ident`; use `string_to_ident_cps` instead which is in CPS
+  form and hence does not require awful hacks.
 
 **Changes in `base_logic`:**
 
diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 6bdb66392a700cc0506bbee72163a249e608b458..422ca913e27a347d532e8c1a9106d49bfe2f064f 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -63,36 +63,22 @@ Module StringToIdent.
   (** [coq_string_to_ident] implements the ident to string conversion in Ltac2 *)
   Ltac2 coq_string_to_ident (s : constr) := ident_from_string (coq_string_to_string s).
 
-  (** We want to wrap this in an Ltac1 API, which requires passing a string to
-      Ltac2 and then performing an intros.
-      TODO: Once we require Coq 8.14, we should be able to pass idents across
-      the Ltac/Ltac2 barrier, which can be used to avoid the revert/intros.
+  (** We want to wrap this in an Ltac1 API, but Ltac1-2 FFI does not support
+      returning values from Ltac2 to Ltac1. So we wrute this in CPS instead.
    *)
 
   Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.
 
-  Ltac intros_by_string :=
-    ltac2:(s1 |- let s := get_opt (Ltac1.to_constr s1) in
-                 let ident := coq_string_to_ident s in
-                 intros $ident).
+  Ltac string_to_ident_cps :=
+    ltac2:(s1 r |- let s := get_opt (Ltac1.to_constr s1) in
+                   let ident := coq_string_to_ident s in
+                   Ltac1.apply r [Ltac1.of_ident ident] Ltac1.run).
 End StringToIdent.
 
 (** Finally we wrap everything up intro a tactic that renames a variable given
-by ident [id] into the name given by string [s].
-Only works if [id] can be reverted, i.e. if nothing else depends on it. *)
+by ident [id] into the name given by string [s]. *)
 Ltac rename_by_string id s :=
-  revert id;
-  StringToIdent.intros_by_string s.
-
-(** We can also use this to write Ltac that *returns* the desired ident.
-However, this function will produce wrong results under [Set Mangle Names], so
-use with caution. *)
-Ltac string_to_ident s :=
-  let s := (eval cbv in s) in
-  let x := constr:(ltac:(clear; (* needed since s might already be in scope
-                         where this is called *)
-                         StringToIdent.intros_by_string s;
-                         exact tt) : unit -> unit) in
-  match x with
-  | (fun (name:_) => _) => name
-  end.
+  StringToIdent.string_to_ident_cps s ltac:(fun x => rename id into x).
+
+(* We also directly expose the CPS primitive. *)
+Ltac string_to_ident_cps := StringToIdent.string_to_ident_cps.
diff --git a/tests/string_ident.v b/tests/string_ident.v
index dc22df6de751ac4f66c2f003313a062f3ba7889c..5313a51b88d9d4c721e7594bfb4e817e84a28c5a 100644
--- a/tests/string_ident.v
+++ b/tests/string_ident.v
@@ -32,7 +32,7 @@ Lemma test_string_to_ident_not_fresh (n:nat) : ∀ (n:nat), nat.
 Proof.
   (* we want to check that this [string_to_ident "n"] call succeeds even with
   [n] in the context *)
-  let x := string_to_ident "n" in
+  string_to_ident_cps "n" ltac:(fun x =>
   let x := fresh x in
-  intros x.
+  intros x).
 Abort.