Gregory Malecha (Sep 09 2021 at 19:37): 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
Gregory Malecha (Sep 09 2021 at 20:10):it's a universe problem :-)
Last updated: Oct 03 2023 at 04:02 UTC