The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

You could write a definition for the coq language using Semantic in Emacs

http://www.gnu.org/software/emacs/manual/html_node/emacs/Semantic.html

Semantic goes the extra mile in extensible and configurable editors like Emacs by striving to rigorously understand the language and its syntax. So if you wrote that, not only would you be helping the open source community, but you would also provide yourself with a way to colorize all the un-referenced definitions/theorems in a module. And if  you can colorize them, you can put it into a configurable script!

On Thu, Jun 20, 2013 at 3:00 PM, Duckki Oe <duckki AT mit.edu> wrote:

Hi,

Is there a tool that can detect unreferenced definitions/theorems in a module (or modules)? I'd like to clean up my modules and remove unnecessary lemmas. But, I put lemmas in hint databases and it'll be very time consuming to manually test if every single lemma is used. Thanks!

-- Duckki