Is there a way to redefine a built-in tactic? Concretely, I tried the following:
Ltac refold := idtac "foo".
Ltac core_constructor := constructor.
Ltac constructor ::= core_constructor ; refold.
Goal nat.
constructor. (* does not print anything… *)
But it seems like constructor
does not get redefined as I hoped it would be…
Tactic Notation "constructor" := core_constructor ; refold.
Meven Lennon-Bertrand has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC