Tej Chajed authored Jul 21, 2020 and Ralf Jung committed Mar 24, 2021

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
does not handle this use case.

Tej Chajed authored Mar 23, 2021 and Ralf Jung committed Mar 23, 2021

Fixes #404

This is an alternative to !591.

This reverts merge request !591

Tej Chajed authored Dec 01, 2020 and Robbert Krebbers committed Dec 01, 2020

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