A plugin for the Coq Proof Assistant 8.5 and 8.6 in Visual Studio Code.
Features
- Asynchronous proofs
- Syntax highlighting
- 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
- Works with prettify-symbols-mode
- Supports _CoqProject
- The proof-view can be opened in an external web browser
- LtacProf results treeview
Screenshots
LtacProfiling view:
