Emilio Jesús Gallego Arias

It would be cool if LSP natively provided us with hints for this, as well as for cursor position. Maybe worth opening an issue upstream?

Genargs are very special objects and handled by SerAPI in a special way too. Maybe we can do better, but we'll need to look into it. See `ser_genarg`.

That's a reasonable feature request, however note that it would require to extend CoqObject. You can indeed use the `CoqAst` object to print sub-asts , but you'll need to do...

The input type here is `gen_tactic_expr`, not `gen_tactic_expr_r` which is the one you are pointing out to.

This indeed needs to be fixed, it is showing the current goal which of course it just a hole waiting to be filled.

It shouldn't be hard to extend indeed, you can call `Proof.partial_proof` to return the term, which can just then be serialized normally. I've implemented that in #271, please let me...

I need to find out where my writing about Coq ASTs is, but indeed: - proofs are represented using "kernel terms" - documents are represented using "CoqAst" which is a...

That's the correct syntax sorry `opam pin add coq-serapi https://github.com/ejgallego/coq-serapi.git#v8.16+show_proof`

Pinning does not force the right Coq version, it seems. For that tree you need to install `coq.8.16` at least.

And the rest of deps, I'd suggest you first install coq-serapi 0.16 , and then pin.