Emilio Jesús Gallego Arias

If you are using 8.8, the first thing is to upgrade to 8.9 as we solved half of the bug there.

A much more reliable way to get the AST is to use `sercomp` [in 8.9 too]

I'd bet that has to do with people using "nested proofs" or weird effectul commands inside proofs. I can provide you a workaround tho if you want to keep using...

Ok, see https://github.com/ejgallego/coq-serapi/commit/337f9b6ebe3da6a8dcf7f96e9e7d826242689b53 The command is very limited [see commit message] but it may help in your case.

It is the input to the parser, you can indeed pass any valid Coq input, it doesn't have to be the same. Note however the limitation with ontop, it has...

`Parse` is indeed still a workaround. The problem you point out still exists, unfortunately there is not a lot we can do in SerAPI as this is a bug in...

Hi @erikmd , sorry for the lag with this. Indeed it seems to me that the right solution is to add the upper bound. I'll update the branches here when...

I reopen as I need to update the opam files here, thanks a lot @erikmd

Hi @affeldt-aist , thanks for the report. This is a big problem indeed, it is due to the HB plugin using -linkall, which has been forbidden since OCaml 4.08 ....

Another solution is to use OCaml