Yannick Forster (Aug 04 2020 at 06:42): Yannick Forster (Aug 04 2020 at 06:42):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?
Pierre-Marie Pédrot (Aug 04 2020 at 08:37):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 @.
Ali Caglayan (Aug 04 2020 at 08:43):What about for more complicated hints? Should we just ignore the warnings and wait for https://github.com/coq/coq/pull/12493
Pierre-Marie Pédrot (Aug 04 2020 at 09:03):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.
Yannick Forster (Aug 04 2020 at 09:40):Thanks Pierre-Marie!
Last updated: Dec 05 2023 at 05:01 UTC