Support destructing exists with intro patterns
The syntax re-uses the existing support for pure names, namely the % and
%H patterns. Using "[% H]" is like iDestruct ... as (?) "H" and using
"[%x H]" (with the string-ident plugin) is like iDestruct ... as (x) "H".
This changes how these patterns are parsed. Previously, both would have been handled as conjunctions (using IntoAnd or IntoSep, depending on whether the hypothesis is persistent or not). This means it was possible for the user to use "[% H]" to destruct a pure hypothesis ⌜φ ∧ ψ⌝ and put only the first conjunct in the Gallina context, leaving the other one in the IPM; such patterns will now break, since iExistDestruct cannot handle this use case.
As a probably-mostly-complete solution, this MR special-cases "[% %]" (and similar patterns that name the hypotheses) to continue to use iAndDestruct, since most likely this would be the pattern used in existing code and not the unusual asymmetric "[% H]".
If we work this out it would fix #310 (closed) without new syntax.