The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

Hi,

Similar to Duckki Oe [1] I would like to get a listing of all
lemmas and definitions that are not used in a certain Coq
development. Similar to [2], I guess that this is relatively easy
to achieve with a plugin. 

If I were to write such a plugin, were should I start searching
for all declarations known to the system? I guess a vernacular
has access to the current module, from where I could search
dependent modules with all declarations therein. Where do I find
this current module?

Bye,

Hendrik


[1] https://sympa.inria.fr/sympa/arc/coq-club/2013-06/msg00141.html
[2] https://sympa.inria.fr/sympa/arc/coq-club/2012-04/msg00078.html