From 26d7af8d28c6e4b24eada1858395dad18767476e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Wed, 4 Oct 2023 12:56:06 +0200
Subject: [PATCH 1/5] Mention the existence of NeoVim support for VsCoq and
 coq-lsp.

---
 pages/user-interfaces.html | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html
index 3996834554..ad19bd6cb4 100644
--- a/pages/user-interfaces.html
+++ b/pages/user-interfaces.html
@@ -36,11 +36,10 @@
 </li>
 
 <li>
-<strong>Vim/NeoVim</strong> users can use the actively
-maintained <a href="https://github.com/whonore/Coqtail">Coqtail</a>
-extension.  This extension is partly based upon a previous, and now
-unmaintained, Vim extension
-called <a href="https://github.com/the-lambda-church/coquille">Coquille</a>.
+<strong>Vim/NeoVim</strong> users can use the <a href="https://github.com/whonore/Coqtail">Coqtail</a>
+extension.  NeoVim users can also test the experimental support for
+<a href="https://github.com/tomtomjhj/vscoq.nvim">VsCoq's vscoqtop server</a>
+or for <a href="https://github.com/tomtomjhj/coq-lsp.nvim">coq-lsp</a>.
 </li>
 
 </ul>

From 6c37904671b45442d6ec6bb33d7e03606dc070a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Wed, 4 Oct 2023 12:56:43 +0200
Subject: [PATCH 2/5] Remove excessive information clutering the list of editor
 support packages.

---
 pages/user-interfaces.html | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html
index ad19bd6cb4..eb11957e75 100644
--- a/pages/user-interfaces.html
+++ b/pages/user-interfaces.html
@@ -28,11 +28,6 @@
 mode <a href="https://proofgeneral.github.io/">Proof General</a>, that
 can be extended by the minor Coq
 mode <a href="https://github.com/cpitclaudel/company-coq">Company-Coq</a>.
-Proof General was one of the first user interface for proof
-assistants, and is one of the most used user interface for Coq today.
-Proof General and Company-Coq give access to many productivity
-shortcuts, including auto-completion and documentation.  On the other
-hand, async proof processing is not supported.
 </li>
 
 <li>

From 3fe4962db3ec37e215defcf2d8dcca669707b6c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Wed, 4 Oct 2023 13:02:09 +0200
Subject: [PATCH 3/5] Move coq_jupyter to the experimental section.

---
 pages/user-interfaces.html | 16 +++++-----------
 1 file changed, 5 insertions(+), 11 deletions(-)

diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html
index eb11957e75..42e7ae1dd6 100644
--- a/pages/user-interfaces.html
+++ b/pages/user-interfaces.html
@@ -41,17 +41,6 @@
 
 </p>
 
-<p>
-An experimental alternative to the editors mentioned above is the
-computational notebook interface provided by Jupyter.
-A <a href="https://github.com/EugeneLoy/coq_jupyter/">Jupyter kernel
-for Coq</a> is available if you want to try this interface, for
-instance for pedagogical or readability purposes.  One of the
-advantages of using a Jupyter notebook is that you can save and
-display a selection of intermediate proof steps, which your reader
-will see without the need to reexecute the document.
-</p>
-
 </div>
 
 <div class="frameworklinks">
@@ -111,6 +100,11 @@
 uncertain:
 <ul>
 <li>
+A <a href="https://github.com/EugeneLoy/coq_jupyter/">Jupyter kernel for Coq</a>
+(supports Coq 8.6 and newer versions using <a href="https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md">Coq's
+XML protocol for IDEs</a>).
+</li>
+<li>
 The <a href="http://coqoon.github.io/">Coqoon</a> Eclipse plugin was
 initially based upon
 the <a href="https://bitbucket.org/coqpide/pidetop/src/PIDEtop/">PIDEtop

From 6cab5ed7232e1adfc83f10b8288ea71074fff79c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Wed, 4 Oct 2023 13:04:12 +0200
Subject: [PATCH 4/5] Remove excessive information about CoqIDe clutering the
 user interface page.

---
 pages/user-interfaces.html | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html
index 42e7ae1dd6..c6469890f2 100644
--- a/pages/user-interfaces.html
+++ b/pages/user-interfaces.html
@@ -60,14 +60,7 @@
 <p>
 Alternatively, you can
 use <a href="https://coq.inria.fr/refman/practical-tools/coqide.html">CoqIDE</a>,
-which is developed and distributed alongside Coq. CoqIDE relies
-on <a href="https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md">Coq's
-XML protocol for IDEs</a> and implements all of the features provided
-by this protocol, meaning in particular asynchronous evaluation.
-CoqIDE comes with standard basic Emacs-like bindings
-and with some specific Coq-related bindings but, as an editor, it is
-not as complete as a general-purpose editor could be (for instance it
-does not have automatic indentation).
+a standalone desktop application which is developed and distributed alongside Coq.
 </p>
 
 <p>

From e29f18b3d6cd99ca1622d90b706fefc17b5d72c6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Wed, 4 Oct 2023 13:06:15 +0200
Subject: [PATCH 5/5] Remove excessive and negative information about jsCoq.

---
 pages/user-interfaces.html | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html
index c6469890f2..7cee004eb8 100644
--- a/pages/user-interfaces.html
+++ b/pages/user-interfaces.html
@@ -66,10 +66,7 @@
 <p>
 As a way to try Coq without installing anything, you can
 use <a href="https://jscoq.github.io/">JsCoq</a>.  JsCoq loads Coq
-entirely in your browser.  However, it is too limited to conduct
-actual projects: it lacks access to the VM and native computing
-machineries of Coq, and may hit out-of-memory and stack-overflow
-failures quicker than native versions of Coq.
+entirely in your browser.
 </p>
 
 </div>