A plugin for the Coq Proof Assistant 8.5 and 8.6 in Visual Studio Code.

• Setup instructions
• Tips

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: