diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 0265d3c4bf643d769cd11eb86ee99912d48b22e1..600951aab25427f6d6a276a0872ccf7134565fe0 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -85,3 +85,13 @@ Only works if [id] can be reverted, i.e. if nothing else depends on it. *)
 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:(StringToIdent.intros_by_string s; exact tt) : unit -> unit) in
+  match x with
+  | (fun (name:_) => _) => name
+  end.