Skip to content

Commit

Permalink
Merge pull request #226 from coq/update-vscode-ext-description
Browse files Browse the repository at this point in the history
Update description of VSCode extensions
  • Loading branch information
Zimmi48 authored Oct 4, 2023
2 parents 1db4898 + 701da1c commit 98a00d1
Showing 1 changed file with 5 additions and 12 deletions.
17 changes: 5 additions & 12 deletions pages/user-interfaces.html
Original file line number Diff line number Diff line change
Expand Up @@ -13,21 +13,14 @@
<ul>

<li>
<strong>Visual Studio Code</strong> and <strong>VSCodium</strong> users can use either of
<strong>Visual Studio Code</strong> and <strong>VSCodium</strong> users can
install either
the <a href="https://github.com/coq-community/vscoq">VsCoq
extension</a>, which is actively maintained by several contributors as part
of <a href="https://github.com/coq-community/manifesto">coq-community</a>, or
the new <a href="https://github.com/ejgallego/coq-lsp">coq-lsp extension</a>,
which is based on an implementation of the <a
extension</a>, or
the <a href="https://github.com/ejgallego/coq-lsp">coq-lsp extension</a>.
Both extensions are now based on the <a
href="https://microsoft.github.io/language-server-protocol">Language
Server Protocol</a> standard, with custom extensions.

<tt>coq-lsp</tt> provides continous document checking and position-based
document navigation (an interaction model similar to what is found in e.g.,
Lean, and which departs from the model found in other Coq user interfaces).
See <tt>coq-lsp's</tt> <a
href="https://github.com/ejgallego/coq-lsp/blob/main/etc/FAQ.md">FAQ</a>
for more information.
</li>

<li>
Expand Down

0 comments on commit 98a00d1

Please sign in to comment.