Paolo Giarrusso (Aug 05 2020 at 14:21): Paolo Giarrusso (Aug 05 2020 at 14:21):Can one produce custom TC error messages, maybe through Hint Extern and Ltac2?
Paolo Giarrusso (Aug 05 2020 at 14:21):(or some other existing plugin)
Last updated: Oct 13 2024 at 01:02 UTC