base_logic/lib/gset_bij: fix gset_bij_own_elem_agree; add gset_bij_own_elem_auth_agree

See merge request iris/iris!663

Fix string_to_ident when ident is not fresh

See merge request iris/iris!667

Add more lemmas for wand_iff and iff

See merge request iris/iris!666

Add included lemmas for frac_agree

See merge request !665

different approach for string_to_ident that works with name mangling

Closes #343

See merge request !660

Add CoreId instances for auth and view

See merge request !664

drop support for Coq 8.11

See merge request iris/iris!657

fix IntoAnd/IntoSep docs

See merge request iris/iris!659

Support destructing exists with intro patterns

Closes #310

See merge request !658

This note is obsolete due to iris/iris!640

generalize into_and_sep_affine so that generalizing just the conjunction instance for IntoExist is sufficient

Tej Chajed authored 4 years ago and Ralf Jung committed 3 years ago

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.