The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

I think the problem here is

>  "I put lemmas in hint databases"

Therefore, an emacs module that merely parses the *.v file won't
suffice, because it's possible that there is some Lemma lem_X, where:

  *) the name lem_X does not appear anywhere else
  *) however lem_X is used as as rewrite/resolve hint used by auto/crush


On Fri, Jun 21, 2013 at 6:35 AM, Kenneth Adam Miller
<kennethadammiller AT gmail.com>
 wrote:
> 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
>>
>>
>