From 492d5a9a508985b41dcfc998fe06c7b54872cf62 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 2 May 2023 20:24:29 +0200
Subject: [PATCH] remove the super hacky non-CPS version of string_to_ident

---
 iris/proofmode/string_ident.v | 14 ++------------
 tests/string_ident.v          |  4 ++--
 2 files changed, 4 insertions(+), 14 deletions(-)

diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 7e79a33c3..422ca913e 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -80,15 +80,5 @@ by ident [id] into the name given by string [s]. *)
 Ltac rename_by_string id s :=
   StringToIdent.string_to_ident_cps s ltac:(fun x => rename id into x).
 
-(** 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.string_to_ident_cps s ltac:(fun x => intros x);
-                         exact tt) : unit -> unit) in
-  match x with
-  | (fun (name:_) => _) => name
-  end.
+(* 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 dc22df6de..5313a51b8 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.
-- 
GitLab