Skip to content

Use user-supplied names in iIntros

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

Preserve identifiers in binders where possible, analogous to the support for destructing existentials in !479 (merged). This works for both iIntros (?) and iIntros "%". Note that the proof mode already handled Coq-level foralls correctly; this change only affects the Iris-level ∀.

Fixes #336 (closed).

Merge request reports