I'm doing some code cleanup on my PG/xml branch. Are the trace and thms buffers used at all for Coq? The thms buffer is not even mentioned in the PG manual.
-- Paul _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
