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