On 2017-02-23 17:14, Paul A. Steckler wrote:
> That procedure creates a daughter span with a context menu. In
> vanilla PG, it looks like the context menu also contains the last
> response from Coq.

I use it from time to time; I think that's also what PG-movie is based on, 
though I don't think anyone really uses that.

> In PG/xml, that's not so useful, since the last response is an XML
> blob.

True, but doesn't that XML usually contain what the old PG would have called 
the "last response"? It would be either a message or a goal.


Attachment: signature.asc
Description: OpenPGP digital signature

ProofGeneral-devel mailing list

Reply via email to