Emilio Jesús Gallego Arias

I think `import pycoq` is needed so the .so file with the `coq` module is loaded?

Indeed, this is an artifact of of the way ppx_python works, for OCaml objects of the from `Cons of t1 * t2` there is little choice but to return a...

For now we should indeed consider the interface low-level, and expose to users a better, typed-API

@Zimmi48 , I'll be happy to provide a NiX derivation for SerAPI. How is Coq installed with NiX ?

@Zimmi48 ok, I'll add Nix support when Coq 8.6 makes into Nix.

For the shorter term, doing `opam install coq-serapi` will be working very soon.

It should be "fairly easy", I am a bit busy right now but I would start from already existing projects that do similar things; basically you do a traversal on...

Actually ppx is not even needed, we just a program that uses compiler-libs. Then, the basic scheme is very simple IMO: ```ocaml let ast = Parse.interface foo in let typ_list...

Hey congrats @Ptival !! I guess you'll have way better things to do than to hack OCaml. Anyways I actually wrote already a very small shim, find it here at...

Maybe something to think about is that if removing failing commands is needed anymore in a model like the one in `coq-lsp`/`fcc`. There, if a command fails, it is just...