Joshua Grosso (Nov 29 2021 at 23:51): 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?
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
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.
Joshua Grosso (Nov 30 2021 at 00:00):Gotcha, I'll try to work on an MVCE.
Joshua Grosso (Nov 30 2021 at 00:11):Ah, I had defined my own notation for ; which was conflicting with Equations.
Joshua Grosso (Nov 30 2021 at 00:12):(and now I can't seem to replicate the fixproto error)
Karl Palmskog (Nov 30 2021 at 00:13):ah, isn't the standard recommendation to use ;; or something? (in own notations)
Joshua Grosso (Nov 30 2021 at 00:20):that sounds reasonable, I'll use that instead; thanks!
Joshua Grosso (Nov 30 2021 at 00:30):Everything works now :smile:
Notification Bot (Nov 30 2021 at 00:30):Joshua Grosso has marked this topic as resolved.
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: Sep 28 2023 at 10:01 UTC