Merged requested to merge tchajed/iris-coq:fix-destruct-multiple-pats into master
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).