From 57e813e6d569de033a1fb3e91d876c07edcd1473 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Apr 2021 18:07:56 +0200
Subject: [PATCH] add back a version of string_to_ident

---
 iris/proofmode/string_ident.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 0265d3c4b..600951aab 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.
-- 
GitLab