Override Tauto.intuition_solver instead of redefining `intuition` (needs Coq 8.15.2)
Currently, std++ shadows the intuition tactic to prevent intuition from using auto with *. Coq 8.15.2 added a Tauto.intuition_solver that can be redefined instead shadowing the intuition tactic, see https://github.com/coq/coq/pull/15866
From https://coq.inria.fr/distrib/current/refman/changes.html#changes-in-8-15-2
Added: intuition and dintuition use Tauto.intuition_solver (defined as auto with *) instead of hardcoding auto with *. This makes it possible to change the default solver with Ltac Tauto.intuition_solver ::= ...
Edited by Ralf Jung