Stop using auto with * in intuition

[SkySkimmer]

No description provided.

[xavierleroy]

Thanks for this pull request. I saw the warnings and I know intuition is about to change. Earlier this year, I tried to do fix each call to intuition but didn't go all the way to the end. Your code is nicer because you just change the Tauto.intuition_solver tactic, not each use of intuition. However, Tauto.intuition_solver is not supported in Coq 8.14 and 8.12 (the oldest version supported by CompCert), so I'll probably go back to my approach, with the additional knowledge gained from your code. (I didn't know about the exfalso hint database...)

Also: you left an intuition info_auto with * , I took the liberty to replace it by intuition and it works just fine.

[SkySkimmer]

However, Tauto.intuition_solver is not supported in Coq 8.14 and 8.12 (the oldest version supported by CompCert),

Tactic Notation "intuition" := (intuition some_solver) also works as long as intuition isn't called through another tactic

[SkySkimmer]

intuition is about to change

There is no rush I think. The warning is enough to avoid inadvertently relying on it in new code, and there are too many users of default intuition in our CI for us to bother porting without a stronger motivation IMO.

[xavierleroy]

Using this PR as a guide, I was able to silence all the 8.17 warnings about intuition, while remaining compatible with 8.12 and up. See 974fbd8. You're listed as co-author on this commit. Now we can close this PR. Thanks again.