Regression from !931 : iRevert used by iInduction is broken
When porting RefinedC to !931 (merged), I noticed that the following code now gives the error Error: Tactic failure: iRevert: l2 is used in hypothesis "Himpl".
, while it used to work before:
From iris.algebra Require Export big_op.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Lemma big_sepL_impl' (PROP:bi) {A B} Φ (Ψ : _ → B → PROP) (l1 : list A) (l2 : list B) :
□ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
[∗ list] k↦x ∈ l2, Ψ k x.
Proof.
iIntros "#Himpl".
iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2).
A workaround seems to be to keep Himpl
in the spatial context.
EDIT: The following code was always broken as noticed by Robbert:
From iris.algebra Require Export big_op.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Lemma big_sepL_impl' {PROP : bi} {A B} (l1 : list A) (l2 : list B) :
⊢@{PROP} □ (∀ k x2, ⌜l2 !! k = Some x2⌝ -∗ True) -∗
True.
Proof. iIntros "#Himpl". iInduction l1 as [|x1 l1] "IH" forall (l2).