From 20d74b17988d89a10799062737b8ba001b9a67e2 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Wed, 14 Apr 2021 12:57:06 +0000
Subject: [PATCH] Fix string_to_ident when ident is not fresh
---
iris/proofmode/string_ident.v | 5 ++++-
tests/string_ident.ref | 2 ++
tests/string_ident.v | 10 ++++++++++
3 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 600951aab..594bd361a 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -91,7 +91,10 @@ 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
+ 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.
diff --git a/tests/string_ident.ref b/tests/string_ident.ref
index 8486db4a4..3ea77a67e 100644
--- a/tests/string_ident.ref
+++ b/tests/string_ident.ref
@@ -10,3 +10,5 @@ Uncaught Ltac2 exception: StringToIdent.NotStringLiteral (constr:(4))
: string
The command has indeed failed with message:
Uncaught Ltac2 exception: StringToIdent.NotStringLiteral (constr:(s))
+"test_string_to_ident_not_fresh"
+ : string
diff --git a/tests/string_ident.v b/tests/string_ident.v
index bc42e0106..6de14c131 100644
--- a/tests/string_ident.v
+++ b/tests/string_ident.v
@@ -26,3 +26,13 @@ Lemma test_not_literal (s:string) : ∀ (n:nat), True.
Proof.
Fail let x := fresh in intros x; rename_by_string x s.
Abort.
+
+Check "test_string_to_ident_not_fresh".
+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
+ let x := fresh x in
+ intros x.
+Abort.
--
GitLab