Now that Coq/Coq#18193 is available, I propose to take a tour of the stdlib and use it to warn about files which are marked as deprecated in the comments (hopefully, it should be simpler than Coq/Coq#18164). What do you think about it?

Unfortunately, I failed my review of https://github.com/coq/coq/pull/18193 and we need to wait for https://github.com/coq/coq/pull/18349 for the feature to be usable.

No worries, I can start listing deprecation candidates.

Last updated: Oct 13 2024 at 01:02 UTC