Cleanup warnings

[SkySkimmer]

This should be backwards compatible.

Remaining warnings:

• implicit-create-(rewrite-)hint-db
• missing-scheme, but only in cases were turning it into an error ignores the error (some scripts doing try rewrite where rewriting does nothing) (modulo rocq bug which prevents try from catching this error Fix "try rewrite" not catching "missing-scheme" error rocq#21370)
• notation level warnings for non-local notations (changing these may not be backwards compatible but we should probably do it eventually)