Confusing error message from iLoeb: `Variable x should be bound to a term but is bound to a ident.`
Example code:
From iris.proofmode Require Import tactics.
Lemma test `{PROP : sbi} (k : nat) (Φ : nat → PROP) :
Φ k -∗ Φ (S k).
Proof.
iLöb as "IH" forall (k1).
(notice that k1
should be k
in the forall
clause)
It fails with a cryptic message:
Error:
In nested Ltac calls to "iLöb as (constr) forall ( (ident) )",
"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 iRevertIntros ( x1 ) "" with iLöbCore as IH),
"tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as IH),
"iRevertIntros ( (ident) ) (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 iRevert ( x1 ); tac; iIntros ( x1 )),
"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )), "iRevert ( (ident) )",
"iForallRevert (ident)" and "x" (with IH:="IH", Hs:=""), last term evaluation
failed.
Variable x should be bound to a term but is bound to a ident.
What's bit strange is that the identifier x
is not used in the code.