Skip to content

Draft: Make sure that `?` in `iIntros`/`iDestruct` generate names that are not in the pattern

Robbert Krebbers requested to merge robbert/iIntro_iDestruct_fresh into master

See where @jung wrote:

We have another behavior change from the ltac2 MR:

Lemma test_iDestruct1_pure (Φ: nat  PROP) :
  ( y z:nat, Φ y) -∗  x, Φ x.
  iDestruct 1 as (? y) "H".

this now fails because the ? gets name y and then the later y says that the name is already used. it used to work fine, presumably because intros ? y actually does some form of lookahead and avoids picking the name y when a later pattern uses that name?

This MR fixes this issue. Thanks to @snyke7 for the Ltac2 hackery.

Reasons for WIP:

  • iIntros "(% & %y & ?)" still fails on the same example. The problem is that we do not collect names from the Iris intro pattern. This should be simple to fix.
  • We need to figure out where to put and how to name the Ltac2 stuff.

Merge request reports