Stream: Equations devs & users

Topic: ✔ coq-equations "not found in table: equations.fixproto"


view this post on Zulip Joshua Grosso (Nov 29 2021 at 23:51):

If Equations gives me Error: not found in table: equations.fixproto, what would be a good first troubleshooting step?

view this post on Zulip Notification Bot (Nov 29 2021 at 23:51):

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

view this post on Zulip Karl Palmskog (Nov 29 2021 at 23:54):

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.

view this post on Zulip Joshua Grosso (Nov 30 2021 at 00:00):

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

view this post on Zulip Joshua Grosso (Nov 30 2021 at 00:11):

Ah, I had defined my own notation for ; which was conflicting with Equations.

view this post on Zulip Joshua Grosso (Nov 30 2021 at 00:12):

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

view this post on Zulip Karl Palmskog (Nov 30 2021 at 00:13):

ah, isn't the standard recommendation to use ;; or something? (in own notations)

view this post on Zulip Joshua Grosso (Nov 30 2021 at 00:20):

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

view this post on Zulip Joshua Grosso (Nov 30 2021 at 00:30):

Everything works now :smile:

view this post on Zulip Notification Bot (Nov 30 2021 at 00:30):

Joshua Grosso has marked this topic as resolved.

view this post on Zulip Matthieu Sozeau (Nov 30 2021 at 18:51):

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


Last updated: Jan 29 2023 at 15:02 UTC