Stream: Coq users

Topic: "Declaring arbitrary terms as hints is fragile"

view this post on Zulip 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?

view this post on Zulip 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 @.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yannick Forster (Aug 04 2020 at 09:40):

Thanks Pierre-Marie!

Last updated: Apr 19 2024 at 17:02 UTC