rename_by_string: avoid revert-intros hack

Using Ltac1.of_ident we can at least avoid doing this revert-intros dance (that even shows up in the proof term!) for variables named by strings..

Unfortunately I found no way to return a value from Ltac2 to Ltac1, so we have to write this in CPS. This means that string_to_ident remains a hack. It is not used in Iris itself but is used in iris-named-props. @tchajed I wonder if the CPS API would be good enough for iris-named-props, so that we could get rid of the string_to_ident hack?