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. Clément.
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
