Michael Soegtrop (Apr 04 2022 at 16:56): Michael Soegtrop (Apr 04 2022 at 16:56):@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?
Jim Fehrle (Apr 04 2022 at 19:38):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.
Jim Fehrle (Apr 04 2022 at 19:41):It also appears to update multiple goals correctly:
Michael Soegtrop (Apr 05 2022 at 07:18):@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.
Michael Soegtrop (Apr 05 2022 at 08:53):@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