Merge PR rocq-prover#21129: Stop using auto with * in intuition solver.

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

Author: coqbot-app[bot]

doc/changelog/04-tactics/21129-intuition-stop-using-auto-with-star-Removed.rst

@@ -0,0 +1,6 @@
+- **Removed:**
+  the implicit call to `auto with *` in intuition solver, that
+  was deprecated since 8.17
+  (`#21129 <https://github.com/rocq-prover/rocq/pull/21129>`_,
+  fixes `#4949 <https://github.com/rocq-prover/rocq/issues/4949>`_,
+  by Pierre-Marie Pédrot).

theories/Corelib/Init/Tauto.v

@@ -105,9 +105,7 @@ Local Ltac tauto_gen flags := tauto_intuitionistic flags || tauto_classical flag
 Ltac tauto := with_uniform_flags ltac:(fun flags => tauto_gen flags).
 Ltac dtauto := with_power_flags ltac:(fun flags => tauto_gen flags).
 
-Ltac intuition_solver :=
-  first [solve [auto]
-        | tryif solve [auto with *] then warn_auto_with_star else idtac].
+Ltac intuition_solver := auto.
 
 Local Ltac intuition_then tac := with_uniform_flags ltac:(fun flags => intuition_gen flags tac).
 Ltac intuition := intuition_then ltac:(idtac;intuition_solver).