Coq Support for Visual Studio Code
TypeScript C# HTML Other
Clone or download
Latest commit 61be3d7 Mar 5, 2017

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


  • 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


Simple example

Screenshot of Proof Goal

LtacProfiling view:
Simple example