aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/README
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-21 22:52:06 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-21 22:52:06 +0000
commit8fe2660c3cdbb75c2067deae664d4f3242bb4d63 (patch)
treef2c3e305895b41fb9e2a0b7f9517ef34f3c2bd73 /coq/README
parent8ae991c148d86724a43f778efd688705e0fe59a2 (diff)
Updated.
Diffstat (limited to 'coq/README')
-rw-r--r--coq/README3
1 files changed, 2 insertions, 1 deletions
diff --git a/coq/README b/coq/README
index 2bb90f33..97ea8ec8 100644
--- a/coq/README
+++ b/coq/README
@@ -15,7 +15,8 @@ Coq Proof General has experimental multiple file handling for some
versions. It does not have support for proof by pointing.
There is support for X Symbol, using simple character sequences rather
-than a special language of tokens. See notes below for syntax.
+than a special language of tokens (which works well with V8's new
+syntax!). See notes below.
There is a tags program, coqtags.