Emilio Jesús Gallego Arias

Added , c.f. https://github.com/ejgallego/coq-serapi/pull/236/files [Note the function was already there but unused, I got side-tracked sadly but indeed there were plans to expose it]

> I'm not sure what to make of this, given that I maintain https://github.com/JasonGross/coq-tools to be compatible with Coq all the way back to 8.5. (I dropped 8.4 when it...

As for this PR I guess the best tradeoff is to keep the Python code in a compat module, and use it if SerAPI < supported version, otherwise use the...

Now that I have hijacked the thread and we are talking about what the protocol can/should do I'd like to do a very brief update on what is the status...

> My solution to this was to run `coqtop -time -emacs` and let Coq parse things into sentences with character locations. And then I discovered even this is not perfect,...

> We could, but that's more maintenance and more debugging. I prefer to take a dependency on a more recent SerAPI. Sounds good, let me then review my org file...

> But indeed this is a case where sercomp is pretty nice. And much faster than `coqc` usually as it has a parsing-only mode.

Actually we have introduced another format for printing tailored to this kind of use cases, so it shouldn't be too hard, as long as you can encode your inductive definitions...

I'm working on a h̶a̶c̶k̶ fix for ejgallego/coq-lsp#330 , at least to the point that it will be useful for Alectryon ; I think that is a good moment to...

[The more principled way is actually a true database of Coq documents, but that will be available not too soon]