Stream: Coq users

Topic: debugging slow autorewrite

view this post on Zulip Roger Bosman (Apr 27 2021 at 08:22):

Hi all,
I have a rule for autorewrite that is very slow, even when it is the only rule given to autorewrite. This singular hint does the opposite of what simpl does, so doing repeat(tactic; simpl) will loop forever. The weird thing is that when I run autorewrite with all my hints it takes a long time, but it does end up with the right answer. How do I debug this?

Last updated: Oct 03 2023 at 20:01 UTC