Tej Chajed authored and Robbert Krebbers committed
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`.7d0bb151
To find the state of this project's repository at the time of any of these versions, check out the tags.