coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] refactoring tools

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] refactoring tools
Date: Sat, 30 Apr 2016 18:29:27 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:XEbICRUWTGZM+d7z8j1SLuFz3IjV8LGtZVwlr6E/grcLSJyIuqrYZhCAt8tkgFKBZ4jH8fUM07OQ6PCwHzxQqs/f4TgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2DJVUYz2PjMPtbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN/dwcbsNBzM/dmsx+cfDtB/ZTALJ6GFPfH8Rl09jB4nA4Rfmaa/wrm6/ne50xSWXOYWiRrQ5XDmk8+FzSQPAhyIONjp/+2bS3J8jxJlHqQ6s8kQsi7XfZ5uYYaJz

On 2016-04-29 22:20, Vadim Zaliva wrote:
> As my project's code base grows I keep discovering lemmas which are
> no longer needed. Also sometimes I end up with two lemmas proving the
> same things under different names. How fellow coq users deal with
> this? Are there are any tool scripts which could help me to find
> unused or duplicate lemmas?

https://github.com/Karmaki/coq-dpdgraph could be worth a try to locate unused
lemmas.

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature

Re: [Coq-Club] refactoring tools, Clément Pit--Claudel, 05/01/2016
- Re: [Coq-Club] refactoring tools, Vadim Zaliva, 05/10/2016