Debugging generalized rewriting tactics

Open radrow opened this issue 5 months ago • 1 comments

Render: https://github.com/radrow/rfcs/blob/set-debug-rewrite/text/000-set-debug-rewrite.md

Referenced issue: rocq-prover/rocq#9285

Jul 07 '25 10:07 radrow

You might also consider whether a step by step GUI display of the term being rewritten (akin to the Ltac debugger display) would be effective (instead of a printed trace). The newer version of the debugger (not yet merged) might be adapted for that without, I think, too much difficulty.

Jul 07 '25 17:07 jfehrle