Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] refactoring tools

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] refactoring tools


Chronological Thread 
  • From: Vadim Zaliva <vzaliva AT cmu.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] refactoring tools
  • Date: Mon, 9 May 2016 16:53:04 -0700
  • Authentication-results: mail2-smtp-roc.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:oKevYx/kZW0C1P9uRHKM819IXTAuvvDOBiVQ1KB90OscTK2v8tzYMVDF4r011RmSDdSdsqkP0bOempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lS8iL1I/tjqibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEz9RAeO4zMuW2EXjBMAVxbX5RX7QJ7ZuS7n8OdxxX/JboXNUbkoVGH6vO9QQxjyhXJfOg==


On Sat, Apr 30, 2016 at 3:29 PM, Clément Pit--Claudel <clement.pit AT gmail.com> wrote:
https://github.com/Karmaki/coq-dpdgraph could be worth a try to locate unused lemmas.

Thanks! 

Now coq-dpdgraph (version in git, not yet on opam) have a new command line utility 'dpdusage'. it is simple but I found it helpful.

Vadim



--
CMU ECE PhD candidate
Mobile: +1(510)220-1060




Archive powered by MHonArc 2.6.18.

Top of Page