subject:"\[PG\-devel\] Trace, thms buffers"

Re: [PG-devel] Trace, thms buffers

2017-02-02 Thread Pierre Courtieu

I don't think it is used. P. 2017-02-01 17:50 GMT+01:00 Paul A. Steckler : > thms ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

[PG-devel] Trace, thms buffers

2017-02-01 Thread Paul A. Steckler

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