Stream: Coq users

Topic: Print error message from failed tactic


view this post on Zulip Gregory Malecha (Sep 09 2021 at 19:37):

I'm inside of a typeclass search and I have a Hint Extern that is something like Hint Extern ... => idtac "X"; apply foo => .... This fails, but when I copy the goal, and run apply foo, it succeeds. I'm wondering if there is some way to say report apply foo so that it will not discard the error message

view this post on Zulip Gregory Malecha (Sep 09 2021 at 20:10):

it's a universe problem :-)


Last updated: Feb 08 2023 at 23:03 UTC