var=foo is a "recursive variable assignment", which is expanded on every
use (including re-running shell commands). What we really want is
var:=foo, which is expanded at definition time.

Generalize the type of gmap_equivI.

See merge request iris/iris!495

Bump std++

See merge request iris/iris!494

do not eta-expand when sealing

Closes #285

See merge request iris/iris!490

Drop support for Coq 8.9

Closes #318

See merge request iris/iris!489

Set default name for unnamed binders to H

Closes #337

See merge request iris/iris!484

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

Fixes #337.

Use user-supplied names in iIntros

Closes #336

See merge request iris/iris!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 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`.