Missing conversion functions for types for the extraction plugin? about coq-serapi HOT 3 CLOSED

Hi @toku-sa-n !

Absolutely, a PR to fix this problem would be much welcome! I'd recommend you also add a test to the test suite.

Unfortunately we cannot do this automatically yet, see ejgallego/coq-lsp#761 for a discussion

from coq-serapi.

I may be missing something, but it seems that we need to modify the upstream Coq code to implement the functions because there are neither wit_* functions defined in Extraction_plugin nor types of 'a Genarg.genarg_type defined there. The G_extraction module where I think such functions are to be defined is empty.

Is it correct?

from coq-serapi.

This is because the extraction.mli file was added. Because of that, it is now not possible to access the AST of extraction commands.

cc @SkySkimmer (coq/coq@99eae36)

from coq-serapi.