GitLab

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.