This is an alternative to !591.

This reverts merge request !591

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

`iDestruct ("H" with "HP")` where "H" is persistent is supposed to
consume "H" if it isn't a forall. Due to a bug in the tactic, this
behavior was never triggered and "H" was always left alone.

This test is incompatible with Coq 8.8 and Coq 8.9, but Iris no longer
supports those versions.

put it into a type class `BiPureForall`.

This property does not hold for embeddings of classical logic into Coq.

A failing iIntros for implications should prettify the identifier before
printing, and iIntros on something that isn't a wand or implication
should say what couldn't be introduced (to clarify that `iIntros "HP
HQ"` failed because of the HQ in particular, for example).

`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).

The error handling for `iIntro (?)` and similar tactics didn't correctly
report failures when the goal couldn't be turned into a universal
quantifier. This is something missing from !482 due to no test
triggering the error.

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

Fixes #337.

Preserve identifiers in binders where possible, analogous to the support
for destructing existentials in !479.

Fixes #336.