Make string-ident a standard part of Iris
Since support for Coq 8.10 has been dropped for a while now and 8.11 is required, the string-ident plugin could be integrated into Iris master so that the named %H intro pattern becomes available in the IPM by default.
Mainly, this would have the benefits of
- not having to explicitly require the user to install the plugin in developments using Iris,
- and thus be beneficial to overall code quality of developments using Iris (since there would be a clear argument for using the new intro pattern instead of using auto-generated names).
@jung suggested I create an issue for this.