Stream: Coq users

Topic: Core, nocore, and custom hint DBs


view this post on Zulip Justin Kelm (Sep 13 2023 at 22:14):

I have a custom hint database db, and (let's say for legacy reasons) a core database that has some questionable hints added to it. How do I only use hints coming from db in e.g. eauto?

If I use eauto or eauto with core, of course it uses the problematic core. If I use eauto with nocore per the documentation, it stops the problem behavior, but also gets nowhere without db. Yet, if I use eauto with db, it succeeds when my Hint Resolve ... : db hints apply, but it appears to still apply problematic core hints when such db hints fail to apply.

What is going on here, exactly?

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 22:52):

What about eauto with db nocore? eauto with db is to documented to

Use the hint databases ident+ in addition to the database core. Use the fake database nocore to omit core.

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 22:53):

(from https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:tacn.auto )

view this post on Zulip Justin Kelm (Sep 14 2023 at 05:19):

Thank you! db nocore works as I expected db alone would have.


Last updated: Jun 13 2024 at 19:02 UTC