Skip to content

Provide functionality from string_ident natively

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

Adds support for the "%H" intro pattern without the need to install https://gitlab.mpi-sws.org/iris/string-ident.

I left the hook and make_string_ident_hook alone so that even the current version of https://gitlab.mpi-sws.org/iris/string-ident will work, but setting the hook doesn't do anything. Users can simply uninstall string-ident at their leisure, or use it with any older versions of Iris.

Fixes #404 (closed)

Edited by Tej Chajed

Merge request reports