Can one produce custom TC error messages, maybe through Hint Extern and Ltac2?
Hint Extern
Ltac2
(or some other existing plugin)
Last updated: Sep 26 2023 at 11:01 UTC