search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
755 stars 70 forks source link

Stop using auto with * in intuition #129

Closed SkySkimmer closed 1 year ago

SkySkimmer commented 1 year ago

compat seems troublesome

JasonGross commented 1 year ago

Do the standard trick of stuffing

Module Coq. Module plugins. Module Tauto. Ltac2 intuition_solver := idtac. End ...

(or whatever the actual full path is) in some file that you Require Import, then overwrite it as Ltac Coq.plugins.Tauto.intuition_solver ::= .... Coq will refuse to shadow absolute names that exist, so this will be a no-op if the name does not exist (overwriting the unused tactic), but will have the desired effect if the name does exist.

SkySkimmer commented 1 year ago

Tactic Notation "intuition" := (intuition auto with whatever) may work, I'll try later.

SkySkimmer commented 1 year ago

It doesn't work, I guess because intuition is called through something else.