abab9579 (Sep 08 2022 at 00:38): abab9579 (Sep 08 2022 at 00:38):Just tried it, it is not the behavior I want - it seems like each step is entire Ltac tactic. I guess I chose the wrong wording.
It seems like this particular tactic usage rewrite frdiffE hangs for indefinitely long (it does seem to stop at some point though), and I need to know what is happening internally. I will try to use profiling for this.
abab9579 (Sep 08 2022 at 00:45):OH, nevermind. It seems like rewrite itself is a primitive tactic.
Thank you for general guidance! I will use this debugging for more complex tactics.
Notification Bot (Sep 08 2022 at 00:45):abab9579 has marked this topic as resolved.
Last updated: Jan 29 2023 at 06:02 UTC