Dear all,

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
Proof Statistics.

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

Reply via email to