Skip to content
Snippets Groups Projects
Forked from Iris / Iris
Source project has a limited visibility.
  • Tej Chajed's avatar
    84144f00
    Fix error when destructing as multiple pats · 84144f00
    Tej Chajed authored
    `iDestruct H as "H1 H2"` produces an error that says the pattern should
    contain exactly one proper introduction pattern. When multiple patterns
    are provided, due to Ltac variable shadowing iDestructHypFindPat was
    instead reporting only the first pattern in the error message (and even
    that was printed as the parsed AST rather than the original string).
    84144f00
    History
    Fix error when destructing as multiple pats
    Tej Chajed authored
    `iDestruct H as "H1 H2"` produces an error that says the pattern should
    contain exactly one proper introduction pattern. When multiple patterns
    are provided, due to Ltac variable shadowing iDestructHypFindPat was
    instead reporting only the first pattern in the error message (and even
    that was printed as the parsed AST rather than the original string).