Skip to content
Snippets Groups Projects
Open Override Tauto.intuition_solver instead of redefining `intuition` (needs Coq 8.15.2)
  • View options
  • Override Tauto.intuition_solver instead of redefining `intuition` (needs Coq 8.15.2)

  • View options
  • Open Issue created by Michael Sammler

    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
    • Merge request
    • Branch

    Linked items ... 0

  • Activity

    • All activity
    • Comments only
    • History only
    • Newest first
    • Oldest first
    Loading Loading Loading Loading Loading Loading Loading Loading Loading Loading