Skip to content

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).