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.
In various tactics such as fcf_skip, the use of "intuition" leads to this warning in Coq 8.17:
The quick-and-dirty way to fix this is to replace
intuitionwithintuition auto with *. The cleaner way to fix it isintuition auto with XXXwhere XXX is the set of hint databases you really need.