Stream: Coq users

Topic: Coq 8.19 -- assert failure in "kernel/"

view this post on Zulip Jerome Hugues (Feb 21 2024 at 23:41):


I am experiencing the following error with Coq 8.19 + coq-ext lib + coq-equations.
The no so minimum reproducer is available here

Error: Anomaly
"File "kernel/", line 134, characters 26-32: Assertion failed."
Please report at

This code is reduced from, it embeds the minimum set of definitions that trigger the issue.

Since the offending code is a coq kernel error, and also involves coq equation, I wonder where to submit it. Should it be a coq issue or a coq-equations one?

I would prefer to submit a smaller reproducer, yet I do not know how to start.

Thanks for your guidance.

view this post on Zulip Karl Palmskog (Feb 22 2024 at 08:25):

based on seeing many earlier issues of a similar flavor, it's very likely this is caused by Equations, e.g., by some bug in Equations. You may want to report a minimized example as an issue, or look if someone has already reported:

view this post on Zulip Karl Palmskog (Feb 22 2024 at 08:37):

arguably the "standard approach" to obtaining minimized examples is using coq-bug-minimizer

Last updated: Jun 13 2024 at 19:02 UTC