Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 23
    • Merge requests 23
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #260
Closed
Open
Issue created Aug 09, 2019 by Dan Frumin@dfruminContributor

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.

Assignee
Assign to
Time tracking