Confusing error message if iLoeb is not available (non-step indexed BI)
Example code:
From iris.proofmode Require Import tactics.
Lemma test `{PROP : bi} (k : nat) (Φ : nat → PROP) :
Φ k -∗ Φ (S k).
Proof.
iLöb as "IH".
(PROP should have type sbi
)
Error message:
In nested Ltac calls to "iLöb as (constr)", "iLöbRevert (constr) with (tactic3)",
"iRevertIntros (constr) with (tactic3)", "go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
"∗" with tac), "iRevertIntros (constr) with (tactic3)",
"go" (bound to
fun Hs =>
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end), "tac" (bound to iLöbCore as IH), "tac" (bound to iLöbCore as IH),
"iLöbCore as (constr)" and "notypeclasses refine (uconstr)", last call failed.
In environment
PROP : bi
k : nat
Φ : nat → PROP
The term "coq_tactics.tac_löb ?Δ "IH" ?Q ?e ?y" has type
"environments.envs_entails ?Δ ?Q" while it is expected to have type
"--------------------------------------∗
Φ k -∗ Φ (S k)
".
I don't know if it is even possible, but it would be nice to detect this error and emit a nicer message.