Querying module definitions

[dkhalansky]

Hi! Is there a way to get sexp-formatted information about modules, like the one acquired by running Print Coq.Init.Datatypes in Vernac? I failed to find a way, and running several commands like (Query () (Definition Coq.Init.Datatypes)) yielded no results.

[ejgallego]

Sure it should be possible to do so; I will prepare a patch later this week, or you could try to give it a go, if you look at the code in serapi_protocol and the code handling Print in Coq you should be able to follow a similar path.

Indeed, thanks to recent work we should be able to output a faithful representation of a module.