Skip to content

Fix bug in hint for `AsIdentName` when term is not a lambda.

Robbert Krebbers requested to merge robbert/as_ident_name_fix into master

The following fails with current Iris:

Lemma test_iIntros_pure_forall `{!BiPureForall PROP} (φ : nat → Prop) :
  (∀ x, ⌜ φ x ⌝) ⊢@{PROP} ⌜ ∀ x, φ x ⌝.
Proof.
  iIntros "H".
  iIntros (x). (* fail *)

It tries to look for an instance AsIdentName φ ?name, where φ is a variable and not a lambda. It appears the corresponding case in solve_as_ident_name is broken. I tried to fix it.

@tchajed Since you wrote the initial code, could you review?

Merge request reports