We have extended Proof General interface with a new functionality that
allows one to statistically analyse various patterns arising in Coq/SSReflect
proofs. Finding common patterns in proofs may be used as a guidance in big proof
developments across different users, as well as for educational/training
We have successfully tested it on several examples and libraries,
and are now looking for more users!
The tool will not alter your normal ProofGeneral routines --
but you will notice ProofGeneral will feature an extra option for
More information can be found here:
We will be happy to hear your feedback.
Jónathan Heras and Katya Komendantskaya
The University of Dundee is a Scottish Registered Charity, No. SC015096.
ProofGeneral mailing list