Quentin VERMANDE (Dec 05 2023 at 16:37): Quentin VERMANDE (Dec 05 2023 at 16:37):I need to load a clause for tc in order for coq.elaborate-skeleton to give the right answer, but when I do Clause => coq.elaborate-skeleton X Y ok, the clause never triggers. According to [at]Davide Fissore, this may be because the clause is loaded for coq.elaborate-skeleton but is not there when the elaborator calls the typeclass solver. Is there a way around this?
Enrico Tassi (Dec 05 2023 at 16:56):No. The diagnostic is correct, this is not supported.
I think you are pushing it a bit too far given the current mix of Coq and Elpi code.
Ideally, the elaborator would be an Elpi program an be merged with the TC and the coercions one, then what you are trying to do would work as you expect. The prototype elaborator part of the sources of Coq-Elpi is not yet ready to be used in conjunction with MathComp, although that is my dream.
Quentin VERMANDE (Dec 05 2023 at 16:57):Ok, thanks.
Notification Bot (Dec 05 2023 at 16:57):Quentin VERMANDE has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC