Many of the MathComp-using projects I maintain have a bunch of
Warning: Nothing to inject. However, there is no warning code associated with this message, so I can't suppress it. This seems inconsistent with nearly any other warning I've encountered - is it by design, or should report an issue?
I think you should report a bug.
Indeed this "warning" predates the warning system, and the merge of ssr into Coq came after the new warning system was introduced and all warnings ported to the new system. What a stroke of luck. Please open an issue about porting this warning to the current warning system.
However, providing a minimal example that triggers this requires more cycles than I currently have. Best I can offer is
File "./Core/DepMaps.v", line 52, characters 0-47:
Warning: Nothing to inject.
Is this something the fabled minimizer could be used for?
Goal forall b : bool, b -> False. move=> b [h]. reises the warning as well. As some point
injection started to fail rather than doing nothing on equations that could not be "injected", while used to fail only on non-equations. The problem is that forgetting an extra
[.] in ssr is easy and 99% of our formulas are equations (hidden
. = true). So we had to turn the error into something else, because we had gazillions of instances. If we port the warning to the current system one can easily switch between warning, error or nothing, and that could help getting rid of these little mistakes.
Last updated: Feb 22 2024 at 05:02 UTC