Use user-supplied names when destructing existentials with ? intro pattern

See merge request iris/iris!479

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

When running `iDestruct "H" as (?) "H"`, use the name of the binder in
"H". For example, if "H" has type `∃ y, Φ y`,  we now use `y` as the
name of the variable after freshening. Previously the name was always
the equivalent of running `fresh H`.

The implementation achieves this by forwarding the desired identifier
name through the `IntoExist` typeclass. Identifiers are serialized in
Gallina by using them as the name of a function of type `ident_name :=
unit -> unit`.

Port HeapLang tactics to efficient style

Closes #315

See merge request iris/iris!475

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

Addresses #315 for several tactics (`wp_alloc`, `wp_load`, `wp_store`,
`wp_free`).

Iris 3.3 changelog summary

See merge request iris/iris!478

Remove dec_agree and cofeT and use Coq #[deprecated] attribute for iAlways

Closes #296

See merge request iris/iris!477

mention that the ASCII syntax exists (but we recommend unicode)

See merge request iris/iris!470

All list "map singleton" lemmas consistently use `singletonM` in their name

Closes #309

See merge request iris/iris!476

LICENSE-CODE: Clarify which BSD license is being used

See merge request iris/iris!472

Mention change to lemmas in changelog

See merge request iris/iris!469