Vincent Semeria (Jul 12 2021 at 08:13): Vincent Semeria (Jul 12 2021 at 08:13):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.
Bas Spitters (Jul 12 2021 at 09:45):Have a look at @Jason Gross coq tools
Yannick Forster (Jul 12 2021 at 11:03):dpdusage of thecoq-dpdgraph tool should do exactly what you want: https://github.com/Karmaki/coq-dpdgraph
Last updated: Jun 10 2023 at 06:31 UTC