Skip to content

Prefix iDestruct automatic names with an underscore

Tej Chajed requested to merge tchajed/iris-coq:prefix-automatic-names into master

Avoids conflicts with user-provided names while still giving existential witnesses meaningful names for readability (which can be used if desired).

Fixes incompatibility coming from !479 (merged) where automatic names required the user to change their choice of manually-written names, even if they weren't referring the automatic names at all.

Edited by Tej Chajed

Merge request reports