Awesome

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:
<img alt="Simple example" src="https://cloud.githubusercontent.com/assets/16118166/15950939/a00a8e02-2e81-11e6-98c4-9425bf6ab9c9.png" width="100%"/>