Regression from !931 : applying some lemmas in iIntros using intro patterns breaks
When porting DimSum to !931 (merged), I encountered a regression with the n-ary iTactics MR: The following code used to work, but now it gives an error "Error: Tactic failure: iStartProof: not a BI assertion.":
From iris.base_logic Require Export iprop.
From iris.proofmode Require Export tactics.
Lemma test {Σ} (m : gmap nat nat) i x :
⊢@{iProp Σ} ⌜kmap (M2 :=gmap nat) id m !! i = Some x⌝ → True.
Proof. iStartProof. iIntros (?%lookup_kmap_Some).
My suspicion is that this has to do with the Inj
argument of lookup_kmap_Some
and that some pure subgoal gets created for it where iIntros
then fails.
The following variant works
From iris.base_logic Require Export iprop.
From iris.proofmode Require Export tactics.
Lemma test {Σ} (m : gmap nat nat) i x :
⊢@{iProp Σ} ⌜kmap (M2 :=gmap nat) id m !! i = Some x⌝ → True.
Proof. iStartProof. iIntros (?%(lookup_kmap_Some _)).