Is it possible to add hints about certain theories to use in auto for just one lemma and then those hints will not apply for the rest of the coq file ?
There are approximations: auto using lemma, or Local Hint Resolve inside a section
Last updated: Jan 31 2023 at 13:02 UTC