Forked from
Iris / Iris
Source project has a limited visibility.
-
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).
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).