@Jim Fehrle : I tried the debugger in 8.15.1 and found that the goal does not change any more when I step through ltac code - it remains what it was when debugging started. If I remember right, this was not so in previous versions. Is this expected?
Can you provide a short example? I couldn't reproduce the problem in master or the updated v8.15 (= 8.15.1 IIUC) with this example:
The only change I recall to debugger goal printing is it that the output will show multiple goals. It's not expected. If you can reproduce this, please open an issue.
It also appears to update multiple goals correctly:
@Jim Fehrle : OK, your example works and it doesn't seem to be easy to find a trivial example. My issues are with the VST "forward" tactic - let me see if I can boil it down.
@Jim Fehrle : the issue happens when one calls a tactic from another file. I will file an issue.
Last updated: Oct 03 2023 at 21:01 UTC