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.
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.
abab9579 has marked this topic as resolved.
Last updated: Jan 29 2023 at 06:02 UTC