Ssreflect Users Discussion List

["JÓNATAN HERAS VICENTE" <>]

 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 purposes.
 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:
 
 http://www.computing.dundee.ac.uk/staff/katya/ML4PG/
 
 We will be happy to hear your feedback.
 
  Best,
  Jónathan Heras and Katya Komendantskaya