Skip to content

Add support for pure names in intro patterns

Tej Chajed requested to merge tchajed/iris-coq:gallina-names into master

Notably this support relies on string to identifier conversion, which works natively using Ltac2 in Coq 8.11+ and with a plugin ( in Coq 8.10. To use it, you must replace intro_patterns.string_to_ident_binder with a real implementation; see string_ident.v for an Ltac2 implementation and enable_pure_names.v for how to install it.

The syntax is %H (within a string intro pattern). This is technically backwards-incompatible, because this was previously supported and parsed as % and H separately. To restore the old behavior, separate with a space, eg [% H].

Fixes #88 (closed)

Edited by Ralf Jung

Merge request reports