Emilio Jesús Gallego Arias

> Would that be easy? That's easy, as CoqMakefile already has a list of "forbidden" modules. However, you get a different problem, and it is that now Coq will fail...

Should be fixed upstream by https://github.com/coq/coq/pull/15220

Umm, I am not sure there is a notion of "parent" goal, I guess tho we could indeed expose the `evar_map` and you could determine the partial order of evar...

Ok, #20 is addressed in #256 , so indeed, I think my strategy may work, tho not sure what would be the output data structure for you to consume @cpitclaudel

> @ejgallego how do you see the future for sertop and its sibling tools? My reading is that if serlib is upstreamed into Coq itself, serapi and sertop could take...

`serapi` is just an OCaml library, you mean that? Sure, we could do that very easily if we have a need.

Sounds good, I'd be happy to do the split if there is a need.

Only problem is that the package name for `coq-serapi` would conflict with the current one, suddenly, users wouldn't get `sertop` after doing `opam install coq-serapi`; IMHO that's a problem.

Actually `sertop` is just a very thin shell over the serapi protocol, so indeed I shall correct my description on the issue. It is `sercomp` and friends who are independent,...

Indeed, `print` mode relies on Coq printer; this means that for example the code may not parse back and formatting will almost likely be different. We could try to preserve...