Today’s release of Coq Platform 2021.09.0 includes a preview of the Ltac Visual Debugger on top of Coq 8.14. It’s not merely “interactive”; it’s a visual debugger. It’s described in https://github.com/coq/coq/wiki/Ltac-Debugger-Preview. Let me know your suggestions for it and whether you find it useful.
2 Likes