Skip to content
  • Tej Chajed's avatar
    Add support for pure names in intro patterns · 1375d6aa
    Tej Chajed authored
    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_hook with a real
    implementation; see for a
    working implementation that works with Coq 8.11 (using Ltac2).
    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].