If Equations gives me `Error: not found in table: equations.fixproto`

, what would be a good first troubleshooting step?

This topic was moved here from #Coq users > coq-equations "not found in table: equations.fixproto" by Karl Palmskog

that's a pretty weird error, you may have to go the Equations author (Matthieu Sozeau) and ping him either here or open a GitHub issue (https://github.com/mattam82/Coq-Equations/issues). Unlikely that many other people have seen it. I guess also taking a look at OCaml sources of Equations might help.

Gotcha, I'll try to work on an MVCE.

Ah, I had defined my own notation for `;`

which was conflicting with `Equations`

.

(and now I can't seem to replicate the `fixproto`

error)

ah, isn't the standard recommendation to use `;;`

or something? (in own notations)

that sounds reasonable, I'll use that instead; thanks!

Everything works now :smile:

Joshua Grosso has marked this topic as resolved.

You were probably requiring some file from Equations after you Require Import Equations, which tends to mess up the constant registration

Last updated: Oct 13 2024 at 01:02 UTC