I'm working on partial PGIP support Coq, and one thing that I would like
to support is the case when Coq outputs "warning" messages, of which
there are many but which are nonfatal. I'm wondering what the right
tag for these are. <errorresponse> is not correct, because we're only
allowed to have one before <ready/>. Is <metainforesponse> correct?
It seems too generic, and where am I supposed to attach other metadata?
ProofGeneral-devel mailing list