Hello, is there a command in Coq that takes a list of .v files and tells which theorems are never called ? It would be helpful to find dead code and remove it. Dead code often creeps in when we simplify or redo proofs.

Have a look at @Jason Gross coq tools

`dpdusage`

of the`coq-dpdgraph`

tool should do exactly what you want: https://github.com/Karmaki/coq-dpdgraph

Last updated: Jan 29 2023 at 08:28 UTC