Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Coq 8.17 deprecation warnings #42

Open
andrew-appel opened this issue Mar 30, 2023 · 0 comments
Open

Coq 8.17 deprecation warnings #42

andrew-appel opened this issue Mar 30, 2023 · 0 comments

Comments

@andrew-appel
Copy link
Collaborator

In various tactics such as fcf_skip, the use of "intuition" leads to this warning in Coq 8.17:

Warning:
"auto with *" was used through the default "intuition_solver" tactic.
This will be replaced by just "auto" in the future.

The quick-and-dirty way to fix this is to replace intuition with intuition auto with *. The cleaner way to fix it is intuition auto with XXX where XXX is the set of hint databases you really need.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant