Skip to content

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

Tej Chajed requested to merge tchajed/iris-coq:exists-auto-name into master

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.

Edited by Tej Chajed

Merge request reports