Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
FTR, coq/coq#15901 might be a good application of this feature request, although it is more about computational reflection rather than extraction.
> Better error messages (things like "Cannot find witness" are shown as debug messages, which is weird). To do error handling properly, we have to call a witness generator (like...
Hi @amahboubi, it seems that [you are using OPAM v1](https://stackoverflow.com/questions/50942323/opam-install-error-no-solution-found) (but then, there would be a problem with installing MathComp...). OPAM file generated by coq-community Templates requires OPAM 2.0 or...
Also, if your OPAM switch uses OCaml < 4.07.0, I suggest using OCaml >= 4.07.0. The latest available version of Coq-Elpi compatible with Coq 8.13.1 (coq-elpi.1.11.1) requires that. (Sorry for...
@amahboubi Could you try to upgrade coq-elpi to 1.11.1 by: ``` opam install coq-elpi.1.11.1 ``` and then try `opam install coq-mathcomp-algebra-tactics.0.1.0` again? (It may force you to remove Hierarchy Builder,...
> Let me know if you need more information. The output of `opam pin` would be useful if there is any.
mczify should also be 1.1.0. But, I expect there is no conflict with that.
Hmm, what about `opam upgrade elpi coq-elpi coq-hierarchy-builder`?
@amahboubi By following the same instruction, my OPAM (2.0.5 actually) could resolve dependencies. Did you run `opam show elpi`?
Also, did you run `opam update` recently?