When I do e.g.
Hint Resolve @plus_comm : core. Coq 8.12 gives me
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation]. While I believe that in general you might obtain fragile behaviour, is this case with prefixing a lemma by
@ really fragile, or is it safe to ignore this warning?
Just remove the
@. Hints that consist only of a global reference have been treated specially for quite a long time already, and behave the same as if you were prefixing them with
What about for more complicated hints? Should we just ignore the warnings and wait for https://github.com/coq/coq/pull/12493
If it's easy to introduce yourself a proxy constant, please do it. The PR has some drawbacks, like the unnatural naming scheme, and some issues w.r.t. module signatures.
Last updated: Feb 06 2023 at 12:04 UTC