aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorHugo Herbelin2020-01-19 08:43:36 +0100
committerGitHub2020-01-19 08:43:36 +0100
commit927c683116c17a4746afdc4000ba2015591d3ba2 (patch)
treeb4f88427caf935b211a2154fc6a1c7436c798e0c /dev
parent1f3ad4f8ebbf48d68488d19335d3c2db18e248f4 (diff)
Removing text saying XML is future of PG, adding explicitly vscoq as a user
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/xml-protocol.md3
1 files changed, 1 insertions, 2 deletions
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 0fc0a413ba..f0b8d6630f 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -5,8 +5,7 @@ for his [vscoq](https://github.com/siegebell/vscoq/) project.
Here, the aim is to provide a "hands on" description of the XML
protocol that coqtop and IDEs use to communicate. The protocol first appeared
-with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming
-versions of Proof General.
+with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/siegebell/vscoq/), and other user interfaces.
A somewhat out-of-date description of the async state machine is
[documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md).