Regression of iFrame (with BiAffine and <absorb> _)
@janno and I noticed a change of behaviour of the iFrame
tactic that is better illustrated by the following code.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Goal forall (PROP : bi) (H_PROP : BiAffine PROP) (P Q : PROP),
<absorb> P ∗ Q ⊢ <absorb> (P ∗ Q).
Proof.
iIntros (?? P Q) "[P Q]".
Fail Fail iFrame "Q".
(* The following used to work. *)
Fail iFrame "Q"; iFrame "P".
Fail iFrame "Q P".
Fail Fail by iSplitR "Q".
Fail Fail by iSplitL "P".
Abort.
The failures were noticed using Iris version dev.2022-09-29.0.b335afaf
, and they did not happen with version dev.2022-05-04.0.10e843d9
. I suspect this is related to !838 (merged) (cc @robbertkrebbers), but I did not bisect.