New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

`coq.ltac.call` fails with `Anomaly "Uncaught exception Not_found."` #436

Closed

pi8027 opened this issue Feb 28, 2023 · 0 comments · Fixed by #438

Contributor

pi8027 commented Feb 28, 2023 •

edited

Loading

Here is an example by @proux01 (I didn't double-check):

From elpi Require Export elpi.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

Ltac ltac_foo := idtac.

Elpi Tactic fail_foo.
Elpi Accumulate lp:{{

pred solve i:goal, o:list sealed-goal.
solve (goal _ _ _ _ [_] as G) GS :-
  coq.ltac.call "ltac_foo" [] G GS.

}}.
Elpi Typecheck.

Goal True.
Proof.
elpi fail_foo ([the Equality.type of unit : Type]).
Qed.

This is a blocking issue in releasing Algebra Tactics compatible with Coq 8.17.

pi8027 mentioned this issue

Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 math-comp/algebra-tactics#80

Closed

gares mentioned this issue

Fix bug affecting algebra tactics #438

Merged

gares closed this as completed in #438

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment