Emilio Jesús Gallego Arias

Indeed compat is a problem, but this particular change should be easy to backport to 8.11 ; I'd be happy to take a PR for that branch.

Yup, it is not possible as of today, parse does call the non terminal for commands. It'd be easy to implement that as a parameter, so indeed we could provide...

There is a plan to handle those properly, and some people have been already waiting for an embarrassing amount of time for me to finish the work :/ I hope...

Hi @cpitclaudel , > I can almost get this information with SerAPI If I ask for CoqSer output (it gives me fully qualified names, which is great). But CoqSer results...

Oh, I see, actually the output here has qualids, because this is an AST synthethized from kernel terms; this also means that unfortunately locations are missing; I wonder how to...

Hi @vsiles , that's a tricky question; indeed it may be doable but there are several approaches: - you could consider this a duplicate of ejgallego/coq-lsp#331 , so we could...

The main blocker for ejgallego/coq-lsp#331 was actually designing a flexible protocol so "internalization" [the part of the elaboration that deals with notations] would be available in some contexts. A really...

> Does that ring any bell ? Umm, it seems you are using an incomplete build? Does it work if you do `dune build` before?

Also, I recommend you place the functions in a separate module from the beginning.

You need to run `sercomp` with the proper ocaml env, dune provides `dune exec -- ` for that purpose, see SerAPIs FAQ: https://github.com/ejgallego/coq-serapi/blob/v8.11/FAQ.md#i-get-an-error-cannot-link-ml-object- and https://github.com/ejgallego/coq-serapi/blob/v8.11/notes/build.md#executing-built-binaries