Missing conversion functions for types for the extraction plugin?

[toku-sa-n]

Hi. While I was viewing serlib's document, I noticed that functions for converting between types for the extraction plugin (e.g., lang) and SExp were missing.

Is it okay to send a PR to implement them?

[ejgallego]

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

[toku-sa-n]

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?

[ejgallego]

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@99eae36202cef321745355976a257e8332f0b82e)