Crash with Coq 8.19 - Githubissues

mattam82 / Coq-Equations

A function definition package for Coq

http://mattam82.github.io/Coq-Equations

GNU Lesser General Public License v2.1

223 stars 44 forks source link

Crash with Coq 8.19 #583

Open jjhugues opened 8 months ago

jjhugues commented 8 months ago

Hi,

The code at https://gist.github.com/jjhugues/6747d65e38a99ed85db35ad4565b0fe6 is a minimized version of a larger development.

Testing with Coq 8.19 + Coq Equations triggers the following error

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

Is there any workaround to this type of issue? Thanks,