Bump std++

See merge request !494

do not eta-expand when sealing

Closes #285

See merge request !490

Drop support for Coq 8.9

Closes #318

See merge request !489

Set default name for unnamed binders to H

Closes #337

See merge request !484

Tej Chajed authored Jul 22, 2020 and Robbert Krebbers committed Jul 22, 2020

Fixes #337.

Use user-supplied names in iIntros

Closes #336

See merge request !482

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

Fixes #336.

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

See merge request !479

Tej Chajed authored Jul 21, 2020 and Robbert Krebbers committed Jul 21, 2020

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 !475

Tej Chajed authored Jul 15, 2020 and Robbert Krebbers committed Jul 15, 2020

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