Skip to content

Fix string_to_ident when ident is not fresh

Tej Chajed requested to merge tchajed/iris-coq:fix-string-ident-clear into master

!660 (merged) re-implemented string_to_ident but doesn't do a clear in the tactic-in-term to make sure it handles an existing name.

Perennial is actually relying on string_to_ident rather than intros_by_string because the NamedProps.v library needs to freshen a name coming from a string, so I worked around this bug by re-implementing string_to_ident in Perennial.

Merge request reports