Stream: Coq users

Topic: Custom TC search error messages?


view this post on Zulip Paolo Giarrusso (Aug 05 2020 at 14:21):

Can one produce custom TC error messages, maybe through Hint Extern and Ltac2?

view this post on Zulip Paolo Giarrusso (Aug 05 2020 at 14:21):

(or some other existing plugin)


Last updated: Jun 25 2024 at 14:01 UTC