VsCoq 1 is an extension for Visual Studio Code (VS Code)
and VSCodium with support for the Coq Proof Assistant.
It is a legacy version compatible with Coq 8.17 or lower. If you are using Coq 8.18 or higher please use the VsCoq extension.
This extension is currently developed by @maximedenes and contributors, as
part of Coq Community. The
original author of this extension is @siegebell.
Commands: step forward, interpret to point, interrupt computation, queries, set display options, etc.
Diff view for proof-view: highlight which terms change between states
Smarter editing: does not roll back the state when editing whitespace or comments