Skip to content

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