coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vadim Zaliva <vzaliva AT cmu.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] refactoring tools
- Date: Fri, 29 Apr 2016 19:20:39 -0700
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f49.google.com
- Ironport-phdr: 9a23:gcSpURTEPpGk1OS0ora6pQQcQ9psv+yvbD5Q0YIujvd0So/mwa64ZxWN2/xhgRfzUJnB7Loc0qyN4/CmCTNLvMfJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviq9uDPE4V1XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzAomxZJBkD35RX7QJ655jXov+58xiCyNsjrC704RGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==
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?
--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
- [Coq-Club] refactoring tools, Vadim Zaliva, 04/30/2016
Archive powered by MHonArc 2.6.18.