The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear all,

I would like to have a way to remove theorems and definitions from a development that have become spurious. The idea is that I would like to mark some theorems and definitions as being the goal of the development, e.g., by annotating them as being "precious" or something like that and then run coq over the development and have it output on which theorems and definitions my "precious" definitions and theorems do not depend. Is there any way to do this? Note that the development could include multiple files.

I have done such things in the past by commenting out everything that is not precious and use coq error messages to find out what is needed and getting that back from the comments. Everything that is still commented out after many iterations of this is needed for the development but this is a bit labor intensive and does not scale well.

Have a nice day,

Chris