More convenient destruct of pure hypotheses

It is currently pretty annoying to destruct things into the pure (Coq) context, because the assertions cannot be named. This should be fixed.

One somewhat hack-ish option would be to do this the ssreflect style. So iDestruct ... as "[% %]" would put two things onto the goal stack, and one would follow this tactic by =>H1 H2 to give them names. This is somewhat non-local, but OTOH it lets us use the full power of ssreflect intro patterns.

Another option would be to somehow solve the "cannot convert string to ident"-problem, and then support patterns of the form %H. This will require a plugin to work in Coq 8.6, which makes it really hard to support Windows (as far as I can tell). Also, I suppose currently %H is parsed just like % H? So there would be a backwards compatibility problem when % starts to behave like # (i.e., being a modifier on the following name). We could mitigate that by detecting uses of %H right now and warning about them (or erroring immediately?).