Regression of [iSpecialize] and related tactics.
I noticed the following regression.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Goal forall (PROP : bi) (P Q : PROP), (∀ (_ : tt = tt), Q) ⊢@{PROP} P.
Proof.
iIntros (???) "H".
Fail iSpecialize ("H" with "[%]"). (* Used to work before, now fails with: *)
(* Tactic failure: iSpecialize: (Forall _ : () = (), Q) not an implication/wand. *)
(* Possible (and maybe even desired) alternative (probably also worked before): *)
unshelve iSpecialize ("H" $! _).
all: done.
Qed.
The first iSpecialize
pattern above was used to work with coq-iris.dev.2022-05-04.0.10e843d9
, and it fails with coq-iris.dev.2022-09-29.0.b335afaf
(and probably on master
. I also reported this in !799 (comment 85201), which I think introduced the regression (cc @jung).