Hi,

I am experiencing the following error with Coq 8.19 + coq-ext lib + coq-equations.

The no so minimum reproducer is available here https://gist.github.com/jjhugues/6747d65e38a99ed85db35ad4565b0fe6

```
Error: Anomaly
"File "kernel/cClosure.ml", line 134, characters 26-32: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
```

This code is reduced from https://github.com/ConorReynolds/coq-institutions, 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.

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: https://github.com/mattam82/Coq-Equations/issues

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

Last updated: Jun 13 2024 at 19:02 UTC