Re: [PG-devel] Trace, thms buffers

[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

[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
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel