Merge branch 'fix-string-ident-clear' into 'master'

Fix string_to_ident when ident is not fresh

See merge request iris/iris!667

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.

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

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.